This paper studies abstraction and refinement techniques in the setting of multi-valued model checking for the
-calculus. Two dimensions of abstractions are identified and studied: Abstraction by joining states of the underlying multi-valued Kripke structure as well as abstraction of truth values, for each following both an
account. It is shown that our notion of abstraction is
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
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.