Martin Leucker, Researcher, Institut für Informatik, Technische Universität München, Germany
Abstraction is one of the key techniques for model checking. In this presentation, we briefly review two-valued as well as three-valued abstraction techniques. We then turn our attention towards multi-valued logics. In multi-valued logics interpreted over multi-valued Kripke structures, the semantics of a formula is no longer just true or false but one of many truth values. To make multi-valued model checking feasible in practice, abstraction and refinement techniques are essential in this setting as well. In this talk, we address abstraction and refinement techniques in the setting of multi-valued model checking for the mu-calculus.