A game-based framework for CTL counterexamples and 3-valued abstraction-refinement.

DOI10.1007/B11831MaRDI QIDQ5900684zbMATH OpenOpenAlexFDO

Authors Sharon Shoham, Orna Grumberg

Publication date 20 April 2010

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b11831

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60) Games involving graphs (91A43)

Recommendations

• A game-based framework for CTL counterexamples and 3-valued abstraction-refinement
• The abstraction-refinement framework in model checking
• Tools and Algorithms for the Construction and Analysis of Systems
• 2-valued and 3-valued abstraction-refinement in model checking
• Solving Games Via Three-Valued Abstraction Refinement

Cited in

(18)

• TOrPEDO : witnessing model correctness with topological proofs
• A framework for compositional verification of multi-valued systems via abstraction-refinement
• When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus
• 2-valued and 3-valued abstraction-refinement in model checking
• Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model Checking
• Model Checking Recursive Programs with Exact Predicate Abstraction
• Multi-valued model checking games
• Integrating topological proofs with model checking to instrument iterative design
• Supervisory control for collision avoidance in vehicular networks using discrete event abstractions
• A game-based framework for CTL counterexamples and 3-valued abstraction-refinement
• Tools and Algorithms for the Construction and Analysis of Systems
• The abstraction-refinement framework in model checking
• Better Under-Approximation of Programs by Hiding Variables
• Verification, Model Checking, and Abstract Interpretation
• Variability abstraction and refinement for game-based lifted model checking of full CTL
• Data structures for symbolic multi-valued model-checking
• 3-valued abstraction: More precision at less cost
• Solving games via three-valued abstraction refinement

This page was built for publication: A game-based framework for CTL counterexamples and 3-valued abstraction-refinement.

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