*For the most recent entries see the
Petri Nets Newsletter.*

## Exploiting predicate structure for efficient reachability detection.

Kashyap, Sujatha;
Garg, Vijay K.
In:
ACM international Conference on Automated software engineering: *ASE '05: Proceedings of the 20th IEEE*, pages 4-13.
ACM Press,
2005.

Abstract:
Partial order (p.o.) reduction techniques are a popular and effective
approach for tackling state space explosion in the verification of
concurrent systems. These techniques generate a reduced search space that
could be exponentially smaller than the complete state space. Their major
drawback is that the amount of reduction achieved is highly sensitive to
the properties being verified. For the same program, different properties
could result in very different amounts of reduction achieved.We present a
new approach which combines the benefits of p.o. reduction with the added
advantage that the size of the constructed state space is completely
independent of the properties being verified. As in p.o. reduction, we use
the notion of persistent sets to construct a representative interleaving
for each maximal trace of the program. However, we retain concurrency
information by assigning vector timestamps to the events in each
interleaving. Our approach hinges upon the use of efficient algorithms
that parse the encoded concurrency information in the representative
interleaving to determine whether a safety violation exists in any
interleaving of the corresponding trace. We show that, for some types of
predicates, reachability detection can be performed in time that is
polynomial in the length of the interleaving. Typically, these predicates
exhibit certain characteristics that can be exploited by the detection
algorithm.We implemented our algorithms in the popular model checker SPIN,
and present experimental results that demonstrate the effectiveness of our
techniques. For example, we verified a distributed dining philosophers
protocol in 0.03 seconds, using 1.253 MB of memory. SPIN, using
traditional p.o. reduction techniques, took 759.71 seconds and 439.116 MB
of memory.

*Do you need a refined search? Try our search engine
which allows complex field-based queries.*
*Back to the Petri Nets Bibliography*