We present an efficient algorithm to determine the maximal class of confluent t-transitions in a labelled transition system. Confluent t-transitions are inert with respect to branching bisimulation. This allows to use t-priorisation, which means that in a state with a confluent outgoing t-transition all other transitions can be removed, maintaining branching bisimulation. In combination with the removal of t-loops, and the compression of t-sequences this yields an efficient algorithm to reduce the size of large state spaces.
|Title of host publication||Mathematical Foundations of Computer Science (Proceedings 25th International Symposium, MFCS2000, Bratislava, Slovakia, August 28-September 1, 2000)|
|Editors||N Nielsen, Mogens, Rovan, B. Rovan|
|Publication status||Published - 2000|
|Name||Lecture Notes in Computer Science|