“Don’t know” for Multi-Valued Systems

Speaker

Martin

Leucker

Title “Don’t know” for Multi-Valued Systems
When 29.06.2009
Where Lecture Room Informatik 1
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.