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

DOI10.1145/1297658.1297659MaRDI QIDQ5277790zbMATH OpenOpenAlexWikidataFDO

Authors Sharon Shoham, Orna Grumberg

Publication date 12 July 2017

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1297658.1297659

zbMATH Keywords

3-valued semanticsabstraction-refinementcounterexamplesCTLmodel-checking gamestemporal logic

Mathematics Subject Classification ID

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

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

(14)

• Producing explanations for rich logics
• Generalized abstraction-refinement for game-based CTL lifted model checking
• Compositional verification and 3-valued abstractions join forces
• When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus
• Abstraction and abstraction refinement
• Solving Games Via Three-Valued Abstraction Refinement
• Multi-valued model checking games
• Improved model checking of hierarchical systems
• Tools and Algorithms for the Construction and Analysis of Systems
• The abstraction-refinement framework in model checking
• A game-based framework for CTL counterexamples and 3-valued abstraction-refinement.
• An abstraction-refinement framework for verifying strategic properties in multi-agent systems with imperfect information
• Incremental model checking for fuzzy computation tree logic
• Tracy, traces, and transducers: computable counterexamples and explanations for HyperLTL model-checking

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 Q5277790)