Pith. sign in

REVIEW 3 major objections 6 minor 43 references

Learning Probabilistic Temporal Logic Specifications for Stochastic Systems

T0 review · 3 major / 6 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Passive learning of probabilistic temporal logic specifications is solved exactly: the proposed algorithm returns a minimal consistent PLTL+ formula whenever a bounded PLTL formula exists.

desk verdict Solid tool paper with a real new problem formulation, but Theorem 1's minimality claim is not supported by the bounded Boolean set-cover step; the fix is to weaken the theorem. read the letter →

arxiv 2505.12107 v1 pith:53IFIQSU submitted 2025-05-17 cs.LO cs.AIcs.FL

Rajarshi Roy , Yash Pote , David Parker , Marta Kwiatkowska This is my paper · ORCID
classification cs.LOcs.AIcs.FL
keywords probabilisticlineartemporallogicspecificationlearningMarkovchainspassivegrammar-basedenumerationmodelcheckingBooleansetcoverreinforcement
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper tackles the passive-learning problem for stochastic systems: from a set of Markov chains labeled positive or negative, learn a concise specification in probabilistic linear temporal logic (PLTL+) that all positive examples satisfy and no negative example satisfies. The paper proposes a three-stage algorithm that enumerates LTL formulas by size and nesting depth, computes probabilistic satisfaction thresholds for each candidate by model checking, and combines surviving candidates into Boolean formulas via a set-cover step. If a PLTL formula of bounded size, depth, and probability gap separates the sample, the algorithm is claimed to return a smallest consistent PLTL+ formula; if no such formula exists, it reports none. The motivation is that such specifications explain stochastic behaviour, for example the difference between reinforcement-learning policies or between variants of a probabilistic protocol.

What carries the argument

The load-bearing object is a PLTL+ formula: a positive Boolean combination, using conjunction and disjunction, of probabilistic LTL statements of the form $P_{\triangleright\triangleleft p}[\varphi]$, each asserting that the probability of an LTL formula $\varphi$ holding along paths of the DTMC meets threshold $p$. The argument is carried by three procedures over candidate LTL formulas: grammar-based enumeration generates all semantically distinct formulas up to size and nesting depth; probabilistic threshold search computes the probability vector for each candidate on every sample DTMC, reads off the minimum probability among positive examples and the maximum among negative examples, and when the gap exceeds tolerance $\delta$ emits the PLTL formula whose threshold is the midpoint of that gap; Boolean set cover scores leftover candidates by how many sample DTMCs they separate and combines the top $L$ into conjunctions and disjunctions. The midpoint threshold is what converts a measured probability gap into a classifier that every positive example satisfies and no negative example satisfies.

What would settle it

Construct a sample of positive and negative DTMCs whose unique minimal consistent PLTL+ formula is $\Phi_1 \wedge \Phi_2$, with each component's score below the $L$-th best candidate and each component individually not consistent with the sample; run the algorithm with $K = |\Phi_1 \wedge \Phi_2|$, the chosen depth $D$, and the chosen $\delta$. If the output is not $\Phi_1 \wedge \Phi_2$ or is a larger formula, the completeness-and-minimality claim is false for the implemented algorithm.

Watch

Extended reading notes

Core claim

The central discovery is that exact passive learning transfers from deterministic traces to stochastic models by replacing trajectory satisfaction with model-checked satisfaction probabilities and by letting Boolean combinations absorb cases where no single PLTL formula separates the classes. Concretely, the paper claims Theorem 1: with sample size $|S|$, size bound $K$, depth bound $D$, and tolerance $\delta$, the learning algorithm is sound (every returned PLTL+ formula is consistent with the sample and has size at most $K$) and complete-and-minimal (if there exists a PLTL formula in the bounded search space $\Theta(K,D,\delta)$ consistent with the sample, it returns a minimal PLTL+ formula). The proof rests on exhaustive grammar-based enumeration, sound threshold search, and the observation that formulas unsatisfiable in every positive state cannot occur in a minimal consistent formula.

Load-bearing premise

