State space reduction using partial $ au $-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.