Model-Checking Infinite State-Space Systems with Fine-Grained
Abstractions Using SPIN
In analyzing infinite-state systems, it is often useful to define
multiple-valued predicates. Such predicates can determine the
(finite) levels of desirability of the current system state and
transitions between them. We can capture multiple-valued
predicates as elements of a logic defined over finite total orders (FTOs).
In this paper we extend automata-theoretic LTL model-checking
to reasoning about a class of multiple-valued logics.
We also show that model-checking over FTOs is reducible to
classical model-checking, and thus can be implemented in SPIN.