We present an efficient algorithm to determine the maximal class of confluent τ -transitions in a labelled transition system. Confluent τ -transitions are inert with respect to branching bisimulation. This al-lows to use τ -priorisation, which means that in a state with a confluent outgoing τ -transition all other transitions can be removed, maintaining branching bisimulation. In combination with the removal of τ -loops, and the compression of T-sequences this yields an efficient algorithm to reduce the size of large state spaces.
CITATION STYLE
Groote, J. F., & van de Pol, J. (2000). State space reduction using partial τ-confluence. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1893, pp. 383–393). Springer Verlag. https://doi.org/10.1007/3-540-44612-5_34
Mendeley helps you to discover research relevant for your work.