Temporal logic and fair discrete systems

DOI10.1007/978-3-319-10575-8_2zbMATH Open1392.68263OpenAlexW2804015072MaRDI QIDQ3176360FDOQ3176360

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

Recommendations

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (25)

• From Muller to parity and Rabin qutomata: optimal transformations preserving (history) determinism
• A simple rewrite system for the normalization of linear temporal logic
• Title not available (Why is that?)
• ESTL: A Temporal Logic for Events and States
• Compositional Reasoning
• Title not available (Why is that?)
• Incorporating monitors in reactive synthesis without paying the price
• Graph Games and Reactive Synthesis
• Model Checking Procedural Programs
• SAT-Based Model Checking
• Problems concerning fairness and temporal logic for conflict-free Petri nets
• Computer Science Logic
• Temporal team semantics revisited
• Title not available (Why is that?)
• Title not available (Why is that?)
• Logic for Programming, Artificial Intelligence, and Reasoning
• Combining Model Checking and Deduction
• Tools and Algorithms for the Construction and Analysis of Systems
• Title not available (Why is that?)
• Implementing a fair monodic temporal logic prover
• The complexity of verifying population protocols
• Abstraction and Abstraction Refinement
• Safety, liveness and fairness in temporal logic
• Multi-Valued Reasoning about Reactive Systems
• Title not available (Why is that?)

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)