{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T12:42:04Z","timestamp":1773060124933,"version":"3.50.1"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030906351","type":"print"},{"value":"9783030906368","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,10,28]],"date-time":"2021-10-28T00:00:00Z","timestamp":1635379200000},"content-version":"vor","delay-in-days":300,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The most efficient way to calculate strong bisimilarity is by finding the relational coarsest partition of a transition system. We provide the first linear-time algorithm to calculate strong bisimulation using parallel random access machines (PRAMs). More precisely, with<jats:italic>n<\/jats:italic>states,<jats:italic>m<\/jats:italic>transitions and<jats:inline-formula><jats:alternatives><jats:tex-math>$$| Act |\\le m$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mo>|<\/mml:mo><mml:mi>A<\/mml:mi><mml:mi>c<\/mml:mi><mml:mi>t<\/mml:mi><mml:mo>|<\/mml:mo><mml:mo>\u2264<\/mml:mo><mml:mi>m<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>action labels, we provide an algorithm for<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\max (n,m)$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mo>max<\/mml:mo><mml:mo>(<\/mml:mo><mml:mi>n<\/mml:mi><mml:mo>,<\/mml:mo><mml:mi>m<\/mml:mi><mml:mo>)<\/mml:mo><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>processors that calculates strong bisimulation in time<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathcal {O}(n+| Act |)$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>O<\/mml:mi><mml:mo>(<\/mml:mo><mml:mi>n<\/mml:mi><mml:mo>+<\/mml:mo><mml:mo>|<\/mml:mo><mml:mi>A<\/mml:mi><mml:mi>c<\/mml:mi><mml:mi>t<\/mml:mi><mml:mo>|<\/mml:mo><mml:mo>)<\/mml:mo><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>and space<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathcal {O}(n+m)$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>O<\/mml:mi><mml:mo>(<\/mml:mo><mml:mi>n<\/mml:mi><mml:mo>+<\/mml:mo><mml:mi>m<\/mml:mi><mml:mo>)<\/mml:mo><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>. The best-known PRAM algorithm has time complexity<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathcal {O}(n\\log n)$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>O<\/mml:mi><mml:mo>(<\/mml:mo><mml:mi>n<\/mml:mi><mml:mo>log<\/mml:mo><mml:mi>n<\/mml:mi><mml:mo>)<\/mml:mo><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>on a smaller number of processors making it less suitable for massive parallel devices such as GPUs. An implementation on a GPU shows that the linear time-bound is achievable on contemporary hardware.<\/jats:p>","DOI":"10.1007\/978-3-030-90636-8_7","type":"book-chapter","created":{"date-parts":[[2021,11,4]],"date-time":"2021-11-04T09:02:36Z","timestamp":1636016556000},"page":"115-133","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["A Linear Parallel Algorithm to Compute Bisimulation and Relational Coarsest Partitions"],"prefix":"10.1007","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","family":"van den 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":[[2021,10,28]]},"reference":[{"issue":"1","key":"7_CR1","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":"1","key":"7_CR2","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. Electr. Notes Theoret. Comput. Sci. 89(1), 99\u2013113 (2003). https:\/\/doi.org\/10.1016\/S1571-0661(05)80099-4","journal-title":"Electr. Notes Theoret. Comput. Sci."},{"key":"7_CR3","doi-asserted-by":"publisher","unstructured":"Blom, S., van de Pol, J.: Distributed branching bisimulation minimization by inductive signatures. In: Brim, L., van de 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":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-030-17465-1_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O Bunte","year":"2019","unstructured":"Bunte, O., et al.: The mCRL2 toolset for analysing concurrent systems. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 21\u201339. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_2"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/3-540-53479-2_17","volume-title":"Semantics of Systems of Concurrent Processes","author":"R De Nicola","year":"1990","unstructured":"De Nicola, R., Vaandrager, F.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407\u2013419. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-53479-2_17"},{"key":"7_CR6","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"},{"issue":"3","key":"7_CR7","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. J. ACM 43(3), 555\u2013600 (1996). https:\/\/doi.org\/10.1145\/233551.233556","journal-title":"J. ACM"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1007\/978-3-662-49674-9_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JF Groote","year":"2016","unstructured":"Groote, J.F., Wijs, A.: An $$O(m\\log n)$$ algorithm for stuttering equivalence and branching bisimulation. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 607\u2013624. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_40"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","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, J.J.A., Wijs, A.: An O(m\u00a0log\u00a0n) algorithm for branching bisimilarity on labelled transition systems. In: TACAS 2020. LNCS, vol. 12079, pp. 3\u201320. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_1"},{"key":"7_CR10","unstructured":"Jeong, C., Kim, Y., Oh, Y., Kim, H.: A faster parallel implementation of Kanellakis-Smolka algorithm for bisimilarity checking. In: Proceedings of the International Computer Symposium. Citeseer (1998)"},{"issue":"1","key":"7_CR11","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. Inf. Comput. 86(1), 43\u201368 (1990). https:\/\/doi.org\/10.1016\/0890-5401(90)90025-D","journal-title":"Inf. Comput."},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","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.) CAV 1994. LNCS, vol. 818, pp. 404\u2013414. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58179-0_71"},{"key":"7_CR13","doi-asserted-by":"publisher","unstructured":"Leiserson, C.E., et al.: There\u2019s plenty of room at the top: what will drive computer performance after Moore\u2019s law? Science 368(6495) (2020). https:\/\/doi.org\/10.1126\/science.aam9744","DOI":"10.1126\/science.aam9744"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Martens, J., Groote, J., Haak, L.v.d., Hijma, P., Wijs, A.: A linear parallel algorithm to compute bisimulation and relational coarsest partitions. arXiv preprint arXiv:2105.11788 (2021)","DOI":"10.1007\/s10270-022-01060-7"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","year":"1980","unstructured":"Milner, R. (ed.): A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980). https:\/\/doi.org\/10.1007\/3-540-10235-3"},{"issue":"6","key":"7_CR16","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 J. Comput. 16(6), 973\u2013989 (1987). https:\/\/doi.org\/10.1137\/0216062","journal-title":"SIAM J. Comput."},{"issue":"7","key":"7_CR17","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."},{"issue":"1","key":"7_CR18","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.: 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":"7_CR19","unstructured":"Sengupta, S., Harris, M., Garland, M., Owens, J.: Efficient parallel scan algorithms for GPUs. In: Scientific Computing with Multicore and Accelerators, chap. 19, pp. 413\u2013442. Taylor & Francis (2011)"},{"issue":"2","key":"7_CR20","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."},{"issue":"3","key":"7_CR21","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"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-662-46681-0_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Wijs","year":"2015","unstructured":"Wijs, A.: GPU accelerated strong and branching bisimilarity checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 368\u2013383. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_29"},{"issue":"3","key":"7_CR23","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/s10703-016-0246-7","volume":"48","author":"A Wijs","year":"2016","unstructured":"Wijs, A., 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. Des. 48(3), 274\u2013300 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0246-7","journal-title":"Formal Methods Syst. Des."}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Component Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-90636-8_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,14]],"date-time":"2023-01-14T13:11:56Z","timestamp":1673701916000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-90636-8_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030906351","9783030906368"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-90636-8_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"28 October 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FACS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Aspects of Component Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 October 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 October 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"facs2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/facs2021.inria.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"44% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1,7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}