Pith. sign in

REVIEW 2 major objections 7 minor 83 references

What is Formal Verification without Specifications? A Survey on mining LTL Specifications

T0 review · 2 major / 7 minor · reviewed 2026-08-10 · deepseek-v4-flash

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

Pith's one-line read This survey organizes recent algorithms for mining Linear Temporal Logic specifications from example behaviors into three families — constraint-based, enumeration-based, and neural-network-based — and compares the guarantees each family…

desk verdict Useful, readable survey of LTL specification mining, but the comparative table under-specifies trace semantics and the work is already a published book chapter. read the letter →

arxiv 2501.16274 v1 pith:ZGBEGSKO submitted 2025-01-27 cs.FL cs.AIcs.LO

Daniel Neider , Rajarshi Roy This is my paper · ORCID
classification cs.FLcs.AIcs.LO
keywords lineartemporallogicspecificationminingpassivelearningformalverificationconstraint-basedsearchenumeration-basedgraphneuralnetworkssurvey
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

Formal verification depends on formal specifications, but writing them by hand is widely seen as a bottleneck. This survey examines recent work that instead learns specifications automatically, expressed in Linear Temporal Logic (LTL), from examples of desired and undesired system behavior. It tries to establish that these efforts are usefully organized by their search strategy: constraint-based methods that encode the learning problem for off-the-shelf solvers, enumeration-based methods that search the space of formulas directly, and neural-network-based methods that trade formal guarantees for scalability. For a practitioner, the survey's value is a comparison of what each approach can promise — soundness, completeness, minimality, and tolerance for noisy or positive-only data — so the choice of method can be matched to the available examples and required assurance.

What carries the argument

The load-bearing object is the syntax directed acyclic graph (syntax DAG) of an LTL formula, which represents shared subformulas so that formula size equals node count. Constraint-based methods use the DAG as the template for SAT/MaxSAT/MILP encodings; enumeration-based methods use partial DAGs and rewrite rules to prune equivalent formulas; neural methods encode words as linear graphs over which graph neural networks propagate satisfaction information of candidate subformulas. The passive-learning definition, with its minimality requirement, is the common yardstick that makes the three families comparable.

What would settle it

Run the surveyed tools on a shared benchmark of labeled traces and compare each result with its Table 1 guarantee; a single counterexample sample on which a sound-and-complete tool returns a non-minimal or inconsistent formula would falsify the comparison, and a published LTL-mining approach that fits none of the three search families would falsify the taxonomy's completeness.

Watch

Extended reading notes

Core claim

On the survey's own terms, the central discovery is that the passive learning problem — given a sample $S=(P,N)$ of positive and negative words, compute a minimal LTL formula consistent with $S$ — admits three methodological families with distinct trade-offs. Constraint-based approaches encode the syntax of candidate formulas as a syntax DAG and their semantics as bounded-model-checking-style constraints, then call SAT, MaxSAT, MILP, or ASP solvers; under perfect positive/negative data, several of them return sound, complete, and minimal formulas. Enumeration-based approaches search the formula space directly, using dynamic programming, rewrite-rule pruning, or GPU acceleration; individual tools range from sound-only anytime algorithms to a sound, complete, and minimal enumerator, and the family overall trades worst-case minimality for scalability. Neural-network approaches, built on the insight that a word can be viewed as a linear graph, learn via graph neural networks and offer no formal consistency guarantees but are aimed at large noisy datasets. The comparison table condenses the surveyed works into columns for LTL fragment, classification of positive and negative examples, input data, and guarantees, grounding the survey's three-way categorization.

Load-bearing premise

The survey's conclusions rest on the works in Table 1 being a representative selection of the field and on those works' self-reported guarantees being accurate, since the paper neither explains a systematic search process nor re-runs the tools.

Editorial extensions