The load-bearing premise is that the Boolean set-cover step keeps enough candidate formulas when it truncates to the L highest-scoring ones; the paper gives no proof that a minimal consistent PLTL+ combination can always be built from that shortlist, so if the needed formula is discarded the completeness-and-minimality guarantee fails.

Editorial extensions

If this is right

  • For any finite sample of Markov chains, the bounded learning problem becomes decidable: the algorithm terminates and either returns a consistent formula of size at most $K$ or certifies that no bounded consistent PLTL formula exists.
  • The learned formulas are small enough to serve as explanations; in the experiments, distinctions between policies trained for different LTL tasks are recovered as statements such as a high probability of globally avoiding holes or of repeatedly reaching a target.
  • A negative result is also informative: for the protocol with more than five secrets, the exhaustive search shows that no formula of the chosen size and depth separates the variants, so the variants are indistinguishable at that specification budget.
  • The tolerance parameter $\delta$ makes the learned descriptions insensitive to small probability perturbations, so the specifications do not chase noise in the sample probabilities.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The published algorithm's Boolean set-cover stage keeps only the $L$ highest-scoring candidates; the proof of Theorem 1 does not address this truncation, so in practice exact minimality of PLTL+ formulas should be read as guaranteed only for the single-formula PLTL case or when the optimal combination lies within the retained shortlist.
  • The same framework could be re-instantiated with a different model-checking oracle, for example one that computes expected rewards, to learn specifications with quantitative reward objectives instead of path probabilities.
  • The midpoint-threshold rule suggests a natural active-learning extension: ask a teacher to label the examples whose measured probabilities fall in the ambiguous gap between the worst positive and best negative values, using the algorithm's own scores to select the most informative queries.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 6 minor

Summary. The paper addresses the passive learning problem of inferring probabilistic linear temporal logic (PLTL) specifications over finite Markov chains. The input is a sample of positive and negative DTMCs, and the goal is a concise PLTL+ formula (a positive Boolean combination of PLTL formulas) that is satisfied by all positive examples and violated by all negative examples. The proposed algorithm, PriTL, combines three procedures: grammar-based enumeration (GBE) of LTL formulas, probabilistic threshold search (PTS) that uses probabilistic model checking to choose probability thresholds, and a Boolean set cover (BSC) procedure that forms Boolean combinations of PLTL candidates. The paper states a soundness, completeness, and minimality guarantee (Theorem 1) and evaluates the tool on RL policy DTMCs and on variants of the EGL contract-signing protocol. The empirical results show that the method finds concise distinguishing formulas in both case studies.

Significance. If the stated guarantees held, this would be the first exact passive learner for probabilistic temporal logic specifications over Markov chains, and the combination of grammar-based enumeration with off-the-shelf probabilistic model checking is a natural and potentially reusable design. The soundness arguments for PTS (Lemma 2) and for the formulas output by BSC (Lemma 4) are credible, and the two case studies demonstrate practical value: the method recovers interpretable formulas that separate RL strategies and detects the absence of distinguishing formulas in the EGL variant comparison. The paper also provides a prototype tool and reproducible experimental setup. However, the completeness-and-minimality claim in Theorem 1 substantially overreaches what is proved: the bounded, score-based BSC step is not shown to preserve completeness or minimality, and the proof of Lemma 1 requires a completeness property of the temporal simplification rules that is not established. These gaps directly affect the paper's central theoretical contribution.

