State space reduction using partial $\tau$-confluence

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.