Back to the future: a fresh look at linear temporal logic

DOI10.1007/978-3-030-79121-6_1OpenAlexW3173305027MaRDI QIDQ2117656

Javier Esparza

Publication date: 22 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-79121-6_1

zbMATH Keywords

formal verificationlinear temporal logic\( \omega \)-automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Uses Software

• PRISM
• SPIN
• Rabinizer
• Strix
• Owl
• MoChiBA

Cites Work

• Unnamed Item
• Unnamed Item
• Strix
• Experiments with deterministic \(\omega\)-automata for formulas of linear temporal logic
• Automata-theoretic techniques for modal logics of programs
• The temporal semantics of concurrent programs
• Completing the temporal picture
• Practical synthesis of reactive systems from LTL specifications via parity games
• From LTL to deterministic automata. A safraless compositional approach
• On-the-Fly Stuttering in the Construction of Deterministic ω-Automata
• On the Krohn-Rhodes Cascaded Decomposition Theorem
• Temporal Verification of Reactive Systems: Response
• The complexity of probabilistic verification
• Handbook of Model Checking
• Rabinizer: Small Deterministic Automata for LTL(F,G)
• One Theorem to Rule Them All
• An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata
• Rabinizer 2: Small Deterministic Automata for LTL ∖ GU
• Characterization of temporal property classes
• Implementation and Application of Automata
• Owl: a library for \(\omega \)-words, automata, and LTL

This page was built for publication: Back to the future: a fresh look at linear temporal logic