"Don't know'' for Multi-Valued Systems

Prof. Dr. Martin Leucker (TU München, DE)

 

Abstract:

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 talk, we address
abstraction and refinement techniques in the setting of multi-valued
model checking for the mu-calculus.

Two dimensions of abstractions are identified and studied: Abstraction
of by joining states of the underlying multi-valued Kripke structure
as well as abstraction of truth values.  We introduce abstractions
following an optimistic and pessimistic account of the
underlying system and truth values.  It is shown that our notion of
abstraction is conservative in the following sense: The truth
value in a concrete system is `between'' the optimistic and
pessimistic assessment.  Moreover, model checking of abstracted
systems is shown to be again a multi-valued model checking problem,
allowing to reuse multi-valued model checking engines.  Finally,
whenever the optimistic and pessimistic model checking result differ,
the cause for such an assessment is identified, allowing the
abstraction to be refined to eventually yield a result for which both
the optimistic and pessimistic assessment coincide.