If this is right

  • A practitioner can use Table 1 to match a miner to the data: perfect labeled data admits several sound, complete, and minimal methods, while noisy or positive-only data forces a choice among relaxed, enumerative, or neural approaches with weaker guarantees.
  • For noisy data, the survey indicates the practical options are MaxSAT-style relaxation in the constraint-based family, enumeration heuristics, or neural networks, with formal guarantees weakening or disappearing in that order.
  • Enumeration-based and GPU-accelerated approaches are presented as the scalable end of the spectrum, positioning them as the practical choice when formula minimality matters less than throughput.
  • Neural-network approaches currently provide no consistency guarantees, but the survey suggests that faithful encodings of LTL semantics into the network architecture can at least guarantee that a formula can be extracted from the trained model.
  • Template-based mining, natural-language-to-LTL translation, and learning in logics beyond LTL (STL, CTL, ATL, MTL, PSL) are adjacent settings that the passive-learning taxonomy does not directly cover but that share the specification bottleneck.

Reading between the lines

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

  • A natural next step the survey leaves implicit is to combine the families, for instance using a neural network to propose candidate formulas that a constraint-based verifier then checks or minimizes, since one family's weakness is another's strength.
  • The positive-only line of work suggests a testable extension: if 'strongness' is formalized as the right optimization criterion, one-class specification miners could be applied to reward-function learning in reinforcement learning, where negative demonstrations are often unavailable.
  • Because the survey does not propose a common benchmark, an immediate consequence a reader might draw is that the field's next bottleneck is empirical: a shared corpus of labeled traces would let the guarantee claims in Table 1 be tested head-to-head.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

2 major / 7 minor

Summary. This paper is a survey of passive learning of Linear Temporal Logic specifications from examples of system behavior. It organizes recent work into three families — constraint-based (SAT/SMT/MaxSAT/ASP), enumeration-based, and neural-network-based — and compares eleven selected works in Table 1 on the dimensions of technique, LTL fragment, input data (positive/negative, perfect/noisy), and theoretical guarantees (soundness, completeness, minimality). The paper also covers extensions: learning from noisy data, positive-only data, template-based mining, translation from natural language, and other temporal logics (STL, CTL, MTL, PSL). The intended contribution is an accessible map of the area for formal methods practitioners.

Significance. The survey fills a useful gap: the LTL specification mining literature is growing quickly and lacks a single entry point. The three-way taxonomy is sensible, and the background in Section 2 is standard. The paper is particularly helpful in explaining the syntax-DAG representation and the folk theorem that minimality is what makes the learning problem non-trivial. The table and accompanying narrative, once corrected for trace semantics, would let practitioners identify which tool families fit their input format and guarantee needs. Since this is a survey, there are no machine-checked proofs or benchmarks to credit, but the presentation is generally clear and the referencing is broad. The main value is organizational, and that value depends on the comparability of Table 1's rows.

major comments (2)
  1. [§2.2 / Definition 1 / Table 1] The paper never fixes the trace semantics for the learning problem. Definition 1 leaves the word domain implicit, and Section 2.2 presents both infinite-word and finite-word semantics without saying which one applies to the rest of the paper. This matters because the guarantees listed in Table 1 — soundness, completeness, minimality — are semantics-relative: a formula that is minimal for LTLf over finite traces need not be minimal for full LTL over infinite words, and consistency on finite examples does not constrain behavior on infinite suffixes. The problem is visible in Table 1 itself: Luo et al. [56] and Wan et al. [81] are listed under "full LTL", but the titles of the cited papers state they learn LTLf formulas (LTL over finite traces). The authors should add a semantics dimension (e.g., LTL over infinite words vs. LTLf) to Table 1, correct the fragment labels, and explain how "minimal" is defined for each row.
  2. [§3, §8, Table 1] The survey claims in the abstract and conclusion to "list and compare recent advances" and to provide a "comprehensive overview", but it gives no search protocol, inclusion/exclusion criteria, or time window for selecting the eleven works in Table 1. Without such criteria the reader cannot determine whether the three-way taxonomy and the qualitative conclusions are representative of the field or merely reflect a convenience sample. At a minimum, the paper should state its selection criteria and scope; alternatively, it should soften the comprehensiveness claim to one about a representative subset.
