State Space Reduction Using Partial tau-Confluence

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

Authors

• Jan Friso Groote
• Jaco van de Pol

Keywords

No keywords are indexed for this paper.