Stuttering Abstraction for Model Checking
Abstraction is one of the most effective approaches to improving the
applicability and the scalability of model-checking. The goal of
abstraction is to construct a model which is small enough to
analyze, yet contains enough detail to allow conclusive analysis
of properties of interest. For a given concrete model,
the size of its smallest possible abstraction is intimately
related to the set of temporal properties preserved by the
abstraction. Thus, smaller abstractions are possible if
we reduce this set, for example, by disallowing the
use of the next-time operator. In this paper, we improve
the conclusiveness and efficiency of the 3-valued abstraction framework.
We start by proposing a number of simulation
relations that preserve true properties expressed in
subsets of CTL without the next-time operator.
We show how these simulation relations are
extended into refinement relations for defining 3-valued abstractions.
Using these refinement relations, we give a new abstraction method
that results in more conclusive abstract models.
We also study the efficient implementation of these abstract models.