Model checking with strong fairness

DOI10.1007/s10703-006-4342-yzbMath1100.68066OpenAlexW2020306722MaRDI QIDQ2505624

Amir Pnueli, Elad Shahar, Li-On Raviv, Yonit Kesten

Publication date: 28 September 2006

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-006-4342-y

zbMATH Keywords

fairnessmodel checkingtemporal logicLTLCTLfair discrete systemstemporal testers

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Temporal Logic and Fair Discrete Systems ⋮ Automatic discovery of fair paths in infinite-state transition systems ⋮ Model checking with fairness assumptions using PAT ⋮ Proving the existence of fair paths in infinite-state systems ⋮ A compositional approach to CTL\(^*\) verification ⋮ \textsc{LTL} falsification in infinite-state systems

Uses Software

• CESAR

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The \(\mu\)-calculus as an assertion-language for fairness arguments
• Completing the temporal picture
• Symbolic model checking: \(10^{20}\) states and beyond
• Modalities for model checking: Branching time logic strikes back
• Verification by augmented finitary abstraction
• A new heuristic for bad cycle detection using BDDs