pith. sign in

arxiv: 2503.15840 · v4 · submitted 2025-03-20 · 💻 cs.LO · cs.FL

Automatic Generation of Safety-compliant Linear Temporal Logic via Large Language Model: A Self-supervised Framework

Junle Li , Siqi Chen , Jiakai Li , Meiqi Tian , Bingzhuo Zhong This is my paper

Pith reviewed 2026-05-22 23:48 UTC · model grok-4.3

classification 💻 cs.LO cs.FL
keywords Linear Temporal LogicLarge Language ModelsSafety ComplianceFormal SpecificationsCyber-Physical SystemsCounterexample-guided RefinementSelf-supervised Framework
0
0 comments X

The pith

An LLM framework generates Linear Temporal Logic specifications that comply with safety restrictions by using language inclusion checks and counterexample-guided fixes.

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

The paper introduces AutoSafeLTL, a self-supervised approach that converts natural language task descriptions into Linear Temporal Logic formulas while enforcing compliance with a given set of safety restrictions for cyber-physical systems. It pairs large language models with formal language inclusion verification: an LLM aligns atomic propositions for semantic match, and another LLM interprets counterexamples from inclusion checks to refine the formulas. This targets the limitation that earlier translation methods ensured only linguistic fidelity, not safety. The reported result is a zero violation rate on the tested safety constraints while keeping the specifications logically consistent and semantically accurate.

Core claim

AutoSafeLTL integrates language inclusion checking with an LLM-as-an-Aligner for atomic proposition matching and an LLM-as-a-Critic for automated refinement from counterexamples, producing LTL specifications that satisfy all imposed safety restrictions at a 0% violation rate while preserving logical consistency and semantic accuracy.

What carries the argument

The AutoSafeLTL loop that feeds language inclusion counterexamples to an LLM critic for iterative LTL refinement.

If this is right

  • The generated LTL specifications achieve a 0% violation rate against the imposed safety restrictions.
  • Logical consistency and semantic accuracy are maintained through the refinement steps.
  • The method combines LLMs with formal verification to support automatic safety-aware specification generation for CPS.
  • The framework demonstrates synergy between AI generation and formal methods for verifiable controller synthesis.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same counterexample-driven refinement pattern could extend to other temporal logics or specification languages.
  • Integration into existing CPS design pipelines could reduce manual safety audits for generated controllers.
  • The approach may generalize to domains where natural language instructions must produce provably safe formal artifacts.

Load-bearing premise

The language inclusion checker detects every safety violation and the LLM produces refinements that fix the violation without creating new ones or changing the intended meaning.

What would settle it

A test set of natural language tasks whose initial LLM-generated LTL violates at least one safety restriction; after running the full refinement loop, inspect whether any output LTL still violates a restriction or no longer matches the original task semantics.

Figures

Figures reproduced from arXiv: 2503.15840 by Bingzhuo Zhong, Jiakai Li, Junle Li, Meiqi Tian, Siqi Chen.

