An O(m log n) algorithm for stuttering equivalence and branching bisimulation

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

10 Citaten (Scopus)
11 Downloads (Pure)

Samenvatting

We provide a new algorithm to determine stuttering equivalence with time complexity O(m log n), where n is the number of states and m is the number of transitions of a Kripke structure. This algorithm can also be used to determine branching bisimulation in O(m(log|Act|+log n)) time. Theoretically, our algorithm substantially improves upon existing algorithms which all have time complexity O(mn) [2,3,9]. Moreover, it has better or equal space complexity. Practical results confirm these findings showing that our algorithm can outperform existing algorithms with orders of magnitude, especially when the sizes of the Kripke structures are large.

Originele taal-2Engels
TitelTools and Algorithms for the Construction and Analysis of Systems
Subtitel22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings
RedacteurenM. Chechik, J.-F. Raskin
Plaats van productieDordrecht
UitgeverijSpringer
Pagina's607-624
Aantal pagina's18
ISBN van elektronische versie978-3-662-49674-9
ISBN van geprinte versie978-3-662-49673-2
DOI's
StatusGepubliceerd - 2016
Evenement22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016) - Eindhoven, Nederland
Duur: 2 apr 20168 apr 2016
Congresnummer: 22

Publicatie series

NaamLecture Notes in Computer Science
Volume9636
ISSN van geprinte versie03029743
ISSN van elektronische versie16113349

Congres

Congres22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016)
Verkorte titelTACAS 2016
LandNederland
StadEindhoven
Periode2/04/168/04/16

Vingerafdruk Duik in de onderzoeksthema's van 'An O(m log n) algorithm for stuttering equivalence and branching bisimulation'. Samen vormen ze een unieke vingerafdruk.

  • Citeer dit

    Groote, J. F., & Wijs, A. J. (2016). An O(m log n) algorithm for stuttering equivalence and branching bisimulation. In M. Chechik, & J-F. Raskin (editors), Tools and Algorithms for the Construction and Analysis of Systems: 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings (blz. 607-624). (Lecture Notes in Computer Science; Vol. 9636). Springer. https://doi.org/10.1007/978-3-662-49674-9_40