minor comments (7)
  1. [§6] The sentence "it suffers from the limitation that the extracted LTL formula might accurately capture the behavior of the trained GNN" should read "might not accurately capture"; as written it asserts a non-limitation.
  2. [§2.1] In the definition of w[i:], "the suffix starting from the starting from position i" contains a duplicated phrase.
  3. [§4.2] The phrase "the authors solve formulate a learning task" contains a typo; it should be "the authors formulate a learning task".
  4. [§4.1] The word "potenitally" is misspelled in the last sentence of Section 4.1.
  5. [§4] Z3 is an SMT solver, not specifically a SAT solver; the text should say "SAT/SMT solver" or "SMT solver" when referring to it.
  6. [§2.2] The finite-word Until clause is typeset as "i≤ j≤| w− 1|"; the bars around w are misplaced and should read "i ≤ j ≤ |w| − 1".
  7. [References] References [13] and [14] are the same paper (Bombara et al., HSCC 2016) and appear twice with identical bibliographic data; one duplicate should be removed.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: this is a survey that organizes independent published results; its taxonomy and Table 1 report, rather than derive, the compared methods' claims.

full rationale

The paper contains no derivation chain of the kind that can be circular: it does not fit parameters to data and then predict those same data, define one quantity in terms of another, or invoke a self-authored uniqueness theorem to force a conclusion. Its central contribution is a three-way taxonomy of existing LTL-mining approaches (constraint-based, enumeration-based, neural-network-based) and Table 1, which compares published methods on technique, fragment, classification setting, input data, and reported guarantees. These entries are taken from the cited primary papers, including several by the authors (Neider-Gavran, Raha et al., Gaglione et al., Roy et al.); however, a survey citing the original papers it summarizes is not circular, and the self-citations are transparent pointers rather than load-bearing justifications of the taxonomy. The comparison's reliance on each cited paper's self-reported guarantees, and the possible ambiguity between finite- and infinite-trace LTL semantics in Table 1, are correctness or comparability concerns about how the survey is framed, not reductions of the survey's claims to its own inputs. No equation in the paper equates an output with an input by construction, and no fitted value is relabeled as a prediction. The absence of a derivation chain means the usual circularity failure mode does not apply.

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

The survey introduces no free parameters, postulates no new entities, and makes no quantitative predictions. Its epistemic commitments are the standard definition of LTL, the passive learning problem statement, and the accuracy of the cited literature.

assumptions (3)
  • standard math The standard LTL semantics over finite words is obtained by the modified clauses for X and U given in Section 2.2.
    The survey's framing of passive learning relies on this finite-trace semantics, which it attributes to the line of work starting with De Giacomo and Vardi [38].
  • domain assumption The descriptions in Table 1 and Sections 4-6 accurately reflect the capabilities and guarantees of the cited tools.
    The survey performs no experiments or reimplementations; its comparison rests on trusting the cited papers' reported properties.
  • domain assumption The passive learning problem in Definition 1, with minimal formula size as the optimization objective, is the right abstraction of the specification mining bottleneck.
    The survey narrows the field to passive learning from labeled traces and uses minimality as the organizing objective; other settings, such as active learning or query-based learning, are out of scope by this choice.

how reviews work

0 comments
Cite this review

Pith. "Pith review of What is Formal Verification without Specifications? A Survey on mining LTL Specifications." pith.science (2026). https://pith.science/paper/ZGBEGSKO

@misc{pith2026250116274,
  author       = {Pith},
  title        = {Pith review of: What is Formal Verification without Specifications? A Survey on mining LTL Specifications},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ZGBEGSKO}},
  note         = {Machine review of arXiv:2501.16274}
}
read the original abstract

Virtually all verification techniques using formal methods rely on the availability of a formal specification, which describes the design requirements precisely. However, formulating specifications remains a manual task that is notoriously challenging and error-prone. To address this bottleneck in formal verification, recent research has thus focussed on automatically generating specifications for formal verification from examples of (desired and undesired) system behavior. In this survey, we list and compare recent advances in mining specifications in Linear Temporal Logic (LTL), the de facto standard specification language for reactive systems. Several approaches have been designed for learning LTL formulas, which address different aspects and settings of specification design. Moreover, the approaches rely on a diverse range of techniques such as constraint solving, neural network training, enumerative search, etc. We survey the current state-of-the-art techniques and compare them for the convenience of the formal methods practitioners.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