major comments (3)
  1. [§4.3, Algorithm 3, Theorem 1] The completeness and minimality clause of Theorem 1 is not justified by the proof. Algorithm 3 line 5 retains only the L highest-scoring PLTL formulas in H*, and line 6 forms only binary combinations Ψ∘Φ with Ψ∈H and Φ∈H*, without adding new combinations back into H; moreover, BSC is invoked on Bn, the formulas of the current size n, so it never combines PLTL atoms of different sizes. No lemma states that every atom of a minimal PLTL+ formula lies in H*, nor that a Boolean combination with more than one Boolean operator or with unequally sized atoms can be constructed. A component formula can be individually low-scoring because it is true in some negative examples, reducing c(φ,r), and can therefore be excluded from H*, after which the minimal combination containing it is never considered. The parameter L does not appear in the statement or proof of Theorem 1, yet the claimed guarantee would have to depend on it. Consequently, even a minimal PLTL+ formula of the form P>p[a] ∧ P>q[G F b], with atoms of sizes 1 and 3, cannot be produced by the algorithm as written, since no iteration of BSC combines size-1 with size-3 candidates.
  2. [§4.1 and Appendix A, Lemma 1] The proof of Lemma 1 is incomplete. It claims that GBE discards a formula ψ only if there exists an already-enumerated ψ' with ψ≡ψ', but the temporal simplification heuristic actually discards any formula that is not in the syntactic normal form produced by the rewrite rules. The paper does not prove that these rewrite rules are complete for semantic equivalence over (2^AP)^ω, i.e., that every discarded formula is semantically equivalent to a smaller formula already generated. The Boolean simplification heuristic does include a semantic equivalence check via LTL satisfiability, but the temporal simplification does not. Therefore a semantically new formula of size ≤N' and depth ≤D can be discarded, breaking the exhaustive-enumeration premise on which Theorem 1's completeness argument rests.
  3. [§4.2, Lemma 3] The pruning rule in PTS discards φ when VM,φ≡0 for each M∈P or VM,φ≡1 for each M∈N, but Lemma 3 proves only the positive case. The text says 'a similar argument applies to the negative cases' without giving the proof. The negative case is not immediately symmetric: a formula that is true in every negative example can still be useful as a conjunct of a conjunction whose truth on negatives is decided by the other conjunct. A rigorous dual argument is needed to justify discarding formulas in this case, and it should be stated explicitly because the completeness guarantee depends on not discarding useful subformulas.
minor comments (6)
  1. [§2.2] The definition of |Φ| for PLTL+ formulas says it is defined 'exactly the same way' as the LTL size, but it is unclear whether the probability threshold p and the P operator are counted; please clarify, since the threshold values affect the statement of the size bound K in Problem 1.
  2. [§5 and Appendix C.1] There is an inconsistency in the name of the Q-learning variant used for suboptimal strategies: the main text refers to the 'KC' algorithm, while Appendix C.1 uses 'CF' in one place and 'KC' in the next; please make the naming consistent.
  3. [Figure 2 and §4] The high-level flow suggests that at each size n, PTS and BSC both run before moving to n+1, but Algorithm 2 has an early return. Please state explicitly whether BSC is skipped when PTS finds a consistent PLTL formula, as this affects the minimality claim.
  4. [Table 1] The column 'LTL Searched' reports fractions such as 24/24 and 110/186; the denominator is not defined in the text or caption, so it is unclear whether it counts all formulas up to the learned formula's size, before or after heuristics.
  5. [Appendix A, proof of Lemma 3] The sentence 'Based on the semantics of X, π[1:] |= φ for some i∈N' is garbled: the semantics of X involves π[1:], with no index i, whereas the index i belongs to the F or U cases. Please correct this typo.
  6. [References] Reference [Brockman, 2016] duplicates [Brockman et al., 2016] and should be merged or removed.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: the learning pipeline is anchored to external PRISM model checking, and the Theorem 1 completeness gap is an unproven step, not circularity.

full rationale

No load-bearing step reduces to its own input. GBE enumerates LTL formulas independently of the sample; PTS computes satisfaction probabilities via PRISM and sets thresholds from the computed vectors (m_phi = (p_phi + n_phi)/2); BSC stores only formulas that are explicitly checked to be consistent (Algorithm 3, line 8). Hence Lemma 4's soundness does not rest on the self-cited [Raha et al., 2022] adaptation; that citation supplies a scoring heuristic, not the consistency guarantee. No fitted parameter is renamed as a prediction: the learned thresholds are exactly the passive-learning task, and the paper makes no out-of-sample prediction claim. The one genuine concern is a proof gap, not circularity: Theorem 1's completeness and minimality proof cites exhaustive GBE (Lemma 1) and Lemma 3, but Algorithm 3 keeps only the L highest-scoring formulas in H* (line 5) and forms one round of pairwise combinations (line 6), with no lemma showing that every atom of a minimal PLTL+ formula survives this pruning. This could invalidate the stated minimality guarantee, but it is not an equivalence of output to input by construction. Therefore the circularity score is 0.

