Abstract
This work presents game-based model checking for abstract models with respect to specifications in μ-calculus, interpreted over a 3-valued semantics. If the model checking result is indefinite (don't know), the abstract model is refined, based on an analysis of the cause for this result. For finite concrete models our abstraction-refinement is fully automatic and guaranteed to terminate with a definite result true or false. © Springer-Verlag Berlin Heidelberg 2005.
Cite
CITATION STYLE
Grumberg, O., Lange, M., Leucker, M., & Shoham, S. (2005). Don’t know in the μ-calculus. In Lecture Notes in Computer Science (Vol. 3385, pp. 233–249). Springer Verlag. https://doi.org/10.1007/978-3-540-30579-8_16
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
