TY - GEN

T1 - State Space Reduction Using Partial τ-Confluence

AU - Groote, J.F.

AU - Pol, van de, J.C.

PY - 2000

Y1 - 2000

N2 - 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.

AB - 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.

UR - http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=1893&spage=383

U2 - 10.1007/3-540-44612-5_34

DO - 10.1007/3-540-44612-5_34

M3 - Conference contribution

SN - 3-540-67901-4

T3 - Lecture Notes in Computer Science

SP - 383

EP - 393

BT - Mathematical Foundations of Computer Science (Proceedings 25th International Symposium, MFCS2000, Bratislava, Slovakia, August 28-September 1, 2000)

A2 - Nielsen, Mogens, Rovan, N

A2 - Rovan, B.

PB - Springer

ER -