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 -