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

DOI10.1145/1297658.1297659zbMath1367.68203OpenAlexW1998779352WikidataQ124834098 ScholiaQ124834098MaRDI QIDQ5277790

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

temporal logiccounterexamplesCTLmodel-checking gamesabstraction-refinement3-valued semantics

Mathematics Subject Classification ID

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

Related Items (7)

Abstraction and Abstraction Refinement ⋮ An abstraction-refinement framework for verifying strategic properties in multi-agent systems with imperfect information ⋮ Generalized abstraction-refinement for game-based CTL lifted model checking ⋮ Multi-valued model checking games ⋮ Improved model checking of hierarchical systems ⋮ Compositional verification and 3-valued abstractions join forces ⋮ Producing explanations for rich logics

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