{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T21:38:53Z","timestamp":1768253933809,"version":"3.49.0"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2022,12,6]],"date-time":"2022-12-06T00:00:00Z","timestamp":1670284800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,12,6]],"date-time":"2022-12-06T00:00:00Z","timestamp":1670284800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100003246","name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["AVVA project 612.001751"],"award-info":[{"award-number":["AVVA project 612.001751"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003246","name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["TTW ChEOPS project 17249"],"award-info":[{"award-number":["TTW ChEOPS project 17249"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2023,4]]},"abstract":"Abstract<\/jats:title>We present the first parallel algorithms that decide strong and branching bisimilarity in linear time. More precisely, if a transition system has n<\/jats:italic> states, m<\/jats:italic> transitions and $$\\vert Act \\vert $$<\/jats:tex-math>\n \n |<\/mml:mo>\n A<\/mml:mi>\n c<\/mml:mi>\n t<\/mml:mi>\n |<\/mml:mo>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> action labels, we introduce an algorithm that decides strong bisimilarity in $$\\mathcal {O}(n+\\vert Act \\vert )$$<\/jats:tex-math>\n \n O<\/mml:mi>\n (<\/mml:mo>\n n<\/mml:mi>\n +<\/mml:mo>\n |<\/mml:mo>\n A<\/mml:mi>\n c<\/mml:mi>\n t<\/mml:mi>\n |<\/mml:mo>\n )<\/mml:mo>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> time on $$\\max (n,m)$$<\/jats:tex-math>\n \n max<\/mml:mo>\n (<\/mml:mo>\n n<\/mml:mi>\n ,<\/mml:mo>\n m<\/mml:mi>\n )<\/mml:mo>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> processors and an algorithm that decides branching bisimilarity in $$\\mathcal {O}(n+\\vert Act \\vert )$$<\/jats:tex-math>\n \n O<\/mml:mi>\n (<\/mml:mo>\n n<\/mml:mi>\n +<\/mml:mo>\n |<\/mml:mo>\n A<\/mml:mi>\n c<\/mml:mi>\n t<\/mml:mi>\n |<\/mml:mo>\n )<\/mml:mo>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> time using up to $$\\max (n^2,m,\\vert Act \\vert n)$$<\/jats:tex-math>\n \n max<\/mml:mo>\n (<\/mml:mo>\n \n n<\/mml:mi>\n 2<\/mml:mn>\n <\/mml:msup>\n ,<\/mml:mo>\n m<\/mml:mi>\n ,<\/mml:mo>\n |<\/mml:mo>\n A<\/mml:mi>\n c<\/mml:mi>\n t<\/mml:mi>\n |<\/mml:mo>\n n<\/mml:mi>\n )<\/mml:mo>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> processors.\n<\/jats:p>","DOI":"10.1007\/s10270-022-01060-7","type":"journal-article","created":{"date-parts":[[2022,12,6]],"date-time":"2022-12-06T14:06:40Z","timestamp":1670335600000},"page":"521-545","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Linear parallel algorithms to compute strong and branching bisimilarity"],"prefix":"10.1007","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4797-7735","authenticated-orcid":false,"given":"Jan","family":"Martens","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2196-6587","authenticated-orcid":false,"given":"Jan Friso","family":"Groote","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0330-5016","authenticated-orcid":false,"given":"Lars B. van den","family":"Haak","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5716-1118","authenticated-orcid":false,"given":"Pieter","family":"Hijma","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2071-9624","authenticated-orcid":false,"given":"Anton","family":"Wijs","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,12,6]]},"reference":[{"key":"1060_CR1","doi-asserted-by":"publisher","unstructured":"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\u2014improvements in expressivity and usability. In: Tools and Algorithms for the Construction and Analysis of Systems\u201425th International Conference (TACAS 2019), Proceedings, Part II, pp. 21\u201339 (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_2","DOI":"10.1007\/978-3-030-17465-1_2"},{"key":"1060_CR2","volume-title":"A Calculus of Communicating Systems. Lecture Notes in Computer Science","author":"R Milner","year":"1980","unstructured":"Milner, R.: A Calculus of Communicating Systems. Lecture Notes in Computer Science, vol. 92. Springer, Cham (1980)"},{"issue":"1","key":"1060_CR3","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"P Kanellakis","year":"1990","unstructured":"Kanellakis, P., Smolka, S.: CCS expressions, finite state processes, and three problems of equivalence. Information and Computation 86(1), 43\u201368 (1990). https:\/\/doi.org\/10.1016\/0890-5401(90)90025-D","journal-title":"Information and Computation"},{"issue":"6","key":"1060_CR4","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R Paige","year":"1987","unstructured":"Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM Journal on Computing 16(6), 973\u2013989 (1987). https:\/\/doi.org\/10.1137\/0216062","journal-title":"SIAM Journal on Computing"},{"key":"1060_CR5","doi-asserted-by":"publisher","DOI":"10.1126\/science.aam9744","author":"CE Leiserson","year":"2020","unstructured":"Leiserson, C.E., Thompson, N.C., Emer, J.S., Kuszmaul, B.C., Lampson, B.W., Sanchez, D., Schardl, T.B.: There\u2019s plenty of room at the top: What will drive computer performance after Moore\u2019s law? Science (2020). https:\/\/doi.org\/10.1126\/science.aam9744","journal-title":"Science"},{"key":"1060_CR6","unstructured":"Groote, J.F., Martens, J., de Vink, E.P.: Lowerbounds for bisimulation by partition refinement. pre-print (2022). arXiv:2203.07158"},{"issue":"3","key":"1060_CR7","doi-asserted-by":"publisher","first-page":"319","DOI":"10.3233\/FI-2010-369","volume":"105","author":"A Valmari","year":"2010","unstructured":"Valmari, A.: Simple bisimilarity minimization in $$O(m \\log n)$$ time. Fundam. Informaticae 105(3), 319\u2013339 (2010). https:\/\/doi.org\/10.3233\/FI-2010-369","journal-title":"Fundam. Informaticae"},{"issue":"2","key":"1060_CR8","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1137\/0213027","volume":"13","author":"L Stockmeyer","year":"1984","unstructured":"Stockmeyer, L., Vishkin, U.: Simulation of parallel random access machines by circuits. SIAM J. Comput. 13(2), 409\u2013422 (1984). https:\/\/doi.org\/10.1137\/0213027","journal-title":"SIAM J. Comput."},{"key":"1060_CR9","doi-asserted-by":"publisher","unstructured":"Martens, J., Groote, J.F., Haak, L.v.d., Hijma, P., Wijs, A.: A linear parallel algorithm to compute bisimulation and relational coarsest partitions. In: International Conference on Formal Aspects of Component Software, pp. 115\u2013133. Springer, Berlin (2021). https:\/\/doi.org\/10.1007\/978-3-030-90636-8_7","DOI":"10.1007\/978-3-030-90636-8_7"},{"key":"1060_CR10","doi-asserted-by":"publisher","unstructured":"Fortune, S., Wyllie, J.: Parallelism in random access machines. In: Proceedings of the Tenth Annual ACM Symposium on Theory of Computing, pp. 114\u2013118 (1978). https:\/\/doi.org\/10.1145\/800133.804339","DOI":"10.1145\/800133.804339"},{"key":"1060_CR11","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-45237-7_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"DN Jansen","year":"2020","unstructured":"Jansen, D.N., Groote, J.F., Keiren, F.J.A., Wijs, A.J.: 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, vol. 12079, pp. 3\u201320. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_1"},{"key":"1060_CR12","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/3-540-58179-0_71","volume-title":"Computer Aided Verification","author":"I Lee","year":"1994","unstructured":"Lee, I., Rajasekaran, S.: A parallel algorithm for relational coarsest partition problems and its implementation. In: Dill, D.L. (ed.) Computer Aided Verification, vol. 818, pp. 404\u2013414. Springer, Cham (1994). https:\/\/doi.org\/10.1007\/3-540-58179-0_71"},{"key":"1060_CR13","doi-asserted-by":"publisher","unstructured":"De\u00a0Nicola, R., Vaandrager, F.: Action versus state based logics for transition systems. In: LITP Spring School on Theoretical Computer Science, pp. 407\u2013419. Springer (1990). https:\/\/doi.org\/10.1007\/3-540-53479-2_17","DOI":"10.1007\/3-540-53479-2_17"},{"key":"1060_CR14","doi-asserted-by":"publisher","unstructured":"Wijs, A.J.: GPU accelerated strong and branching bisimilarity checking. In: TACAS. Lecture Notes in Computer Science, vol. 9035, pp. 368\u2013383. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_29","DOI":"10.1007\/978-3-662-46681-0_29"},{"issue":"3","key":"1060_CR15","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/s10703-016-0246-7","volume":"48","author":"AJ Wijs","year":"2016","unstructured":"Wijs, A.J., Katoen, J.-P., Bo\u0161na\u010dki, D.: Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components. Formal Methods Syst. Design 48(3), 274\u2013300 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0246-7","journal-title":"Formal Methods Syst. Design"},{"issue":"1","key":"1060_CR16","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1093\/comjnl\/bxs156","volume":"57","author":"MA Reniers","year":"2014","unstructured":"Reniers, M.A., Schoren, R., Willemse, T.A.C.: Results on embeddings between state-based and event-based systems. Comput. J. 57(1), 73\u201392 (2014). https:\/\/doi.org\/10.1093\/comjnl\/bxs156","journal-title":"Comput. J."},{"key":"1060_CR17","doi-asserted-by":"publisher","unstructured":"Sengupta, S., Harris, M., Garland, M., Owens, J.: Efficient Parallel Scan Algorithms for Manycore GPUs. In: Scientific Computing with Multicore and Accelerators, pp. 413\u2013442. Taylor & Francis, Boca Raton (2011). Chap. 19. https:\/\/doi.org\/10.1201\/b10376","DOI":"10.1201\/b10376"},{"issue":"1","key":"1060_CR18","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/S1571-0661(05)80099-4","volume":"89","author":"S Blom","year":"2003","unstructured":"Blom, S., Orzan, S.: Distributed branching bisimulation reduction of state spaces. Electron. Notes Theor. Comput. Sci. 89(1), 99\u2013113 (2003). https:\/\/doi.org\/10.1016\/S1571-0661(05)80099-4","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"3","key":"1060_CR19","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"RJ Van Glabbeek","year":"1996","unstructured":"Van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. JACM 43(3), 555\u2013600 (1996). https:\/\/doi.org\/10.1145\/233551.233556","journal-title":"JACM"},{"key":"1060_CR20","doi-asserted-by":"publisher","unstructured":"Groote, J.F., Vaandrager, F.: An efficient algorithm for branching bisimulation and stuttering equivalence. In: International Colloquium on Automata, Languages, and Programming, pp. 626\u2013638. Springer, Cham (1990). https:\/\/doi.org\/10.1007\/BFb0032063","DOI":"10.1007\/BFb0032063"},{"issue":"1","key":"1060_CR21","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"MC Browne","year":"1988","unstructured":"Browne, M.C., Clarke, E.M., Gr\u00fcmberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theor. Comput. Sci. 59(1), 115\u2013131 (1988). https:\/\/doi.org\/10.1016\/0304-3975(88)90098-9","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"1060_CR22","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1186\/1471-2105-13-281","volume":"13","author":"D Bo\u0161na\u010dki","year":"2012","unstructured":"Bo\u0161na\u010dki, D., Odenbrett, M.R., Wijs, A., Ligtenberg, W., Hilbers, P.: Efficient reconstruction of biological networks via transitive reduction on general purpose graphics processors. BMC Bioinform. 13(1), 281 (2012). https:\/\/doi.org\/10.1186\/1471-2105-13-281","journal-title":"BMC Bioinform."},{"key":"1060_CR23","doi-asserted-by":"publisher","unstructured":"Han, Y., Pan, V., Reif, J.: Efficient parallel algorithms for computing all pair shortest paths in directed graphs. In: Proceedings of the Fourth Annual ACM Symposium on Parallel Algorithms and Architectures, pp. 353\u2013362 (1992). https:\/\/doi.org\/10.1145\/140901.141913","DOI":"10.1145\/140901.141913"},{"issue":"1","key":"1060_CR24","doi-asserted-by":"publisher","first-page":"638","DOI":"10.1007\/BF03180566","volume":"4","author":"J Balc\u00e1zar","year":"1992","unstructured":"Balc\u00e1zar, J., Gabarro, J., Santha, M.: Deciding bisimilarity is P-complete. Formal Aspects Comput. 4(1), 638\u2013648 (1992). https:\/\/doi.org\/10.1007\/BF03180566","journal-title":"Formal Aspects Comput."},{"issue":"7","key":"1060_CR25","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1109\/71.707548","volume":"9","author":"S Rajasekaran","year":"1998","unstructured":"Rajasekaran, S., Lee, I.: Parallel algorithms for relational coarsest partition problems. IEEE Trans. Parallel Distrib. Syst. 9(7), 687\u2013699 (1998). https:\/\/doi.org\/10.1109\/71.707548","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"1060_CR26","unstructured":"Jeong, C., Kim, Y., Oh, Y., Kim, H.: A faster parallel implementation of Kanellakis\u2013Smolka algorithm for bisimilarity checking. In: Proceedings of the International Computer Symposium. Citeseer (1998)"},{"key":"1060_CR27","doi-asserted-by":"publisher","unstructured":"Blom, S., van\u00a0de Pol, J.: Distributed branching bisimulation minimization by inductive signatures. In: Brim, L., van\u00a0de Pol, J. (eds.) Proceedings 8th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2009, Eindhoven, The Netherlands, 4th November 2009. EPTCS, vol. 14, pp. 32\u201346 (2009). https:\/\/doi.org\/10.4204\/EPTCS.14.3","DOI":"10.4204\/EPTCS.14.3"},{"key":"1060_CR28","doi-asserted-by":"crossref","unstructured":"Tewari, A., Srivastava, U., Gupta, P.: A parallel DFA minimization algorithm. In: International Conference on High-Performance Computing, pp. 34\u201340. Springer, Berlin (2002)","DOI":"10.1007\/3-540-36265-7_4"},{"issue":"3","key":"1060_CR29","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/s00236-019-00363-5","volume":"58","author":"J Bj\u00f6rklund","year":"2021","unstructured":"Bj\u00f6rklund, J., Cleophas, L.: Aggregation-based minimization of finite state automata. Acta Informatica 58(3), 177\u2013194 (2021)","journal-title":"Acta Informatica"},{"key":"1060_CR30","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/0304-3975(85)90159-8","volume":"40","author":"R Paige","year":"1985","unstructured":"Paige, R., Tarjan, R.E., Bonic, R.: A linear time solution to the single function coarsest partition problem. Theor. Comput. Sci. 40, 67\u201384 (1985)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"1060_CR31","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/0304-3975(94)90030-2","volume":"129","author":"JF J\u00e1J\u00e1","year":"1994","unstructured":"J\u00e1J\u00e1, J.F., Ryu, K.W.: An efficient parallel algorithm for the single function coarsest partition problem. Theor. Comput. Sci. 129(2), 293\u2013307 (1994)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"1060_CR32","doi-asserted-by":"publisher","first-page":"770","DOI":"10.1137\/0217049","volume":"17","author":"R Cole","year":"1988","unstructured":"Cole, R.: Parallel merge sort. SIAM J. Comput. 17(4), 770\u2013785 (1988)","journal-title":"SIAM J. Comput."}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-022-01060-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-022-01060-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-022-01060-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,31]],"date-time":"2023-03-31T06:09:47Z","timestamp":1680242987000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-022-01060-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12,6]]},"references-count":32,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,4]]}},"alternative-id":["1060"],"URL":"https:\/\/doi.org\/10.1007\/s10270-022-01060-7","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,12,6]]},"assertion":[{"value":"6 April 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 August 2022","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 September 2022","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 December 2022","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}