Abstract of Paper

State Space Reduction using Partial $\tau$-Confluence
by Jan Friso Groote and Jaco van de Pol

Abstract:

We present an efficient algorithm to determine the maximal class of
confluent $\tau$-transitions in a labelled transition system. Confluent
$\tau$-transitions are inert with respect to branching bisimulation.  This
allows to use $\tau$-priorisation, which means that in a state with a
confluent outgoing $\tau$-transition all other transitions can be removed,
maintaining branching bisimulation.  In combination with the removal of
$\tau$-loops, and the compression of $\tau$-sequences this yields an
efficient algorithm to reduce the size of large state spaces.