Automated temporal reasoning about reactive systems

DOI10.1007/3-540-60915-6_3zbMath1543.68206MaRDI QIDQ6560389

E. Allen Emerson

Publication date: 21 June 2024

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Probabilistic temporal logic with countably additive semantics

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The temporal logic of branching time
• Adequate proof principles for invariance and liveness properties of concurrent programs
• Results on the propositional \(\mu\)-calculus
• Using branching time temporal logic to synthesize synchronization skeletons
• A model and temporal proof system for networks of processes
• The complementation problem for Büchi automata with applications to temporal logic
• Automata-theoretic techniques for modal logics of programs
• Uniform inevitability is tree automaton ineffable
• The temporal semantics of concurrent programs
• An elementary proof of the completeness of PDL
• Myths about the mutual exclusion problem
• Verifying concurrent processes using temporal logic
• Fairness and related properties in transition systems - a temporal logic to deal with fairness
• Local model checking for infinite state spaces
• Propositional dynamic logic of regular programs
• A linear-time model-checking algorithm for the alternation-free modal mu- calculus
• Modalities for model checking: Branching time logic strikes back
• Alternative semantics for temporal logics
• Decision procedures and expressiveness in the temporal logic of branching time
• A lattice-theoretical fixpoint theorem and its applications
• Temporal logic can be more expressive
• Propositional dynamic logic of looping and converse is elementarily decidable
• Synthesis of Communicating Processes from Temporal Logic Specifications
• Reasoning with time and chance
• Can message buffers be axiomatized in linear temporal logic?
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Deciding full branching time logic
• Graph-Based Algorithms for Boolean Function Manipulation
• Automatic Verification of Sequential Circuits Using Temporal Logic
• “Sometimes” and “not never” revisited
• The complexity of propositional linear temporal logics
• Proving Liveness Properties of Concurrent Programs
• Is “sometime” sometimes better than “always”?
• Communicating sequential processes
• Star-free regular sets of ω-sequences
• Reasoning about systems with many processes
• Testing and generating infinite sequences by a finite automaton
• Decidability of Second-Order Theories and Automata on Infinite Trees

This page was built for publication: Automated temporal reasoning about reactive systems