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.

Software Engineering [SEN]
Specification and Analysis of Embedded Systems

Groote, J. F., & van de Pol, J. (2000). State space reduction using partial $ au $-confluence. Software Engineering [SEN]. CWI.