83 extracted references · 49 canonical work pages

  1. [61]

    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 Systems: Computation and Control, Sydney, New South Wales, Australia, April 21-24, 20...

    arXiv 2020

  2. [56]

    Lang2ltl: Translating natural language commands to temporal robot task specification

    Jason Xinyu Liu, Ziyi Yang, Ifrah Idrees, Sam Liang, Benjamin Schornstein, Stefanie Tellex, and Ankit Shah. Lang2ltl: Translating natural language commands to temporal robot task specification. CoRR , abs/2302.11649, 2023. URL: https://doi.org/10.48550/arXiv.2302.11649, https://arxiv.org/abs/2302.11649 arXiv:2302.11649 , https://doi.org/10.48550/ARXIV.230...

    arXiv doi:10.48550/arxiv.2302.11649 2023

  3. [81]

    Eric Verhulst and Gjalt G. de Jong. Opencomrtos: An ultra-small network centric embedded RTOS designed using formal modeling. In SDL Forum , volume 4745 of Lecture Notes in Computer Science , pages 258--271. Springer, 2007

    work page 2007

  4. [1]

    , " * write output.state after.block = add.period write

    ENTRY address author booktitle chapter doi edition editor eid howpublished institution journal key month note number organization pages publisher school series title type url volume year label INTEGERS output.state before.all mid.sentence after.sentence after.block FUNCTION init.state.consts #0 'before.all := #1 'mid.sentence := #2 'after.sentence := #3 '...

  5. [2]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION word.in bbl.in capitalize ":" * " " *...

  6. [3]

    Rajeev Alur, Rastislav Bod \' k, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar - Lezama, Emina Torlak, and Abhishek Udupa. Syntax-guided synthesis. In Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013 , pages 1--8. IEEE , 2013. URL: https://ieeexplore.ieee.or...

    arXiv 2013

  7. [4]

    Glenn Ammons, Rastislav Bod \' k, and James R. Larus. Mining specifications. In John Launchbury and John C. Mitchell, editors, Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, OR, USA, January 16-18, 2002 , pages 4--16. ACM , 2002. https://doi.org/10.1145/503272.503275 doi:10.1145/503272.503275

    arXiv 2002

  8. [5]

    Fareed Arif, Daniel Larraz, Mitziu Echeverria, Andrew Reynolds, Omar Chowdhury, and Cesare Tinelli

    M. Fareed Arif, Daniel Larraz, Mitziu Echeverria, Andrew Reynolds, Omar Chowdhury, and Cesare Tinelli. SYSLITE: syntax-guided synthesis of PLTL formulas from finite traces. In FMCAD , pages 93--103. IEEE , 2020

    2020

