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}.