Assumptions & free parameters 3 free parameters · 5 assumptions · 0 invented entities

The central claim rests on standard model-checking correctness, the assumption that input DTMCs are exact, and an unproved completeness assumption for the Boolean set-cover heuristic. No new physical or formal entities are postulated; PLTL+ is a syntactic extension of existing PLTL.

free parameters (3)
  • probabilistic tolerance delta = 0.05
    Hand-set minimum gap between positive and negative satisfaction probabilities. It determines when a formula is considered distinguishing and sets the midpoint threshold.
  • maximum temporal depth D = 2
    Hand-set bound on LTL nesting depth. Formulas deeper than 2 are excluded from the search, which affects both interpretability and completeness.
  • Boolean combination limit L = 10
    BSC keeps only the 10 highest-scoring PLTL formulas for Boolean combination. This is omitted from Theorem 1 but can affect whether a minimal PLTL+ formula is found.
assumptions (5)
  • domain assumption PRISM correctly computes Pr(s |= phi) for LTL formulas on finite DTMCs.
    PTS relies on PRISM's hybrid model checking engine for all probability vectors. Correctness of this step is assumed from the model checking literature rather than proved here.
  • domain assumption The input DTMCs exactly represent the systems of interest.
    The consistency guarantee is with respect to the given Markov chains. If the DTMCs are approximate or sampled from trajectories, the learned formula may not hold for the real system.
  • standard math Finite-memory strategies induce finite DTMCs.
    Section 2.1 restricts to finite-memory strategies so that the induced DTMC is finite, citing Baier and Katoen 2008. This is standard and well supported.
  • ad hoc to paper BSC's bounded heap and scoring function suffice to find minimal Boolean combinations.
    No proof is given that keeping only the L highest-scoring formulas preserves completeness. This premise is load-bearing for the minimality part of Theorem 1 and is not established.
  • domain assumption A consistent PLTL formula exists within Theta(K,D,delta).
    The completeness and minimality guarantee is conditional on a solution existing inside the bounded search space defined by size, depth, and tolerance.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Learning Probabilistic Temporal Logic Specifications for Stochastic Systems." pith.science (2026). https://pith.science/paper/53IFIQSU

@misc{pith2026250512107,
  author       = {Pith},
  title        = {Pith review of: Learning Probabilistic Temporal Logic Specifications for Stochastic Systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/53IFIQSU}},
  note         = {Machine review of arXiv:2505.12107}
}
read the original abstract

There has been substantial progress in the inference of formal behavioural specifications from sample trajectories, for example, using Linear Temporal Logic (LTL). However, these techniques cannot handle specifications that correctly characterise systems with stochastic behaviour, which occur commonly in reinforcement learning and formal verification. We consider the passive learning problem of inferring a Boolean combination of probabilistic LTL (PLTL) formulas from a set of Markov chains, classified as either positive or negative. We propose a novel learning algorithm that infers concise PLTL specifications, leveraging grammar-based enumeration, search heuristics, probabilistic model checking and Boolean set-cover procedures. We demonstrate the effectiveness of our algorithm in two use cases: learning from policies induced by RL algorithms and learning from variants of a probabilistic model. In both cases, our method automatically and efficiently extracts PLTL specifications that succinctly characterise the temporal differences between the policies or model variants.

Figures

Figures reproduced from arXiv: 2505.12107 by the authors.

