An O(m log n) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation

J.F. Groote, D.N. Jansen, J.J.A. Keiren, A.J. Wijs

Research output: Contribution to journalArticleAcademicpeer-review

Abstract

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, where Act is the set of actions in a labeled transition system.

Theoretically, our algorithm substantially improves upon existing algorithms, which all have time complexity of the form O(mn) at best. Moreover, it has better or equal space complexity. Practical results confirm these findings: they show that our algorithm can outperform existing algorithms by several orders of magnitude, especially when the Kripke structures are large.

The importance of our algorithm stretches far beyond stuttering equivalence and branching bisimulation. The known O(mn) algorithms were already far more efficient (both in space and time) than most other algorithms to determine behavioral equivalences (including weak bisimulation), and therefore they were often used as an essential preprocessing step. This new algorithm makes this use of stuttering equivalence and branching bisimulation even more attractive.
Original languageEnglish
Article number13
JournalAcm Transactions on Computational Logic
Volume18
Issue number2
DOIs
Publication statusPublished - 23 Jun 2017

Fingerprint

Bisimulation
Branching
Equivalence
Computing
Time Complexity
Labeled Transition System
Space Complexity
Stretch
Preprocessing

Keywords

  • branching bisimulation
  • algorithm

Cite this

@article{2834e58fc12e463498033c6d920be70c,
title = "An O(m log n) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation",
abstract = "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, where Act is the set of actions in a labeled transition system.Theoretically, our algorithm substantially improves upon existing algorithms, which all have time complexity of the form O(mn) at best. Moreover, it has better or equal space complexity. Practical results confirm these findings: they show that our algorithm can outperform existing algorithms by several orders of magnitude, especially when the Kripke structures are large.The importance of our algorithm stretches far beyond stuttering equivalence and branching bisimulation. The known O(mn) algorithms were already far more efficient (both in space and time) than most other algorithms to determine behavioral equivalences (including weak bisimulation), and therefore they were often used as an essential preprocessing step. This new algorithm makes this use of stuttering equivalence and branching bisimulation even more attractive.",
keywords = "branching bisimulation, algorithm",
author = "J.F. Groote and D.N. Jansen and J.J.A. Keiren and A.J. Wijs",
year = "2017",
month = "6",
day = "23",
doi = "10.1145/3060140",
language = "English",
volume = "18",
journal = "Acm Transactions on Computational Logic",
issn = "1529-3785",
publisher = "Association for Computing Machinery (ACM)",
number = "2",

}

An O(m log n) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation. / Groote, J.F.; Jansen, D.N.; Keiren, J.J.A.; Wijs, A.J.

In: Acm Transactions on Computational Logic, Vol. 18, No. 2, 13, 23.06.2017.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - An O(m log n) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation

AU - Groote, J.F.

AU - Jansen, D.N.

AU - Keiren, J.J.A.

AU - Wijs, A.J.

PY - 2017/6/23

Y1 - 2017/6/23

N2 - 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, where Act is the set of actions in a labeled transition system.Theoretically, our algorithm substantially improves upon existing algorithms, which all have time complexity of the form O(mn) at best. Moreover, it has better or equal space complexity. Practical results confirm these findings: they show that our algorithm can outperform existing algorithms by several orders of magnitude, especially when the Kripke structures are large.The importance of our algorithm stretches far beyond stuttering equivalence and branching bisimulation. The known O(mn) algorithms were already far more efficient (both in space and time) than most other algorithms to determine behavioral equivalences (including weak bisimulation), and therefore they were often used as an essential preprocessing step. This new algorithm makes this use of stuttering equivalence and branching bisimulation even more attractive.

AB - 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, where Act is the set of actions in a labeled transition system.Theoretically, our algorithm substantially improves upon existing algorithms, which all have time complexity of the form O(mn) at best. Moreover, it has better or equal space complexity. Practical results confirm these findings: they show that our algorithm can outperform existing algorithms by several orders of magnitude, especially when the Kripke structures are large.The importance of our algorithm stretches far beyond stuttering equivalence and branching bisimulation. The known O(mn) algorithms were already far more efficient (both in space and time) than most other algorithms to determine behavioral equivalences (including weak bisimulation), and therefore they were often used as an essential preprocessing step. This new algorithm makes this use of stuttering equivalence and branching bisimulation even more attractive.

KW - branching bisimulation

KW - algorithm

U2 - 10.1145/3060140

DO - 10.1145/3060140

M3 - Article

VL - 18

JO - Acm Transactions on Computational Logic

JF - Acm Transactions on Computational Logic

SN - 1529-3785

IS - 2

M1 - 13

ER -