Model-Checking Infinite State-Space Systems with Fine-Grained Abstractions Using SPIN

Abstract

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.