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

## Partial Order Reductions Preserving Simulations.

Penczek, Wojciech;
Gerth, Rob;
Kuiper, Ruurd;
Szreter, Maciej
In:
Burkhard, H.-D.; Czaja, L.; Nguyen, H.-S.; Starke, P.: *Proceedings of the CSP'99 Workshop, Warsaw, 28-30 September 1999*, pages 153-171.
1999.

Abstract:
The `state explosion problem' can be alleviated by using partial order
reduction techniques. These methods rely on expanding only a fragment of
the full state space of a program, which is sufficient for verifying the
formulas of temporal logics LTL-x or CTL*-x (i. e., LTL or CTL* without
the next state operator). This is guaranteed by preserving either a
stuttering maximal trace equivalence or a stuttering bisimulation between
the full and the reduced state space. Since a stuttering bisimulation is
much more restrictive than a stuttering maximal trace equivalence,
resulting in a less powerful reductions for CTL*-x, we study here partial
order reductions that preserve equivalences `in-between', in particular a
stuttering simulation which is induced by the universal fragment of
CTL*-x, called ACTL*-x. The reductions generated by our method preserve
also branching simulation and weak simulation, but surprisingly, they do
not appear to be included into the reductions obtained by Peled's method
for verifying LTL-x properties. Therefore, in addition to ACTL*-x
reduction method we suggest also an approvement of the LTL-x reduction
method. Moreover, we consider concurrency fair version of ACTL*-x and
prove that reduction for fair ACTL*-x is much more efficient than for
ACTL*-x.

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