Document Open Access Logo

A State-Based O(m log n) Partitioning Algorithm for Branching Bisimilarity

Authors Jan Friso Groote , David N. Jansen

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CONCUR.2025.18.pdf
  • Filesize: 0.84 MB
  • 16 pages
HTML5 Logo HTML (experimental)
LIPIcs.CONCUR.2025.18.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Design and analysis of algorithms
  • Software and its engineering → Formal software verification
Keywords
  • Algorithm
  • Branching bisimulation
  • Partition refinement of states

Metrics

Abstract

We present a new O(mlog n) algorithm to calculate branching bisimulation equivalence, which is the finest commonly used behavioural equivalence on labelled transition systems that takes the internal action τ into account. This algorithm combines the simpler data structure of an earlier algorithm for Kripke structures (without action labels) with the memory-efficiency of a later algorithm partitioning sets of labelled transitions. It employs a particularly elegant four-way split of blocks of states, which refines a block under two splitters and isolates all new bottom states, simultaneously. Benchmark results show that this new algorithm outperforms the best known algorithm for branching bisimulation both in time and space.

Cite As Get BibTex

Jan Friso Groote and David N. Jansen. A State-Based O(m log n) Partitioning Algorithm for Branching Bisimilarity. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 18:1-18:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CONCUR.2025.18

Author Details

Jan Friso Groote
  • Department of Computer Science, Eindhoven University of Technology, The Netherlands
David N. Jansen
  • Key Laboratory of System Software, Chinese Academy of Sciences, Beijing, China
  • State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China

Funding

  • Jansen, David N.: This work is supported by ISCAS Basic Research ISCAS-JCZD-202302 and is part of the European Union's Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant no. 101008233.

References

  1. Rocco De Nicola and Frits Vaandrager. Action versus state based logics for transition systems. In I. Guessarian, editor, Semantics of systems of concurrent processes: LITP spring school on theoretical computer science, volume 469 of LNCS, pages 407-419. Springer, Berlin, 1990. URL: https://doi.org/10.1007/3-540-53479-2_17.
  2. Jean-Claude Fernandez. An implementation for an efficient algorithm for bisimulation equivalence. Science of Computer Programming, 13(2-3):219-236, 1990. URL: https://doi.org/10.1016/0167-6423(90)90071-K.
  3. Hubert Garavel and Bas Luttik. Four formal models of IEEE 1394 link layer. In Frédéric Lang and Matthias Volk, editors, Proceedings Sixth Workshop on Models for Formal Analysis of Real System [MARS], volume 399 of EPTCS, pages 21-100, 2024. URL: https://doi.org/10.4204/EPTCS.399.5.
  4. Rob J. van Glabbeek and W. Peter Weijland. Branching time and abstraction in bisimulation semantics. J. ACM, 43(3):555-600, 1996. URL: https://doi.org/10.1145/233551.233556.
  5. Jan Friso Groote, David N. Jansen, Jeroen J.A. Keiren, and Anton J. Wijs. An O(m log n) algorithm for computing stuttering equivalence and branching bisimulation. ACM Trans. Comput. Logic, 18(2):Article 13, 2017. URL: https://doi.org/10.1145/3060140.
  6. Jan Friso Groote and Mohammad Reza Mousavi. Modeling and Analysis of Communicating Systems. MIT Press, 2014. URL: https://mitpress.mit.edu/9780262547871/.
  7. Jan Friso Groote and Frits Vaandrager. An efficient algorithm for branching bisimulation and stuttering equivalence. In M. S. Paterson, editor, Automata, languages and programming [ICALP], volume 443 of LNCS, pages 626-638. Springer, Berlin, 1990. URL: https://doi.org/10.1007/BFb0032063.
  8. Jan Friso Groote and Anton Wijs. An O(m log n) algorithm for stuttering equivalence and branching bisimulation. In Marsha Chechik and Jean-François Raskin, editors, Tools and algorithms for the construction and analysis of systems: TACAS, volume 9636 of LNCS, pages 607-624. Springer, Berlin, 2016. URL: https://doi.org/10.1007/978-3-662-49674-9_40.
  9. Jules Jacobs and Thorsten Wißmann. Fast coalgebraic bisimilarity minimization. Proc. ACM Program. Lang., 7(POPL):1514-1541, 2023. URL: https://doi.org/10.1145/3571245.
  10. David N. Jansen, Jan Friso Groote, Jeroen J.A. Keiren, and Anton Wijs. An O(m log n) algorithm for branching bisimilarity on labelled transition systems. In Armin Biere and David Parker, editors, Tools and Algorithms for the Construction and Analysis of Systems: TACAS, Part II, volume 12079 of LNCS, pages 3-20. Springer, Cham, 2020. URL: https://doi.org/10.1007/978-3-030-45237-7_1.
  11. Robin Milner. A Calculus of Communicating Systems, volume 92 of LNCS. Springer, Berlin, 1980. URL: https://doi.org/10.1007/3-540-10235-3.
  12. Robert Paige and Robert E. Tarjan. Three partition refinement algorithms. SIAM J. Comput. , 16(6):973-989, 1987. URL: https://doi.org/10.1137/0216062.
  13. Robert Tarjan. Depth-first search and linear graph algorithms. SIAM J. Comput., 1(2):146-160, 1972. URL: https://doi.org/10.1137/0201010.
  14. Antti Valmari. Bisimilarity minimization in O(m log n) time. In Giuliana Franceschinis and Karsten Wolf, editors, Applications and Theory of Petri Nets: PETRI NETS, volume 5606 of LNCS, pages 123-142. Springer, Berlin, 2009. URL: https://doi.org/10.1007/978-3-642-02424-5_9.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact