Generating Counterexamples for Multi-Valued Model-Checking
Abstract
Counterexamples explain why a desired temporal logic property fails to
hold, and as such are considered to be the most useful form of output
from model-checkers. Multi-valued model-checking, introduced
in~\cite{chechik01a} is an extension of classical model-checking.
Instead of classical logic, it operates on elements of a given De
Morgan algebra, e.g. the Kleene algebra~\cite{kleene52}.
Multi-valued model-checking has been used in a number of applications,
primarily when reasoning about partial~\cite{bruns01} and
inconsistent~\cite{easterbrook01} systems. In this paper we show how
to generate counterexamples for multi-valued model-checking. We
describe the proof system for a multi-valued variant of CTL, discuss
how to use it to generate counterexamples. The techniques presented in
this paper have been implemented as part of our symbolic multi-valued
model-checker \xchek~\cite{chechik02b}.