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.

Specification and verification (program logics, model checking, etc.) (msc 68Q60), Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (msc 68Q85)
Software Engineering [SEN]
Specification and Analysis of Embedded Systems

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