Figure 1
Figure 1. Figure 1: Overview of AutoSafeLTL Framework, with detailed introduction in Section 3. 1.2 Contribution In this paper, we introduce AutoSafeLTL, a novel framework (as shown in [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Overview of Operator Matching in the Syntactic Check Now, we revisit the running example to demonstrate the syntactic check. Example 2. (continued): (Running example) Having the Base Rule in LTL-format, we extract the AP library as [right_turn, straight_500m,left_turn, straight_1km, arrive_destination]. Then, LLM-as-a-Aligner is invoked to com￾pare the LTL-formatted Desired Tasks with the AP Library. Accor… view at source ↗
Figure 3
Figure 3. Figure 3: Left: The Base Rule. Right: The Desired Task in LTL generated in the first round. (Both represented in BA format for illustrating the running example) Counterexample: Aut A (after light preprocessing): of Trans. 47, of States 11. Aut B (after light preprocessing): of Trans. 8, of States 3. Counterexample: !straight_200m Not included. Time used(ms): 38 [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
read the original abstract

Converting high-level tasks described by natural language into formal specifications like Linear Temporal Logic (LTL) is a key step towards providing formal safety guarantees over cyber-physical systems (CPS). While the compliance of the formal specifications themselves against the safety restrictions imposed on CPS is crucial for ensuring safety, most existing works only focus on translation consistency between natural languages and formal specifications. In this paper, we introduce AutoSafeLTL, a self-supervised framework that utilizes large language models (LLMs) to automate the generation of LTL specifications complying with a set of safety restrictions while preserving their logical consistency and semantic accuracy. As a key insight, our framework integrates Language Inclusion check with an automated counterexample-guided modification mechanism to ensure the safety-compliance of the resulting LTL specifications. In particular, we develop 1) an LLM-as-an-Aligner, which performs atomic proposition matching between generated LTL specifications and safety restrictions to enforce semantic alignment; and 2) an LLM-as-a-Critic, which automates LTL specification refinement by interpreting counterexamples derived from Language Inclusion checks. Experimental results demonstrate that our architecture effectively guarantees safety-compliance for the generated LTL specifications, achieving a 0% violation rate against imposed safety restrictions. This shows the potential of our work in synergizing AI and formal verification techniques, enhancing safety-aware specification generation and automatic verification for both AI and critical CPS applications.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

3 major / 2 minor

Summary. The paper introduces AutoSafeLTL, a self-supervised LLM-based framework for generating LTL specifications from natural language that comply with given safety restrictions. It combines an LLM-as-an-Aligner for semantic alignment of atomic propositions and an LLM-as-a-Critic that refines candidate formulas using counterexamples returned by a language-inclusion checker, with the central empirical claim that the resulting specifications achieve a 0% violation rate against the imposed restrictions while preserving logical consistency and semantic accuracy.

Significance. If the empirical safety claim is shown to be robust, the work would provide a practical bridge between natural-language task descriptions and formally verifiable LTL specifications for cyber-physical systems, extending prior translation-focused methods by incorporating an automated counterexample-guided safety loop. The explicit use of language inclusion as an external oracle is a clear methodological strength.

major comments (3)
  1. [§3.2] §3.2 (LLM-as-a-Critic): No formal argument or error-bound analysis is supplied showing that an LLM interpretation of a counterexample (which may be an infinite word or Büchi-automaton path) necessarily produces a modification that (a) removes the detected violation, (b) preserves satisfiability and logical consistency, and (c) introduces no new violations. The 0% violation claim therefore rests entirely on the unverified behavior of the LLM step.
  2. [§4] §4 (Experimental evaluation): The abstract and experimental section report a 0% violation rate but supply no information on test-set cardinality, the provenance or selection procedure of the safety restrictions, the concrete definition of “violation,” or any baseline comparison against direct LLM generation or existing LTL translators. These omissions make it impossible to determine whether the result is load-bearing or an artifact of the chosen instances.
  3. [§3.1] §3.1 (Language Inclusion integration): The framework treats the external inclusion checker as an infallible oracle whose counterexamples are always correctly parsed by the LLM; no discussion is given of the PSPACE-completeness of LTL inclusion or of the possibility that an LLM mis-step silently re-introduces a safety violation.
minor comments (2)
  1. The repeated full phrases “LLM-as-an-Aligner” and “LLM-as-a-Critic” would benefit from a short table of abbreviations on first use.
  2. Several sentences in the introduction and related-work sections contain minor grammatical issues and missing citations to prior LTL synthesis and LLM-for-formal-methods literature.

Simulated Author's Rebuttal

3 responses · 1 unresolved

We thank the referee for the constructive and detailed comments, which highlight important aspects of our framework's theoretical grounding and experimental reporting. We address each major comment below and indicate the revisions we will make.

read point-by-point responses

  1. Referee: [§3.2] §3.2 (LLM-as-a-Critic): No formal argument or error-bound analysis is supplied showing that an LLM interpretation of a counterexample (which may be an infinite word or Büchi-automaton path) necessarily produces a modification that (a) removes the detected violation, (b) preserves satisfiability and logical consistency, and (c) introduces no new violations. The 0% violation claim therefore rests entirely on the unverified behavior of the LLM step.

    Authors: We agree that the LLM-as-a-Critic relies on the empirical behavior of the LLM rather than a formal guarantee. The design is iterative: the inclusion checker is re-invoked after each refinement until no violation remains, providing an external verification loop. However, we do not claim or provide a theoretical error bound on the LLM's interpretation step. In the revision we will add an explicit limitations paragraph acknowledging the heuristic nature of this component and the dependence on empirical validation. revision: partial

  2. Referee: [§4] §4 (Experimental evaluation): The abstract and experimental section report a 0% violation rate but supply no information on test-set cardinality, the provenance or selection procedure of the safety restrictions, the concrete definition of “violation,” or any baseline comparison against direct LLM generation or existing LTL translators. These omissions make it impossible to determine whether the result is load-bearing or an artifact of the chosen instances.

    Authors: The referee is correct that these details are currently insufficient. The manuscript will be revised to report the exact test-set size, the origin and selection criteria of the safety restrictions, a precise definition of violation (i.e., language inclusion failure), and direct comparisons against baselines including vanilla LLM prompting and prior LTL translation methods. revision: yes

  3. Referee: [§3.1] §3.1 (Language Inclusion integration): The framework treats the external inclusion checker as an infallible oracle whose counterexamples are always correctly parsed by the LLM; no discussion is given of the PSPACE-completeness of LTL inclusion or of the possibility that an LLM mis-step silently re-introduces a safety violation.

    Authors: The inclusion checker is an external, sound automata-based tool and is therefore treated as correct for the instances on which it terminates. We will add a short paragraph noting the PSPACE-completeness of LTL inclusion and the theoretical possibility of LLM misinterpretation of counterexamples, while emphasizing that the iterative re-checking loop is intended to detect and correct such errors in practice. revision: partial

standing simulated objections not resolved
  • A formal error-bound analysis or correctness proof for the LLM-as-a-Critic step cannot be supplied without fundamentally altering the empirical, LLM-driven nature of the method.

Circularity Check

0 steps flagged

No significant circularity; safety claims rest on external checker

full rationale

The paper's central result is an empirical 0% violation rate obtained by running an external language-inclusion checker on LLM-generated LTL formulas and feeding counterexamples back to an LLM-as-Critic. No equation, parameter, or quantity is defined in terms of the target safety metric and then re-used as a prediction; the inclusion check is a standard PSPACE decision procedure imported from automata theory rather than constructed from the framework's own outputs. No self-citation is invoked to justify uniqueness or to close a derivation loop. The architecture therefore contains no self-definitional, fitted-input, or self-citation-load-bearing step that reduces the claimed guarantee to its own inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 2 invented entities

The framework rests on the correctness of the external language inclusion checker and on the LLM's ability to interpret counterexamples without introducing semantic drift; these are domain assumptions rather than new entities with independent evidence.

axioms (2)
  • domain assumption The language inclusion checker correctly implements LTL semantics and returns valid counterexamples when a specification violates the safety restrictions.
    The entire refinement loop depends on the checker being sound; the abstract invokes it as the source of counterexamples.
  • domain assumption LLM outputs can be reliably parsed into valid LTL formulas without introducing syntax errors that the checker cannot handle.
    The framework assumes downstream parsing and refinement steps succeed.
invented entities (2)
  • LLM-as-an-Aligner no independent evidence
    purpose: Performs atomic proposition matching between generated LTL and safety restrictions
    New role introduced to enforce semantic alignment; no independent evidence outside the framework.
  • LLM-as-a-Critic no independent evidence
    purpose: Interprets counterexamples to refine LTL specifications
    New role for automated refinement; no independent evidence outside the framework.

pith-pipeline@v0.9.0 · 5792 in / 1501 out tokens · 24917 ms · 2026-05-22T23:48:59.252798+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Grammar-Constrained Refinement of Safety Operational Rules Using Language in the Loop: What Could Go Wrong

    cs.SE 2026-04 unverdicted novelty 5.0

    A grammar-constrained counterfactual refinement framework resolves inconsistencies in safety operational rules for an autonomous driving system while staying syntactically valid.

Reference graph

Works this paper leans on

59 extracted references · 59 canonical work pages · cited by 1 Pith paper

  1. [1]

    Advanced ramsey-based büchi automata inclusion testing

    Parosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukáš Holík, Chih-Duo Hong, Richard Mayr, and Tomáš Vojnar. Advanced ramsey-based büchi automata inclusion testing. In Joost-Pieter Katoen and Barbara König, editors,CONCUR 2011 – Concurrency Theory, pages 187–202, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. Title Suppressed Due to Excessive Length 17

    work page 2011

  2. [2]

    Advanced ramsey-based büchi automata inclusion testing

    Parosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukáš Holík, Chih-Duo Hong, Richard Mayr, and Tomáš Vojnar. Advanced ramsey-based büchi automata inclusion testing. In Joost-Pieter Katoen and Barbara König, editors,CONCUR 2011 – Concurrency Theory, pages 187–202, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg

    work page 2011

  3. [3]

    Symbolic ltl reactive synthesis

    Remco Abraham. Symbolic ltl reactive synthesis. Master’s thesis, University of Twente, 2021

    work page 2021

  4. [4]

    Ltl model checking for security protocols

    Alessandro Armando, Roberto Carbone, and Luca Compagna. Ltl model checking for security protocols. In20th IEEE Computer Security Foundations Symposium (CSF’07), pages 385–396, 2007

    work page 2007

  5. [5]

    Springer Berlin Heidelberg, Berlin, Heidelberg, 2012

    Tomáš Babiak, Mojmír Křetínský, Vojtěch Řehák, and Jan Strejček.LTL to Büchi Automata Translation: Fast and More Deterministic, volume 7214 ofLecture Notes in Computer Science, page 95–109. Springer Berlin Heidelberg, Berlin, Heidelberg, 2012

    work page 2012

  6. [6]

    MIT Press, Cambridge, Mass., 2008

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

    work page 2008

  7. [7]

    Equivalence and Inclusion Problem for Strongly Unambiguous Büchi Automata, volume 6031 ofLecture Notes in Computer Science, page 118–129

    Nicolas Bousquet and Christof Löding. Equivalence and Inclusion Problem for Strongly Unambiguous Büchi Automata, volume 6031 ofLecture Notes in Computer Science, page 118–129. Springer Berlin Heidelberg, Berlin, Heidelberg, 2010

    work page 2010

  8. [8]

    Synthesis of ltl formulas from natural language texts: State of the art and research directions

    Andrea Brunello, Angelo Montanari, and Mark Reynolds. Synthesis of ltl formulas from natural language texts: State of the art and research directions. LIPIcs, Volume 147, TIME 2019, 147:17:1–17:19, 2019

    work page 2019

  9. [9]

    Automatic control synthesis for swarm robots from formation and location-based high-level specifications

    Ji Chen, Hanlin Wang, Michael Rubenstein, and Hadas Kress-Gazit. Automatic control synthesis for swarm robots from formation and location-based high-level specifications. In 2020 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pages 8027–8034, 2020

    work page 2020

  10. [10]

    NL2TL: Transform- ing natural languages to temporal logics using large language models

    Yongchao Chen, Rujul Gandhi, Yang Zhang, and Chuchu Fan. NL2TL: Transform- ing natural languages to temporal logics using large language models. In Houda Bouamor, Juan Pino, and Kalika Bali, editors,Proceedings of the 2023 Confer- ence on Empirical Methods in Natural Language Processing, pages 15880–15903, Singapore, December 2023. Association for Computa...

    work page 2023

  11. [11]

    Edmund Clarke, Orna Grumberg, and Doron Peled.Model Checking. 01 2001

    work page 2001

  12. [12]

    Efficient reduction of nondeterministic au- tomata with application to language inclusion testing.Logical Methods in Com- puter Science, Volume 15, Issue 1, 11 2017

    Lorenzo Clemente and Richard Mayr. Efficient reduction of nondeterministic au- tomata with application to language inclusion testing.Logical Methods in Com- puter Science, Volume 15, Issue 1, 11 2017

    work page 2017

  13. [13]

    Springer Nature Switzerland, Cham, 2023

    Matthias Cosler, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, and Car- oline Trippel.nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models, volume 13965 ofLecture Notes in Computer Science, page 383–396. Springer Nature Switzerland, Cham, 2023

    work page 2023

  14. [14]

    Dill, Alan J

    David L. Dill, Alan J. Hu, and Howard Wong-Toi.Checking for language inclusion using simulation preorders, volume 575 ofLecture Notes in Computer Science, page 255–265. Springer Berlin Heidelberg, Berlin, Heidelberg, 1992

    work page 1992

  15. [15]

    Duret-Lutz and D

    A. Duret-Lutz and D. Poitrenaud. Spot: an extensible model checking library us- ing transition-based generalized buchi automata. InThe IEEE Computer Society’s 12th Annual International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems, 2004. (MASCOTS 2004). Proceed- ings., page 76–83, Volendam, The Netherlands, EU,...

    work page 2004

  16. [16]

    Spot 2.0 — a framework for ltl and ω-automata manipulation

    Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Étienne Renault, and Laurent Xu. Spot 2.0 — a framework for ltl and ω-automata manipulation. In Cyrille Artho, Axel Legay, and Doron Peled, editors, 18 Junle Li, Meiqi Tian, and Bingzhuo Zhong Automated Technology for Verification and Analysis, pages 122–129, Cham, 2016. Springe...

    work page 2016

  17. [17]

    Springer International Publishing, Cham, 2022

    Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, and Henrich Lauko.From Spot 2.0 to Spot 2.10: What’s New?, volume 13372 ofLecture Notes in Computer Science, page 174–187. Springer International Publishing, Cham, 2022

    work page 2022

  18. [18]

    Formalizing traffic rules for machine interpretability

    Klemens Esterle, Luis Gressenbuch, and Alois Knoll. Formalizing traffic rules for machine interpretability. In 2020 IEEE 3rd Connected and Automated Vehicles Symposium (CAVS), pages 1–7. IEEE, 2020

    work page 2020

  19. [19]

    Fainekos, H

    G.E. Fainekos, H. Kress-Gazit, and G.J. Pappas. Temporal logic motion planning for mobile robots. InProceedings of the 2005 IEEE International Conference on Robotics and Automation, pages 2020–2025, 2005

    work page 2005

  20. [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. Proceedings of the AAAI Conference on Artificial Intelligence, 37:16428–16430, June 2023

    work page 2023

  21. [21]

    Springer Berlin Heidel- berg, Berlin, Heidelberg, 2001

    Paul Gastin and Denis Oddoux.Fast LTL to Büchi Automata Translation, volume 2102 of Lecture Notes in Computer Science, page 53–65. Springer Berlin Heidel- berg, Berlin, Heidelberg, 2001

    work page 2001

  22. [22]

    Simple on-the-fly automatic verification of linear temporal logic.Proceedings of the 6th Symposium on Logic in Computer Science, 15, 12 1995

    Rob Gerth, Den Dolech, Doron Peled, Moshe Vardi, and Pierre Wolper. Simple on-the-fly automatic verification of linear temporal logic.Proceedings of the 6th Symposium on Logic in Computer Science, 15, 12 1995

    work page 1995

  23. [23]

    Predictive monitoring of traffic rules

    Luis Gressenbuch and Matthias Althoff. Predictive monitoring of traffic rules. In 2021 IEEE International Intelligent Transportation Systems Conference (ITSC), pages 915–922. IEEE, 2021

    work page 2021

  24. [24]

    Specification patterns for probabilistic quality properties

    Lars Grunske. Specification patterns for probabilistic quality properties. InPro- ceedings of the 13th international conference on Software engineering - ICSE ’08, page 31, Leipzig, Germany, 2008. ACM Press

    work page 2008

  25. [25]

    Bsp algorithms for LTL & CTL* model checking of security pro- tocols

    Michael Guedj. Bsp algorithms for LTL & CTL* model checking of security pro- tocols. PhD thesis, Université de Paris-Est/Créteil, 2012

    work page 2012

  26. [26]

    Formal specifications from natural language, 2023

    Christopher Hahn, Frederik Schmitt, Julia Janice Tillman, Niklas Metzger, Julian Siber, and Bernd Finkbeiner. Formal specifications from natural language, 2023

    work page 2023

  27. [27]

    Deepstl: from english requirements to signal temporal logic

    Jie He, Ezio Bartocci, Dejan Ničković, Haris Isakovic, and Radu Grosu. Deepstl: from english requirements to signal temporal logic. InProceedings of the 44th In- ternational Conference on Software Engineering, page 610–622, Pittsburgh Penn- sylvania, May 2022. ACM

    work page 2022

  28. [28]

    Holzmann

    G.J. Holzmann. The model checker spin. IEEE Transactions on Software Engi- neering, 23(5):279–295, May 1997

    work page 1997

  29. [29]

    Swen Jacobs, Guillermo A. Perez, Remco Abraham, Veronique Bruyere, Michael Cadilhac, Maximilien Colange, Charly Delfosse, Tom van Dijk, Alexandre Duret- Lutz, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Michael Luttenberger, Klara Meyer, Thibaud Michaud, Adrien Pommellet, Florian Renkin, Philipp Schlehuber-Caissier, Mouhammad Sakr, S...

    work page 2018

  30. [30]

    Springer Berlin Heidelberg, Berlin, Heidelberg, 2011

    Stasys Jukna.The Pigeonhole Principle, pages 53–75. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011

    work page 2011

  31. [31]

    Greenstreet

    Christoph Kern and Mark R. Greenstreet. Formal verification in hardware design: a survey.ACM Trans. Des. Autom. Electron. Syst., 4(2):123–193, April 1999. Title Suppressed Due to Excessive Length 19

    work page 1999

  32. [32]

    Cambridge University Press, 2009

    Philipp Koehn.Statistical machine translation. Cambridge University Press, 2009

    work page 2009

  33. [33]

    Konrad and B.H.C

    S. Konrad and B.H.C. Cheng. Real-time specification patterns. In Proceedings. 27th International Conference on Software Engineering, 2005. ICSE 2005., page 372–381, St. Louis, MO, USA, 2005. IEEe

    work page 2005

  34. [34]

    Construction and verification of plc-programs by ltl-specification

    EV Kuzmin, Valery A Sokolov, and DA Ryabukhin. Construction and verification of plc-programs by ltl-specification. Automatic Control and Computer Sciences, 49:453–465, 2015

    work page 2015

  35. [35]

    Shuvendu K. Lahiri, Sarah Fakhoury, Aaditya Naik, Georgios Sakkas, Saikat Chakraborty, Madanlal Musuvathi, Piali Choudhury, Curtis von Veh, Jee- vana Priya Inala, Chenglong Wang, and Jianfeng Gao. Interactive code generation via test-driven user-intent formalization, 2023

    work page 2023

  36. [36]

    Temporal logic task plan- ning for autonomous systems with active acquisition of information.IEEE Trans- actions on Intelligent Vehicles, 9(1):1436–1449, 2024

    Shuaiyi Li, Mengjie Wei, Shaoyuan Li, and Xiang Yin. Temporal logic task plan- ning for autonomous systems with active acquisition of information.IEEE Trans- actions on Intelligent Vehicles, 9(1):1436–1449, 2024

    work page 2024

  37. [37]

    Temporal logic guided safe reinforcement learning using control barrier functions, 2019

    Xiao Li and Calin Belta. Temporal logic guided safe reinforcement learning using control barrier functions, 2019

    work page 2019

  38. [38]

    Reinforcement learning with tem- poral logic rewards

    Xiao Li, Cristian-Ioan Vasile, and Calin Belta. Reinforcement learning with tem- poral logic rewards. In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pages 3834–3839, 2017

    work page 2017

  39. [39]

    Lang2LTL: Translating natural language commands to temporal specification with large language models

    Jason Xinyu Liu, Ziyi Yang, Benjamin Schornstein, Sam Liang, Ifrah Idrees, Ste- fanie Tellex, and Ankit Shah. Lang2LTL: Translating natural language commands to temporal specification with large language models. InWorkshop on Language and Robotics at CoRL 2022, 2022

    work page 2022

  40. [40]

    Michael Luttenberger, Philipp J Meyer, and Salomon Sickert. Practical synthesis of reactive systems from ltl specifications via parity games: You can teach an old dog new tricks: making a classic approach structured, forward-explorative, and incremental. Acta Informatica, 57(1):3–36, 2020

    work page 2020

  41. [41]

    Springer-Verlag, Berlin, Heidelberg, 1995

    Zohar Manna and Amir Pnueli.Temporal verification of reactive systems: safety. Springer-Verlag, Berlin, Heidelberg, 1995

    work page 1995

  42. [42]

    Oscar Mickelin, Necmiye Ozay, and Richard M. Murray. Synthesis of correct-by- construction control protocols for hybrid systems using partial state information. In 2014 American Control Conference, pages 2305–2311, 2014

    work page 2014

  43. [43]

    Springer Berlin Heidelberg, Berlin, Heidelberg, 1996

    Rani Nelken and Nissim Francez.Automatic translation of natural language sys- tem specifications into temporal logic, volume 1102 ofLecture Notes in Computer Science, page 360–371. Springer Berlin Heidelberg, Berlin, Heidelberg, 1996

    work page 1996

  44. [44]

    Ltl-specification for development and verification of control programs.Modeling and Analysis of Information Systems, 30(4):308–339, 2023

    Maxim Vyacheslavovich Neyzov and Egor Vladimirovich Kuzmin. Ltl-specification for development and verification of control programs.Modeling and Analysis of Information Systems, 30(4):308–339, 2023

    work page 2023

  45. [45]

    Onthelanguageinclusionproblemfortimedautomata: closing a decidability gap

    J.OuaknineandJ.Worrell. Onthelanguageinclusionproblemfortimedautomata: closing a decidability gap. InProceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004., pages 54–63, 2004

    work page 2004

  46. [46]

    The temporal logic of programs

    Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pages 46–57, 1977

    work page 1977

  47. [47]

    Risk-aware autonomous driving for linear temporal logic specifications

    Shuhao Qi, Zengjie Zhang, Zhiyong Sun, and Sofie Haesaert. Risk-aware autonomous driving for linear temporal logic specifications. arXiv preprint arXiv:2409.09769, 2024

    work page arXiv 2024

  48. [48]

    Richard Büchi

    J. Richard Büchi. Symposium on decision problems: On a decision method in restricted second order arithmetic. In Ernest Nagel, Patrick Suppes, and Alfred Tarski, editors,Logic, Methodology and Philosophy of Science, volume 44 ofStudies in Logic and the Foundations of Mathematics, pages 1–11. Elsevier, 1966. 20 Junle Li, Meiqi Tian, and Bingzhuo Zhong

    work page 1966

  49. [49]

    Safe reinforcement learning with policy-guided plan- ning for autonomous driving

    Jikun Rong and Nan Luan. Safe reinforcement learning with policy-guided plan- ning for autonomous driving. In2020 IEEE International Conference on Mecha- tronics and Automation (ICMA), pages 320–326. IEEE, 2020

    work page 2020

  50. [50]

    A survey of static formal methods for building dependable industrial automation systems

    Roopak Sinha, Sandeep Patil, Luis Gomes, and Valeriy Vyatkin. A survey of static formal methods for building dependable industrial automation systems. IEEE Transactions on Industrial Informatics, 15(7):3772–3783, 2019

    work page 2019

  51. [51]

    Efficient Büchi Automata from LTL Formulae, volume 1855 ofLecture Notes in Computer Science, page 248–263

    FabioSomenziandRoderickBloem. Efficient Büchi Automata from LTL Formulae, volume 1855 ofLecture Notes in Computer Science, page 248–263. Springer Berlin Heidelberg, Berlin, Heidelberg, 2000

    work page 2000

  52. [52]

    Behavior-based multi-robot collision avoidance

    Dali Sun, Alexander Kleiner, and Bernhard Nebel. Behavior-based multi-robot collision avoidance. In2014 IEEE International Conference on Robotics and Au- tomation (ICRA), pages 1668–1673, 2014

    work page 2014

  53. [53]

    An automata-theoretic approach to linear temporal logic.Lecture Notes in Computer Science, 08 1996

    Moshe Vardi. An automata-theoretic approach to linear temporal logic.Lecture Notes in Computer Science, 08 1996

    work page 1996

  54. [54]

    Language inclusion checking of timed automata based on property patterns.Ap- plied Sciences, 12(24):12946, December 2022

    Ting Wang, Yan Shen, Tieming Chen, Baiyang Ji, Tiantian Zhu, and Mingqi Lv. Language inclusion checking of timed automata based on property patterns.Ap- plied Sciences, 12(24):12946, December 2022

    work page 2022

  55. [55]

    Formal consistency checking over specifications in natural languages

    Rongjie Yan, Chih-Hong Cheng, and Yesheng Chai. Formal consistency checking over specifications in natural languages. InDesign, Automation & Test in Europe Conference & Exhibition (DATE), 2015, page 1677–1682, Grenoble, France, 2015. IEEE Conference Publications

    work page 2015

  56. [56]

    Global temporallogiccontrolsynthesisformultiagentsystemswithtimeandspacemargin

    Tiange Yang, Jinfeng Liu, Yuanyuan Zou, Tianyu Jia, and Shaoyuan Li. Global temporallogiccontrolsynthesisformultiagentsystemswithtimeandspacemargin. IEEE Transactions on Industrial Electronics, pages 1–11, 2024

    work page 2024

  57. [57]

    Formal synthesis of controllers for safety- critical autonomous systems: Developments and challenges

    Xiang Yin, Bingzhao Gao, and Xiao Yu. Formal synthesis of controllers for safety- critical autonomous systems: Developments and challenges. Annual Reviews in Control, 57:100940, 2024

    work page 2024

  58. [58]

    Automata- based controller synthesis for stochastic systems: A game framework via approxi- mate probabilistic relations.Automatica, 147:110696, 2023

    Bingzhuo Zhong, Abolfazl Lavaei, Majid Zamani, and Marco Caccamo. Automata- based controller synthesis for stochastic systems: A game framework via approxi- mate probabilistic relations.Automatica, 147:110696, 2023

    work page 2023

  59. [59]

    eventually

    Bingzhuo Zhong, Majid Zamani, and Marco Caccamo. Formal synthesis of con- trollers for uncertain linear systems against-regular properties: A set-based ap- proach. IEEE Transactions on Automatic Control, 69(1):214–229, 2023. Title Suppressed Due to Excessive Length 21 A Prompts used for invoking LLMs Transform the following natural language driving instru...

    work page 2023