An \(O(m \log n)\) algorithm for branching bisimilarity on labelled transition systems. (English) Zbl 1483.68232
Biere, Armin (ed.) et al., Tools and algorithms for the construction and analysis of systems. 26th international conference, TACAS 2020, held as part of the European joint conferences on theory and practice of software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12079, 3-20 (2020).
Summary: 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
[the authors, ACM Trans. Comput. Log. 18, No. 2, Article No. 13, 34 p. (2017; Zbl 1367.68211)],
which is unfortunately rather complex. This paper combines its ideas with the ideas from
[A. Valmari, Lect. Notes Comput. Sci. 5606, 123–142 (2009; Zbl 1242.68186)],
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.
For the entire collection see [Zbl 1471.68010].
For the entire collection see [Zbl 1471.68010].
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 68W40 | Analysis of algorithms |
References:
| [1] | 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 · Zbl 0293.94022 |
| [2] | 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 · Zbl 1242.68186 |
| [3] | 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 · Zbl 1259.68115 |
| [4] | 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 · doi:10.1093/comjnl/bxs156 |
| [5] | Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973-989 (1987). https://doi.org/10.1137/0216062 · Zbl 0654.68072 · doi:10.1137/0216062 |
| [6] | Milner, R.: A calculus of communicating systems, LNCS, vol. 92. Springer, Berlin (1980). https://doi.org/10.1007/3-540-10235-3 · Zbl 0452.68027 |
| [7] | 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 · Zbl 0705.68063 · doi:10.1016/0890-5401(90)90025-D |
| [8] | 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 |
| [9] | 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 |
| [10] | 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 · Zbl 0938.68538 |
| [11] | 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 · Zbl 1420.68146 |
| [12] | 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 · Zbl 0765.68125 |
| [13] | 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 · Zbl 1367.68211 |
| [14] | 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 · Zbl 0882.68085 · doi:10.1145/233551.233556 |
| [15] | 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 |
| [16] | De Nicola, R., Vaandrager, F.: Three logics for branching bisimulation. J. ACM 42(2), 458-487 (1995). https://doi.org/10.1145/201019.201032 · Zbl 0886.68064 · doi:10.1145/201019.201032 |
| [17] | 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 |
| [18] | 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 · doi:10.1080/00031305.1969.10481865 |
| [19] | 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 · Zbl 1271.68133 · doi:10.1016/S1571-0661(05)80099-4 |
| [20] | 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 |
| [21] | 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 · doi:10.1109/MC.2016.127 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
