When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus

DOI10.1016/J.IC.2006.10.009zbMath1306.68100OpenAlexW2110783522MaRDI QIDQ2643076

Martin Lange, Sharon Shoham, Martin Leucker, Orna Grumberg

Publication date: 23 August 2007

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2006.10.009

Mathematics Subject Classification ID

Applications of game theory (91A80) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (10)

Conway Games, Coalgebraically ⋮ Equivalences and Congruences on Infinite Conway Games ⋮ Abstraction and Abstraction Refinement ⋮ An abstraction-refinement framework for verifying strategic properties in multi-agent systems with imperfect information ⋮ Improved model checking of hierarchical systems ⋮ Model checking properties on reduced trace systems ⋮ Compositional verification and 3-valued abstractions join forces ⋮ Unnamed Item ⋮ Efficient Algorithms for Omega-Regular Energy Games ⋮ A framework for compositional verification of multi-valued systems via abstraction-refinement

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Results on the propositional \(\mu\)-calculus
• Tableau-based model checking in the propositional mu-calculus
• Symbolic model checking: \(10^{20}\) states and beyond
• Property preserving abstractions for the verification of concurrent systems
• A lattice-theoretical fixpoint theorem and its applications
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification
• Computer Aided Verification
• Decidability of DPDA equivalence
• On model checking for the \(\mu\)-calculus and its fragments

This page was built for publication: When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus