Temporal Logic and Fair Discrete Systems

DOI10.1007/978-3-319-10575-8_2zbMath1392.68263OpenAlexW2804015072MaRDI QIDQ3176360

Amir Pnueli, Nir Piterman

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)

Related Items (10)

SAT-Based Model Checking ⋮ Compositional Reasoning ⋮ Abstraction and Abstraction Refinement ⋮ Model Checking Procedural Programs ⋮ Combining Model Checking and Deduction ⋮ Graph Games and Reactive Synthesis ⋮ Incorporating monitors in reactive synthesis without paying the price ⋮ Multi-Valued Reasoning about Reactive Systems ⋮ A simple rewrite system for the normalization of linear temporal logic ⋮ The complexity of verifying population protocols

Uses Software

• CESAR
• UNITY

Cites Work

• A hierarchy of temporal logics with past
• The temporal logic of branching time
• Branching versus linear logics yet again
• Using branching time temporal logic to synthesize synchronization skeletons
• The complementation problem for Büchi automata with applications to temporal logic
• Recognizing safety and liveness
• Myths about the mutual exclusion problem
• Reasoning about infinite computations
• Specification in CTL + past for verification in CTL.
• Decision procedures and expressiveness in the temporal logic of branching time
• Model checking with strong fairness
• Temporal logic and state systems
• On Bounded Specifications
• Modeling for Verification
• Automata Theory and Model Checking
• Explicit-State Model Checking
• Binary Decision Diagrams
• Satisfiability Modulo Theories
• Predicate Abstraction for Program Verification
• Model Checking Procedural Programs
• Combining Model Checking and Deduction
• Functional Specification of Hardware via Temporal Logic
• Graph Games and Reactive Synthesis
• Model Checking Real-Time Systems
• Verification of Hybrid Systems
• A completeness theorem in modal logic
• Temporal logic can be more expressive
• On the Merits of Temporal Testers
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Deciding full branching time logic
• “Sometimes” and “not never” revisited
• The complexity of propositional linear temporal logics
• Up and Down The Temporal Way
• An automata-theoretic approach to branching-time model checking
• The Common Fragment of ACTL and LTL
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Temporal Logic and Fair Discrete Systems