XChek -- A Multi-Valued Symbolic Model-Checker

Project members

Description

Classical logic cannot be used to effectively reason about systems with uncertainty (lack of essential information) or inconsistency (contradictory information often occurring when information is gathered from multiple sources). This is why we propose the use of quasi-boolean multi-valued logics for reasoning about such systems.

Multi-valued logics support the explicit modeling of uncertainty and disagreement by allowing additional truth values in the logic. Such logics can be used for verification of dynamic properties of systems even where complete, agreed upon models of the system are not available.

We have built a symbolic model-checker for multi-valued temporal logics. The model-checker works for any multi-valued logic whose truth values form a quasi-boolean lattice. Our models are generalized Kripke structures. where both atomic propositions and transitions between states may take any of the truth values of a given multi-valued logic. Properties to be model checked are expressed in a temporal logic generalized with a multi-valued semantics.

Most relevant publications

• Multi-Valued Symbolic Model-Checking This is the definitive paper on our approach. It describes the theory and a few interesting applications of multi-valued model-checking. (2003)
• Multi-Valued Model Checking via Classical Model Checking Multi-valued model-checking is reducible to several questions to the classical model-checker. This paper shows the reduction. (2003)
• Generating Counterexamples for Multi-Valued Model-Checking Here we describe how to represent multi-valued counter-examples and use them for exploration and navigation. (2003)
• Model-Checking Infinite State-Space Systems with Finte-Grained Abstractions Using SPIN Here we describe multi-valued automata-theoretic model-checking. (2001)
• Data Structures for Symbolic Multi-Valued Model-Checking There are many ways to represent multi-valued models symbolically. This paper discusses the available alternatives and evaluates them empirically. (2002)

Implementation:

    The prototype version of the model-checker is available.  To obtain a copy, send an email to xchek@cs.utoronto.ca.

Future work

• input language for the model-checker: We are struggling with finding a good input language for our model-checker. It currently supports XML and a simplified version of SMV models, but much more work is necessary both in language design and in engineering to make this a really usable tool.
• incorporation of the SAT solver: We would like our model-checker to use current Bounded Model-Checking (BMC) technology, based on the use of SAT solvers.
• LTL Model-Checking and Query-Checking: We found that in many cases we would like to ask an LTL rather than a CTL question. This is currently not implemented in our framework, but should, if we want to make it more usable.
• Building a Simulator: We need a tool for generating and playing back sequences of inputs. Such a tool would be useful for understanding models, testcases, runtime verification and a variety of other tasks.