State Space Reduction Using Partial τ-Confluence

J.F. Groote, J.C. Pol, van de

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

21 Citations (Scopus)
2 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publicationMathematical Foundations of Computer Science (Proceedings 25th International Symposium, MFCS2000, Bratislava, Slovakia, August 28-September 1, 2000)
EditorsN Nielsen, Mogens, Rovan, B. Rovan
PublisherSpringer
Pages383-393
ISBN (Print)3-540-67901-4
DOIs
Publication statusPublished - 2000

Publication series

NameLecture Notes in Computer Science
Volume1893
ISSN (Print)0302-9743

Cite this

Groote, J. F., & Pol, van de, J. C. (2000). State Space Reduction Using Partial τ-Confluence. In N. Nielsen, Mogens, Rovan, & B. Rovan (Eds.), Mathematical Foundations of Computer Science (Proceedings 25th International Symposium, MFCS2000, Bratislava, Slovakia, August 28-September 1, 2000) (pp. 383-393). (Lecture Notes in Computer Science; Vol. 1893). Springer. https://doi.org/10.1007/3-540-44612-5_34