Automated temporal reasoning about reactive systems
From MaRDI portal
Temporal logic (03B44) Logic in computer science (03B70) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Recommendations
Cites work
- A lattice-theoretical fixpoint theorem and its applications
- A linear-time model-checking algorithm for the alternation-free modal mu- calculus
- A model and temporal proof system for networks of processes
- Adequate proof principles for invariance and liveness properties of concurrent programs
- Alternative semantics for temporal logics
- An elementary proof of the completeness of PDL
- Automata-theoretic techniques for modal logics of programs
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Automatic Verification of Sequential Circuits Using Temporal Logic
- Can message buffers be axiomatized in linear temporal logic?
- Communicating sequential processes
- Decidability of Second-Order Theories and Automata on Infinite Trees
- Deciding full branching time logic
- Decision procedures and expressiveness in the temporal logic of branching time
- Fairness and related properties in transition systems - a temporal logic to deal with fairness
- Graph-Based Algorithms for Boolean Function Manipulation
- scientific article; zbMATH DE number 4179361 (Why is no real title available?)
- scientific article; zbMATH DE number 3861073 (Why is no real title available?)
- scientific article; zbMATH DE number 3870578 (Why is no real title available?)
- scientific article; zbMATH DE number 3876574 (Why is no real title available?)
- scientific article; zbMATH DE number 3898850 (Why is no real title available?)
- scientific article; zbMATH DE number 3919813 (Why is no real title available?)
- scientific article; zbMATH DE number 3937153 (Why is no real title available?)
- scientific article; zbMATH DE number 3972158 (Why is no real title available?)
- scientific article; zbMATH DE number 3972842 (Why is no real title available?)
- scientific article; zbMATH DE number 3974280 (Why is no real title available?)
- scientific article; zbMATH DE number 3982506 (Why is no real title available?)
- scientific article; zbMATH DE number 3990873 (Why is no real title available?)
- scientific article; zbMATH DE number 3735115 (Why is no real title available?)
- scientific article; zbMATH DE number 3755842 (Why is no real title available?)
- scientific article; zbMATH DE number 50851 (Why is no real title available?)
- scientific article; zbMATH DE number 177240 (Why is no real title available?)
- scientific article; zbMATH DE number 177253 (Why is no real title available?)
- scientific article; zbMATH DE number 3492660 (Why is no real title available?)
- scientific article; zbMATH DE number 3537204 (Why is no real title available?)
- scientific article; zbMATH DE number 3574936 (Why is no real title available?)
- scientific article; zbMATH DE number 4124989 (Why is no real title available?)
- scientific article; zbMATH DE number 3237829 (Why is no real title available?)
- scientific article; zbMATH DE number 3271460 (Why is no real title available?)
- scientific article; zbMATH DE number 3363520 (Why is no real title available?)
- scientific article; zbMATH DE number 3368555 (Why is no real title available?)
- Is “sometime” sometimes better than “always”?
- Local model checking for infinite state spaces
- Modalities for model checking: Branching time logic strikes back
- Myths about the mutual exclusion problem
- Propositional dynamic logic of looping and converse is elementarily decidable
- Propositional dynamic logic of regular programs
- Proving Liveness Properties of Concurrent Programs
- Reasoning about systems with many processes
- Reasoning with time and chance
- Results on the propositional \(\mu\)-calculus
- Star-free regular sets of ω-sequences
- Synthesis of Communicating Processes from Temporal Logic Specifications
- Temporal logic can be more expressive
- Testing and generating infinite sequences by a finite automaton
- The complementation problem for Büchi automata with applications to temporal logic
- The complexity of propositional linear temporal logics
- The temporal logic of branching time
- The temporal semantics of concurrent programs
- Uniform inevitability is tree automaton ineffable
- Using branching time temporal logic to synthesize synchronization skeletons
- Verifying concurrent processes using temporal logic
- “Sometimes” and “not never” revisited
This page was built for publication: Automated temporal reasoning about reactive systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6560389)