Figure 1
Figure 1. An illustration of an office-world environment with the following features: office [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. The high-level overview of the learning algorithm. The set [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Runtime comparison for strategies generated from varying [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: The MDP environment for the frozen lake task. Blue rep [PITH_FULL_IMAGE:figures/full_fig_p010_4.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

43 extracted references · 30 canonical work pages

  1. [1]

    Principles of model checking

    Christel Baier and Joost - Pieter Katoen. Principles of model checking . MIT Press, 2008

    2008

  2. [2]

    Data-driven statistical learning of temporal logic properties

    Ezio Bartocci, Luca Bortolussi, and Guido Sanguinetti. Data-driven statistical learning of temporal logic properties. In FORMATS , volume 8711 of Lecture Notes in Computer Science , pages 23--37. Springer, 2014

    work page 2014

  3. [3]

    Survey on mining signal temporal logic specifications

    Ezio Bartocci, Cristinel Mateis, Eleonora Nesterini, and Dejan Nickovic. Survey on mining signal temporal logic specifications. Inf. Comput. , 289(Part):104957, 2022

    work page 2022

  4. [4]

    40 years of formal methods - some obstacles and some possibilities? In FM , volume 8442 of Lecture Notes in Computer Science , pages 42--61

    Dines Bj rner and Klaus Havelund. 40 years of formal methods - some obstacles and some possibilities? In FM , volume 8442 of Lecture Notes in Computer Science , pages 42--61. Springer, 2014

    2014

  5. [5]

    Explainable multi-agent reinforcement learning for temporal queries

    Kayla Boggess, Sarit Kraus, and Lu Feng. Explainable multi-agent reinforcement learning for temporal queries. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China , pages 55--63. ijcai.org, 2023

    work page 2023

  6. [6]

    A decision tree approach to data classification using signal temporal logic

    Giuseppe Bombara, Cristian Ioan Vasile, Francisco Penedo, Hirotoshi Yasuoka, and Calin Belta. A decision tree approach to data classification using signal temporal logic. In Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control , HSCC '16, page 1–10, New York, NY, USA, 2016. Association for Computing Machinery

    work page 2016

  7. [7]

    Learning branching-time properties in CTL and ATL via constraint solving

    Benjamin Bordais, Daniel Neider, and Rajarshi Roy. Learning branching-time properties in CTL and ATL via constraint solving. In Andr \' e Platzer, Kristin Yvonne Rozier, Matteo Pradella, and Matteo Rossi, editors, Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part I , volume 14933 of Lecture Notes...

    work page 2024

  8. [8]

    Zavlanos, and Miroslav Pajic

    Alper Kamil Bozkurt, Yu Wang, Michael M. Zavlanos, and Miroslav Pajic. Control synthesis from linear temporal logic specifications using model-free reinforcement learning. In 2020 IEEE International Conference on Robotics and Automation, ICRA 2020, Paris, France, May 31 - August 31, 2020 , pages 10349--10355. IEEE , 2020

    work page 2020

Show all 43 references
  1. [10]

    Openai gym

    G Brockman. Openai gym. arXiv preprint arXiv:1606.01540 , 2016

    2016 arXiv

  2. [11]

    McIlraith

    Alberto Camacho and Sheila A. McIlraith. Learning interpretable models expressed in linear temporal logic. In ICAPS , pages 621--630. AAAI Press, 2019

    2019

  3. [12]

    Klassen, Richard Anthony Valenzano, and Sheila A

    Alberto Camacho, Rodrigo Toro Icarte, Toryn Q. Klassen, Richard Anthony Valenzano, and Sheila A. McIlraith. LTL and beyond: Formal languages for reward function specification in reinforcement learning. In Sarit Kraus, editor, Proceedings of the Twenty-Eighth International Join...

    2019

  4. [13]

    Learning temporal properties from event logs via sequential analysis

    Francesco Chiariello. Learning temporal properties from event logs via sequential analysis. In TIME , volume 318 of LIPIcs , pages 14:1--14:14. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2024

    2024

  5. [14]

    Danesh, Anurag Koul, Alan Fern, and Saeed Khorram

    Mohamad H. Danesh, Anurag Koul, Alan Fern, and Saeed Khorram. Re-understanding finite-state representations of recurrent policy networks. In ICML , volume 139 of Proceedings of Machine Learning Research , pages 2388--2397. PMLR , 2021

    2021

  6. [15]

    Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, J \'e r \^o me Dubois, Cl \'e ment Gillard, and Henrich Lauko. From S pot 2.0 to S pot 2.10: What's new? In Proceed...

    2022

  7. [16]

    Spot’s temporal logic formulas, 2024

    Alexandre Duret-Lutz. Spot’s temporal logic formulas, 2024. Accessed: 02-01-2025

    2024

  8. [17]

    Dwyer, George S

    Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Property specification patterns for finite-state verification. In FMSP , pages 7--15. ACM , 1998

    1998

  9. [18]

    A randomized protocol for signing contracts

    Shimon Even, Oded Goldreich, and Abraham Lempel. A randomized protocol for signing contracts. Commun. ACM , 28(6):637--647, 1985

    1985

  10. [19]

    Analytic Combinatorics

    Philippe Flajolet and Robert Sedgewick. Analytic Combinatorics . Cambridge University Press, 2009

    2009

  11. [20]

    NL2LTL - a python package for converting natural language (NL) instructions to linear temporal logic (LTL) formulas

    Francesco Fuggitti and Tathagata Chakraborti. NL2LTL - a python package for converting natural language (NL) instructions to linear temporal logic (LTL) formulas. In AAAI , pages 16428--16430. AAAI Press, 2023

    2023

  12. [21]

    Mark Gold

    E. Mark Gold. Complexity of automaton identification from given data. Inf. Control. , 37(3):302--320, 1978

    1978

  13. [22]

    Pappas, and Insup Lee

    Mohammadhosein Hasanbeig, Yiannis Kantaros, Alessandro Abate, Daniel Kroening, George J. Pappas, and Insup Lee. Reinforcement learning for temporal logic control synthesis with probabilistic satisfaction guarantees. In 58th IEEE Conference on Decision and Control, CDC 2019, Ni...

    2019

  14. [23]

    Kemeny, J

    J. Kemeny, J. Snell, and A. Knapp. Denumerable M arkov Chains . Springer-Verlag, 2nd edition, 1976

    1976

  15. [24]

    Kwiatkowska, Gethin Norman, and David Parker

    Marta Z. Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of probabilistic real-time systems. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Pro...

    2011

  16. [25]

    Reinforcement learning with temporal logic rewards

    Xiao Li, Cristian Ioan Vasile, and Calin Belta. Reinforcement learning with temporal logic rewards. In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2017, Vancouver, BC, Canada, September 24-28, 2017 , pages 3834--3839. IEEE , 2017

    2017

  17. [26]

    Bridging ltlf inference to GNN inference for learning ltlf formulae

    Weilin Luo, Pingjia Liang, Jianfeng Du, Hai Wan, Bo Peng, and Delong Zhang. Bridging ltlf inference to GNN inference for learning ltlf formulae. In AAAI , pages 9849--9857. AAAI Press, 2022

    2022

  18. [27]

    Explainable reinforcement learning: A survey and comparative review

    Stephanie Milani, Nicholay Topin, Manuela Veloso, and Fei Fang. Explainable reinforcement learning: A survey and comparative review. ACM Comput. Surv. , 56(7):168:1--168:36, 2024

    2024

  19. [28]

    Deshmukh, Aniruddh Gopinath Puranic, Marcell Vazquez - Chanlatte, and Alexandre Donz \' e

    Sara Mohammadinejad, Jyotirmoy V. Deshmukh, Aniruddh Gopinath Puranic, Marcell Vazquez - Chanlatte, and Alexandre Donz \' e . Interpretable classification of time-series data using efficient enumerative techniques. In HSCC '20: 23rd ACM International Conference on Hybrid Syste...

    2020

  20. [29]

    Learning linear temporal properties

    Daniel Neider and Ivan Gavran. Learning linear temporal properties. In Nikolaj S. Bj rner and Arie Gurfinkel, editors, 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018 , pages 1--10. IEEE , 2018

    2018

  21. [30]

    What is formal verification without specifications? A survey on mining LTL specifications

    Daniel Neider and Rajarshi Roy. What is formal verification without specifications? A survey on mining LTL specifications. In Principles of Verification (3) , volume 15262 of Lecture Notes in Computer Science , pages 109--125. Springer, 2025

    2025

  22. [31]

    A robust genetic algorithm for learning temporal specifications from data

    Laura Nenzi, Simone Silvetti, Ezio Bartocci, and Luca Bortolussi. A robust genetic algorithm for learning temporal specifications from data. In QEST , volume 11024 of Lecture Notes in Computer Science , pages 323--338. Springer, 2018

    2018

  23. [32]

    Norman and V

    G. Norman and V. Shmatikov. Analysis of probabilistic contract signing. Journal of Computer Security , 14(6):561--589, 2006

    2006

  24. [33]

    The temporal logic of programs

    Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977 , pages 46--57. IEEE Computer Society, 1977

    1977

  25. [34]

    Sat-based learning of computation tree logic

    Adrien Pommellet, Daniel Stan, and Simon Scatton. Sat-based learning of computation tree logic. In Christoph Benzm \" u ller, Marijn J. H. Heule, and Renate A. Schmidt, editors, Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 202...

    2024

  26. [35]

    Scalable anytime algorithms for learning fragments of linear temporal logic

    Ritam Raha, Rajarshi Roy, Nathana \"e l Fijalkow, and Daniel Neider. Scalable anytime algorithms for learning fragments of linear temporal logic. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems , pages 263--280, Cham,...

    2022

  27. [36]

    Learning interpretable models in the property specification language

    Rajarshi Roy, Dana Fisman, and Daniel Neider. Learning interpretable models in the property specification language. In IJCAI , pages 2213--2219. ijcai.org, 2020

    2020

  28. [37]

    Learning interpretable temporal properties from positive examples only

    Rajarshi Roy, Jean - Rapha \" e l Gaglione, Nasim Baharisangari, Daniel Neider, Zhe Xu, and Ufuk Topcu. Learning interpretable temporal properties from positive examples only. CoRR , abs/2209.02650, 2022

    2022 arXiv

  29. [38]

    Specification: The biggest bottleneck in formal methods and autonomy

    Kristin Yvonne Rozier. Specification: The biggest bottleneck in formal methods and autonomy. In VSTTE , volume 9971 of Lecture Notes in Computer Science , pages 8--26, 2016

    2016

  30. [39]

    Sample efficient model-free reinforcement learning from LTL specifications with optimality guarantees

    Daqian Shao and Marta Kwiatkowska. Sample efficient model-free reinforcement learning from LTL specifications with optimality guarantees. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SA...

    2023

  31. [40]

    Generation of policy-level explanations for reinforcement learning

    Nicholay Topin and Manuela Veloso. Generation of policy-level explanations for reinforcement learning. In AAAI , pages 2514--2521. AAAI Press, 2019

    2019

  32. [41]

    Ltl learning on gpus

    Mojtaba Valizadeh, Nathana \"e l Fijalkow, and Martin Berger. Ltl learning on gpus. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification , pages 209--231, Cham, 2024. Springer Nature Switzerland

    2024

  33. [42]

    M. Vardi. Automatic verification of probabilistic concurrent finite state programs. In Proc. 26th Annual Symposium on Foundations of Computer Science (FOCS'85) , pages 327--338. IEEE Computer Society Press, 1985

    1985

  34. [43]

    End-to-end learning of ltlf formulae by faithful ltlf encoding

    Hai Wan, Pingjia Liang, Jianfeng Du, Weilin Luo, Rongzhen Ye, and Bo Peng. End-to-end learning of ltlf formulae by faithful ltlf encoding. In AAAI , pages 9071--9079. AAAI Press, 2024

    2024

  35. [44]

    write newline

    " write newline "" before.all 'output.state := FUNCTION fin.entry add.period write newline FUNCTION new.block output.state before.all = 'skip after.block 'output.state := if FUNCTION new.sentence output.state after.block = 'skip output.state before.all = 'skip after.sentence '...

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.