Abstract
Branching bisimilarity is a behavioural equivalence relation on labelled transition systems (LTSs) that takes internal actions into account. It has the traditional advantage that algorithms for branching bisimilarity are more efficient than ones for other weak behavioural equivalences, especially weak bisimilarity. With m the number of transitions and n the number of states, the classic \({O\left( {m n}\right) }\) algorithm was recently replaced by an \(O({m (\log \left| { Act }\right| + \log n)})\) algorithm [9], which is unfortunately rather complex. This paper combines its ideas with the ideas from Valmari [20], resulting in a simpler \(O({m \log n})\) algorithm. Benchmarks show that in practice this algorithm is also faster and often far more memory efficient than its predecessors, making it the best option for branching bisimulation minimisation and preprocessing for calculating other weak equivalences on LTSs.
Chapter PDF
Similar content being viewed by others
References
Bal, H., Epema, D., de Laat, C., van Nieuwpoort, R., Romein, J., Seinstra, F., Snoek, C., Wijshoff, H.: A medium-scale distributed system for computer science research: Infrastructure for the long term. IEEE Computer 49(5), 54–63 (2016). https://doi.org/10.1109/MC.2016.127
Bartholomeus, M., Luttik, B., Willemse, T.: Modelling and analysing ERTMS Hybrid Level 3 with the mCRL2 toolset. In: Howar, F., Barnat, J. (eds.) Formal methods for industrial critical systems: FMICS. LNCS, vol. 11119, pp. 98–114. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-00244-2_7
Blom, S., Orzan, S.: Distributed branching bisimulation reduction of state spaces. Electron. Notes Theor. Comput. Sci. 80(1), 99–113 (2003). https://doi.org/10.1016/S1571-0661(05)80099-4
Brugger, R.M.: A note on unbiased estimation of the standard deviation. The American Statistician 23(4), 32 (1969). https://doi.org/10.1080/00031305.1969.10481865
Bunte, O., Groote, J.F., Keiren, J.J.A., Laveaux, M., Neele, T., de Vink, E.P., Wesselink, W., Wijs, A.J., Willemse, T.A.C.: The mCRL2 toolset for analysing concurrent systems. In: Vojnar, T., Zhang, L. (eds.) Tools and algorithms for the construction and analysis of systems: TACAS, Part II. LNCS, vol. 11428, pp. 21–39. Springer (2019). https://doi.org/10.1007/978-3-030-17465-1_2
De Nicola, R., Vaandrager, F.: Three logics for branching bisimulation. J. ACM 42(2), 458–487 (1995). https://doi.org/10.1145/201019.201032
van Glabbeek, R.J.: The linear time – branching time spectrum II. In: Best, E. (ed.) CONCUR’93: 4th international conference on concurrency theory. LNCS, vol. 715, pp. 66–81. Springer, Berlin (1993). https://doi.org/10.1007/3-540-57208-2_6
van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555–600 (1996). https://doi.org/10.1145/233551.233556
Groote, J.F., Jansen, D.N., Keiren, J.J.A., Wijs, A.J.: An \(O({m \log n})\) algorithm for computing stuttering equivalence and branching bisimulation. ACM Trans. Comput. Logic 18(2), Article 13 (2017). https://doi.org/10.1145/3060140
Groote, J.F., Vaandrager, F.: An efficient algorithm for branching bisimulation and stuttering equivalence. In: Paterson, M.S. (ed.) Automata, languages and programming [ICALP]. LNCS, vol. 443, pp. 626–638. Springer, Berlin (1990). https://doi.org/10.1007/BFb0032063
Groote, J.F., Wijs, A.J.: An \(O(m \log n)\) algorithm for stuttering equivalence and branching bisimulation. In: Chechik, M., Raskin, J.F. (eds.) Tools and algorithms for the construction and analysis of systems: TACAS. LNCS, vol. 9636, pp. 607–624. Springer, Berlin (2016). https://doi.org/10.1007/978-3-662-49674-9_40
Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: 36th annual symposium on foundations of computer science [FOCS]. pp. 453–462. IEEE Comp. Soc., Los Alamitos, Calif. (1995). https://doi.org/10.1109/SFCS.1995.492576
Hopcroft, J.: An \(n \log n\) algorithm for minimizing states in a finite automaton. In: Kohavi, Z., Paz, A. (eds.) Theory of machines and computations, pp. 189–196. Academic Press, New York (1971). https://doi.org/10.1016/B978-0-12-417750-5.50022-1
Jansen, D.N., Groote, J.F., Keiren, J.J.A., Wijs, A.J.: A simpler \(O({m \log n})\) algorithm for branching bisimilarity on labelled transition systems. arXiv preprint 1909.10824 (2019), https://arxiv.org/abs/1909.10824
Jansen, D.N., Groote, J.F., Keiren, J.J.A., Wijs, A.J.: An \(O(m \log n)\) algorithm for branching bisimilarity on labelled transition systems. Figshare (2020), https://doi.org/10.6084/m9.figshare.11876688.v1
Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. 86(1), 43–68 (1990). https://doi.org/10.1016/0890-5401(90)90025-D
Milner, R.: A calculus of communicating systems, LNCS, vol. 92. Springer, Berlin (1980). https://doi.org/10.1007/3-540-10235-3
Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973–989 (1987). https://doi.org/10.1137/0216062
Reniers, M.A., Schoren, R., Willemse, T.A.C.: Results on embeddings between state-based and event-based systems. Comput. J. 57(1), 73–92 (2014). https://doi.org/10.1093/comjnl/bxs156
Valmari, A.: Bisimilarity minimization in \(O(m \log n)\) time. In: Franceschinis, G., Wolf, K. (eds.) Applications and theory of Petri nets: PETRI NETS, LNCS, vol. 5606, pp. 123–142. Springer, Berlin (2009). https://doi.org/10.1007/978-3-642-02424-5_9
Valmari, A., Lehtinen, P.: Efficient minimization of DFAs with partial transition functions. In: Albers, S., Weil, P. (eds.) 25th international symposium on theoretical aspects of computer science: STACS, LIPIcs, vol. 1, pp. 645–656. Schloss Dagstuhl, Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2008). https://doi.org/10.4230/LIPIcs.STACS.2008.1328
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Jansen, D.N., Groote, J.F., Keiren, J.J.A., Wijs, A. (2020). An O(m log n) algorithm for branching bisimilarity on labelled transition systems. In: Biere, A., Parker, D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2020. Lecture Notes in Computer Science(), vol 12079. Springer, Cham. https://doi.org/10.1007/978-3-030-45237-7_1
Download citation
DOI: https://doi.org/10.1007/978-3-030-45237-7_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45236-0
Online ISBN: 978-3-030-45237-7
eBook Packages: Computer ScienceComputer Science (R0)