## ``Next'' Heuristic for On-the-fly Model Checking

*Rajeev Alur and
Bow-Yaw Wang*
We present a new heuristic for on-the-fly enumerative
invariant verification.
The heuristic is based on a construct for temporal scaling,
called *next*, that
compresses a sequence of transitions leading to a given target set
into a single metatransition.
First, we give an on-the-fly algorithm to search a process expression
built using the constructs of hiding, parallel composition, and temporal
scaling.
Second, we show that as long the target set Theta of transitions
includes all transitions that access variables shared with the environment,
the process *next Theta for P* and *P* are equivalent according
to the weak-simulation equivalence.
As a result, to search the product of given processes, we can cluster
processes into groups with as little communication among them as possible,
and compose the groups only after applying appropriate hiding and
temporal scaling operators.
Applying this process recursively gives an expression that has multiple
nested applications of *next*, and has potentially much fewer states
than the original product.
We report on an implementation, and show significant reductions for
a tree-structured parity computer and a ring-structured leader-election
protocol.

In
*Proceedings of the
Tenth International Conference on Concurrency Theory*
(CONCUR'99),
Lecture Notes in Computer Science 1664,
Springer-Verlag, pp. 98--113, 1999.