Multi-Valued Model Checking via Classical Model Checking
Abstract
Multi-valued model-checking is an extension of classical
model-checking to reasoning about systems with uncertain information,
which are common during early design stages. The additional values of
the logic are used to capture the degree of uncertainty. In this
paper, we show that the multi-valued $\mu$-calculus model-checking
problem is reducible to several classical model-checking problems. The
reduction allows one to reuse existing model-checking tools and
algorithms to solve multi-valued model-checking problems. This paper
generalizes, extends and corrects previous work in this area, done in
the context of 3-valued models, symbolic model-checking, and De Morgan
algebras.