Show all 83 references
  1. [6]

    Parametric identification of temporal properties

    Eugene Asarin, Alexandre Donz\' e , Oded Maler, and Dejan Nickovic. Parametric identification of temporal properties. In Proceedings of the Second International Conference on Runtime Verification , RV'11, page 147–160, Berlin, Heidelberg, 2011. Springer-Verlag. https://doi.org...

    2011 doi

  2. [7]

    A story about formal methods adoption by a railway signaling manufacturer

    Stefano Bacherini, Alessandro Fantechi, Matteo Tempestini, and Niccol \` o Zingoni. A story about formal methods adoption by a railway signaling manufacturer. In FM , volume 4085 of Lecture Notes in Computer Science , pages 179--189. Springer, 2006

    2006

  3. [8]

    Using B as a high level programming language in an industrial project: Roissy VAL

    Fr \' e d \' e ric Badeau and Arnaud Amelot. Using B as a high level programming language in an industrial project: Roissy VAL . In ZB , volume 3455 of Lecture Notes in Computer Science , pages 334--354. Springer, 2005

    2005

  4. [9]

    Principles of model checking

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

    2008

  5. [10]

    Barrett, Christopher L

    Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4 . In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT...

    2011 doi

  6. [11]

    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. URL: https://doi.org/10.1016/j.ic.2022.104957, https://doi.org/10.1016/J.IC.2022.104957 doi:10.1016/J.IC.2022.104957

    2022

  7. [12]

    Picosat essentials

    Armin Biere. Picosat essentials. J. Satisf. Boolean Model. Comput. , 4(2-4):75--97, 2008. URL: https://doi.org/10.3233/sat190039, https://doi.org/10.3233/SAT190039 doi:10.3233/SAT190039

    2008 doi

  8. [13]

    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

  9. [14]

    Bj rner and Anh - Dung Phan

    Nikolaj S. Bj rner and Anh - Dung Phan. \( \) z - maximal satisfaction with Z3 . In Temur Kutsia and Andrei Voronkov, editors, 6th International Symposium on Symbolic Computation in Software Science, SCSS 2014, Gammarth, La Marsa, Tunisia, December 7-8, 2014 , volume 30 of EPi...

    2014 doi

  10. [16]

    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,...

    2016

  11. [17]

    The complexity of learning temporal properties

    Benjamin Bordais, Daniel Neider, and Rajarshi Roy. The complexity of learning temporal properties. CoRR , abs/2408.04486, 2024. URL: https://doi.org/10.48550/arXiv.2408.04486, https://arxiv.org/abs/2408.04486 arXiv:2408.04486 , https://doi.org/10.48550/ARXIV.2408.04486 doi:10....

    2024 doi arXiv

  12. [18]

    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, ...

    2024 doi

  13. [19]

    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 - Augu...

    2020

  14. [20]

    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 doi

  15. [21]

    McIlraith

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

    2019

  16. [22]

    Temporal-logic queries

    William Chan. Temporal-logic queries. In CAV , volume 1855 of Lecture Notes in Computer Science , pages 450--463. Springer, 2000

    2000

  17. [23]

    Towards explainable formal methods: From LTL to natural language with neural machine translation

    Himaja Cherukuri, Alessio Ferrari, and Paola Spoletini. Towards explainable formal methods: From LTL to natural language with neural machine translation. In Vincenzo Gervasi and Andreas Vogelsang, editors, Requirements Engineering: Foundation for Software Quality - 28th Intern...

    2022 doi

  18. [24]

    Learning temporal logic formulas from suboptimal demonstrations: theory and experiments

    Glen Chou, Necmiye Ozay, and Dmitry Berenson. Learning temporal logic formulas from suboptimal demonstrations: theory and experiments. Auton. Robots , 46(1):149--174, 2022. URL: https://doi.org/10.1007/s10514-021-10004-x, https://doi.org/10.1007/S10514-021-10004-X doi:10.1007/...

    2022 doi

  19. [25]

    Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu

    Edmund M. Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu. Bounded model checking using satisfiability solving. Formal Methods Syst. Des. , 19(1):7--34, 2001. https://doi.org/10.1023/A:1011276507260 doi:10.1023/A:1011276507260

    2001 doi

  20. [26]

    Cofer and Steven P

    Darren D. Cofer and Steven P. Miller. DO-333 certification case studies. In NASA Formal Methods , volume 8430 of Lecture Notes in Computer Science , pages 1--15. Springer, 2014

    2014

  21. [27]

    nl2spec: Interactively translating unstructured natural language to temporal logics with large language models

    Matthias Cosler, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, and Caroline Trippel. nl2spec: Interactively translating unstructured natural language to temporal logics with large language models. In Constantin Enea and Akash Lal, editors, Computer Aided Verification - 3...

    2023 doi

  22. [28]

    Leonardo Mendon c a de Moura and Nikolaj S. Bj rner. Z3: an efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Co...

    2008 doi

  23. [29]

    Dwyer, George S

    Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Property specification patterns for finite-state verification. In Mark A. Ardis and Joanne M. Atlee, editors, Proceedings of the Second Workshop on Formal Methods in Software Practice, March 4-5, 1998, Clearwater Beach...

    1998

  24. [30]

    Fecko, M

    Mariusz A. Fecko, M. \" U mit Uyar, Paul D. Amer, Adarshpal S. Sethi, Theodore Dzik, R. Menell, and Michael McMahon. A success story of formal description techniques: Estelle specification and test generation for MIL-STD 188-220. Comput. Commun. , 23(12):1196--1213, 2000

    2000

  25. [31]

    The complexity of learning linear temporal formulas from examples

    Nathana \" e l Fijalkow and Guillaume Lagarde. The complexity of learning linear temporal formulas from examples. In ICGI , volume 153 of Proceedings of Machine Learning Research , pages 237--250. PMLR , 2021

    2021

  26. [32]

    Ltlmop: Experimenting with language, temporal logic and robot control

    Cameron Finucane, Gangyuan Jing, and Hadas Kress - Gazit. Ltlmop: Experimenting with language, temporal logic and robot control. In 2010 IEEE/RSJ International Conference on Intelligent Robots and Systems, October 18-22, 2010, Taipei, Taiwan , pages 1988--1993. IEEE , 2010. ht...

    2010

  27. [33]

    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 Proceedings of the Thirty-Seventh AAAI Conference on Artificial Intelligence and Thirty-Fifth Conference on Inn...

    2023 doi

  28. [34]

    Learning linear temporal properties from noisy data: A maxsat-based approach

    Jean - Rapha \" e l Gaglione, Daniel Neider, Rajarshi Roy, Ufuk Topcu, and Zhe Xu. Learning linear temporal properties from noisy data: A maxsat-based approach. In Zhe Hou and Vijay Ganesh, editors, Automated Technology for Verification and Analysis - 19th International Sympos...

    2021 doi

  29. [35]

    Model checking at scale: Automated air traffic control design space exploration

    Marco Gario, Alessandro Cimatti, Cristian Mattarei, Stefano Tonetta, and Kristin Yvonne Rozier. Model checking at scale: Automated air traffic control design space exploration. In CAV (2) , volume 9780 of Lecture Notes in Computer Science , pages 3--22. Springer, 2016

    2016

  30. [36]

    Answer Set Solving in Practice

    Martin Gebser, Roland Kaminski, Benjamin Kaufmann, and Torsten Schaub. Answer Set Solving in Practice . Synthesis Lectures on Artificial Intelligence and Machine Learning. Morgan & Claypool Publishers, 2012. https://doi.org/10.2200/S00457ED1V01Y201211AIM019 doi:10.2200/S00457E...

    2012 doi

  31. [37]

    Classical negation in logic programs and disjunctive databases

    Michael Gelfond and Vladimir Lifschitz. Classical negation in logic programs and disjunctive databases. New Gener. Comput. , 9(3/4):365--386, 1991. https://doi.org/10.1007/BF03037169 doi:10.1007/BF03037169

    1991 doi

  32. [38]

    Learning linear temporal properties for autonomous robotic systems

    Enrico Ghiorzi, Michele Colledanchise, Gianluca Piquet, Stefano Bernagozzi, Armando Tacchella, and Lorenzo Natale. Learning linear temporal properties for autonomous robotic systems. IEEE Robotics Autom. Lett. , 8(5):2930--2937, 2023. https://doi.org/10.1109/LRA.2023.3263368 d...

    2023

  33. [39]

    ARSENAL: automatic requirements specification extraction from natural language

    Shalini Ghosh, Daniel Elenius, Wenchao Li, Patrick Lincoln, Natarajan Shankar, and Wilfried Steiner. ARSENAL: automatic requirements specification extraction from natural language. In NASA Formal Methods, NFM , 2016. https://doi.org/10.1007/978-3-319-40648-0\_4 doi:10.1007/978...

    2016 doi

  34. [40]

    Giuseppe De Giacomo and Moshe Y. Vardi. Linear temporal logic and linear dynamic logic on finite traces. In Francesca Rossi, editor, IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013 , pages 854--860...

    2013

  35. [41]

    Formal requirements elicitation with FRET

    Dimitra Giannakopoulou, Thomas Pressburger, Anastasia Mavridou, Julian Rhein, Johann Schumann, and Nija Shi. Formal requirements elicitation with FRET . In International Conference on Requirements Engineering: Foundation for Software Quality, REFSQ , 2020. URL: http://ceur-ws....

    2020

  36. [42]

    Little tricky logic: Misconceptions in the understanding of LTL

    Ben Greenman, Sam Saarinen, Tim Nelson, and Shriram Krishnamurthi. Little tricky logic: Misconceptions in the understanding of LTL . Art Sci. Eng. Program. , 7(2), 2023

    2023

  37. [43]

    Kreber, Markus Norman Rabe, and Bernd Finkbeiner

    Christopher Hahn, Frederik Schmitt, Jens U. Kreber, Markus Norman Rabe, and Bernd Finkbeiner. Teaching temporal logics to neural networks. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021 . OpenReview.net, 2021. URL:...

    2021

  38. [44]

    Hamilton, Rex Ying, and Jure Leskovec

    William L. Hamilton, Rex Ying, and Jure Leskovec. Representation learning on graphs: Methods and applications. IEEE Data Eng. Bull. , 40(3):52--74, 2017. URL: http://sites.computer.org/debull/A17sept/p52.pdf

    2017

  39. [45]

    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

  40. [46]

    Holzmann

    Gerard J. Holzmann. The logic of bugs. In SIGSOFT FSE , pages 81--87. ACM , 2002

    2002

  41. [47]

    Towards ilp-based ltlf passive learning

    Antonio Ielo, Mark Law, Valeria Fionda, Francesco Ricca, Giuseppe De Giacomo, and Alessandra Russo. Towards ilp-based ltlf passive learning. In Inductive Logic Programming: 32nd International Conference, ILP 2023, Bari, Italy, November 13–15, 2023, Proceedings , page 30–45, Be...

    2023 doi

  42. [48]

    Bayesian inference of linear temporal logic specifications for contrastive explanations

    Joseph Kim, Christian Muise, Ankit Shah, Shubham Agarwal, and Julie Shah. Bayesian inference of linear temporal logic specifications for contrastive explanations. In IJCAI , pages 5591--5598. ijcai.org, 2019

    2019

  43. [49]

    sel4: formal verification of an operating-system kernel

    Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. sel4: formal verification of an operating-system kernel. Commun. ACM , ...

    2010

  44. [50]

    Temporal logics for learning and detection of anomalous behavior

    Zhaodan Kong, Austin Jones, and Calin Belta. Temporal logics for learning and detection of anomalous behavior. IEEE Transactions on Automatic Control , 62(3):1210--1222, 2017. https://doi.org/10.1109/TAC.2016.2585083 doi:10.1109/TAC.2016.2585083

    2017

  45. [51]

    Temporal logic inference for classification and prediction from data

    Zhaodan Kong, Austin Jones, Ana Medina Ayala, Ebru Aydin Gol, and Calin Belta. Temporal logic inference for classification and prediction from data. In Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control , HSCC '14, page 273–282, New Yor...

    2014

  46. [52]

    Fainekos, and George J

    Hadas Kress - Gazit, Georgios E. Fainekos, and George J. Pappas. Translating structured english to robot controllers. Advanced Robotics , 22(12):1343--1359, 2008

    2008

  47. [53]

    Investigating program behavior using the texada LTL specifications miner

    Caroline Lemieux and Ivan Beschastnikh. Investigating program behavior using the texada LTL specifications miner. In Myra B. Cohen, Lars Grunske, and Michael Whalen, editors, 30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015, Lincoln, NE, USA, ...

    2015 doi

  48. [54]

    Wenchao Li, Lili Dworkin, and Sanjit A. Seshia. Mining assumptions for synthesis. In MEMOCODE , pages 43--50. IEEE , 2011

    2011

  49. [55]

    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. https://doi...

    2017

  50. [57]

    Breaking and fixing the needham-schroeder public-key protocol using FDR

    Gavin Lowe. Breaking and fixing the needham-schroeder public-key protocol using FDR . Softw. Concepts Tools , 17(3):93--102, 1996

    1996

  51. [58]

    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

  52. [59]

    Specification sketching for linear temporal logic

    Simon Lutz, Daniel Neider, and Rajarshi Roy. Specification sketching for linear temporal logic. In \' E tienne Andr \' e and Jun Sun, editors, Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Singapore, October 24-27, 2023, Proceedi...

    2023 doi

  53. [60]

    Learning temporal formulas from examples is hard

    Corto Mascle, Nathana \" e l Fijalkow, and Guillaume Lagarde. Learning temporal formulas from examples is hard. CoRR , abs/2312.16336, 2023. URL: https://doi.org/10.48550/arXiv.2312.16336, https://arxiv.org/abs/2312.16336 arXiv:2312.16336 , https://doi.org/10.48550/ARXIV.2312....

    2023 doi arXiv

  54. [62]

    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. https://doi.org/10.23919/...

    2018

  55. [63]

    What Is Formal Verification Without Specifications? A Survey on Mining LTL Specifications , pages 109--125

    Daniel Neider and Rajarshi Roy. What Is Formal Verification Without Specifications? A Survey on Mining LTL Specifications , pages 109--125. Springer Nature Switzerland, Cham, 2025. https://doi.org/10.1007/978-3-031-75778-5_6 doi:10.1007/978-3-031-75778-5_6

    2025 doi

  56. [64]

    Nemhauser and Laurence A

    George L. Nemhauser and Laurence A. Wolsey. Integer and Combinatorial Optimization . Wiley interscience series in discrete mathematics and optimization. Wiley, 1988. https://doi.org/10.1002/9781118627372 doi:10.1002/9781118627372

    1988 doi

  57. [65]

    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 Annabelle McIver and Andras Horvath, editors, Quantitative Evaluation of Systems , pages 323--338, Cham, 2018. Springer International...

    2018

  58. [66]

    Nikora and Galen Balcom

    Allen P. Nikora and Galen Balcom. Automated identification of LTL patterns in natural language requirements. In ISSRE 2009, 20th International Symposium on Software Reliability Engineering, Mysuru, Karnataka, India, 16-19 November 2009 , pages 185--194. IEEE Computer Society, ...

    2009 doi

  59. [67]

    Planning with state abstractions for non-markovian task specifications

    Yoonseon Oh, Roma Patel, Thao Nguyen, Baichuan Huang, Ellie Pavlick, and Stefanie Tellex. Planning with state abstractions for non-markovian task specifications. In Antonio Bicchi, Hadas Kress - Gazit, and Seth Hutchinson, editors, Robotics: Science and Systems XV, University ...

    2019 doi

  60. [68]

    Data-efficient learning of natural language to linear temporal logic translators for robot task specification

    Jiayi Pan, Glen Chou, and Dmitry Berenson. Data-efficient learning of natural language to linear temporal logic translators for robot task specification. In IEEE International Conference on Robotics and Automation, ICRA 2023, London, UK, May 29 - June 2, 2023 , pages 11554--11...

    2023

  61. [69]

    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. https://doi.org/10.1109/SFCS.1977.32 doi:10.1109/SFCS.1977.32

    1977 doi

  62. [70]

    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 doi

  63. [71]

    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

  64. [72]

    Scarlet: Scalable anytime algorithms for learning fragments of linear temporal logic

    Ritam Raha, Rajarshi Roy, Nathana \" e l Fijalkow, and Daniel Neider. Scarlet: Scalable anytime algorithms for learning fragments of linear temporal logic. J. Open Source Softw. , 9(93):5052, 2024. URL: https://doi.org/10.21105/joss.05052, https://doi.org/10.21105/JOSS.05052 d...

    2024 doi

  65. [73]

    P \' e rez

    Ritam Raha, Rajarshi Roy, Nathana \" e l Fijalkow, Daniel Neider, and Guillermo A. P \' e rez. Synthesizing efficiently monitorable formulas in metric temporal logic. In VMCAI (2) , volume 14500 of Lecture Notes in Computer Science , pages 264--288. Springer, 2024

    2024

  66. [74]

    Barrett, and Cesare Tinelli

    Andrew Reynolds, Haniel Barbosa, Andres N \" o tzli, Clark W. Barrett, and Cesare Tinelli. cvc4sy: Smart and fast term enumeration for syntax-guided synthesis. In Isil Dillig and Serdar Tasiran, editors, Computer Aided Verification - 31st International Conference, CAV 2019, Ne...

    2019 doi

  67. [75]

    Exact synthesis of LTL properties from traces

    Heinz Riener. Exact synthesis of LTL properties from traces. In FDL , pages 1--6. IEEE , 2019

    2019

  68. [76]

    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

  69. [77]

    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

  70. [78]

    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

  71. [79]

    Shah, and Shen Li

    Ankit Shah, Pritish Kamath, Julie A. Shah, and Shen Li. Bayesian inference of temporal task specifications from demonstrations. In NeurIPS , pages 3808--3817, 2018

    2018

  72. [80]

    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. URL: https://doi.org/10.1007/978-3-031-65633-0_10

    2024 doi

  73. [82]

    Andreas W \" a chter and Lorenz T. Biegler. On the implementation of an interior-point filter line-search algorithm for large-scale nonlinear programming. Math. Program. , 106(1):25--57, 2006. URL: https://doi.org/10.1007/s10107-004-0559-y, https://doi.org/10.1007/S10107-004-0...

    2006 doi

  74. [83]

    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

  75. [84]

    Mining temporal specifications from object usage

    Andrzej Wasylkowski and Andreas Zeller. Mining temporal specifications from object usage. Autom. Softw. Eng. , 18(3-4):263--292, 2011

    2011

Pith tools

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