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

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

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

linear temporal logicformal verification\( \omega \)-automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Cites Work

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

Cited In (2)

• Tomorrow’s Sea-Battle and the Beginning of Temporal Logic
• Past is for free: On the complexity of verifying linear temporal properties with past

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2117656)