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.
|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]|
|Organisation||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.