Temporal logic and fair discrete systems

DOI10.1007/978-3-319-10575-8_2MaRDI QIDQ3176360zbMATHOpenAlexFDO

Authors Nir Piterman, Amir Pnueli

Publication date 20 July 2018

Published in Handbook of Model Checking (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-10575-8_2

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Recommendations

• Temporal logic and state systems
• Temporal logics in computer science. Finite-state systems
• scientific article; zbMATH DE number 47403
• An introduction to practical formal methods using temporal logic
• scientific article; zbMATH DE number 4119600

Cites work

• scientific article; zbMATH DE number 1705164 (Why is no real title available?)
• scientific article; zbMATH DE number 3129315 (Why is no real title available?)
• scientific article; zbMATH DE number 3930354 (Why is no real title available?)
• scientific article; zbMATH DE number 3940713 (Why is no real title available?)
• scientific article; zbMATH DE number 3757688 (Why is no real title available?)
• scientific article; zbMATH DE number 1223729 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• scientific article; zbMATH DE number 4119616 (Why is no real title available?)
• scientific article; zbMATH DE number 1916673 (Why is no real title available?)
• scientific article; zbMATH DE number 3339435 (Why is no real title available?)
• A completeness theorem in modal logic
• A hierarchy of temporal logics with past
• An automata-theoretic approach to branching-time model checking
• Automata theory and model checking
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Binary decision diagrams
• Branching versus linear logics yet again
• Combining Model Checking and Deduction
• Deciding full branching time logic
• Decision procedures and expressiveness in the temporal logic of branching time
• Explicit-state model checking
• Functional specification of hardware via temporal logic
• Graph Games and Reactive Synthesis
• Model Checking Real-Time Systems
• Model checking procedural programs
• Model checking with strong fairness
• Modeling for Verification
• Myths about the mutual exclusion problem
• On bounded specifications
• On the Merits of Temporal Testers
• Predicate abstraction for program verification
• Reasoning about infinite computations
• Recognizing safety and liveness
• Satisfiability modulo theories
• Specification in CTL + past for verification in CTL.
• Temporal logic and state systems
• Temporal logic can be more expressive
• The Common Fragment of ACTL and LTL
• 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
• Up and Down The Temporal Way
• Using branching time temporal logic to synthesize synchronization skeletons
• Verification of Hybrid Systems
• “Sometimes” and “not never” revisited

Cited in

(31)

• Why systems of temporal logic are sometimes (un)useful?
• A language-theoretic view of verification
• Model checking procedural programs
• Hybrid Systems: Computation and Control
• Computer Science Logic
• scientific article; zbMATH DE number 3940713 (Why is no real title available?)
• scientific article; zbMATH DE number 4070338 (Why is no real title available?)
• Graph Games and Reactive Synthesis
• scientific article; zbMATH DE number 1796144 (Why is no real title available?)
• On some time properties of untimed propositional implication
• Temporal team semantics revisited
• Logic for Programming, Artificial Intelligence, and Reasoning
• scientific article; zbMATH DE number 1444725 (Why is no real title available?)
• Combining Model Checking and Deduction
• The complexity of verifying population protocols
• SAT-Based Model Checking
• A simple rewrite system for the normalization of linear temporal logic
• Abstraction and abstraction refinement
• scientific article; zbMATH DE number 1754681 (Why is no real title available?)
• Indiscrete models: model building and model checking over linear time
• ESTL: A Temporal Logic for Events and States
• Tools and Algorithms for the Construction and Analysis of Systems
• Problems concerning fairness and temporal logic for conflict-free Petri nets
• From Muller to parity and Rabin qutomata: optimal transformations preserving (history) determinism
• An introduction to practical formal methods using temporal logic
• Multi-Valued Reasoning about Reactive Systems
• Incorporating monitors in reactive synthesis without paying the price
• Compositional reasoning
• Safety, liveness and fairness in temporal logic
• Implementing a fair monodic temporal logic prover
• scientific article; zbMATH DE number 3993549 (Why is no real title available?)

Describes a project that uses

Uses Software

• CESAR
• UNITY

This page was built for publication: Temporal logic and fair discrete systems

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