{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,5]],"date-time":"2026-01-05T22:06:01Z","timestamp":1767650761777,"version":"3.41.0"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2017,4,30]],"date-time":"2017-04-30T00:00:00Z","timestamp":1493510400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2017,4,30]]},"abstract":"<jats:p>\n            We provide a new algorithm to determine stuttering equivalence with time complexity\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>m<\/jats:italic>\n            log\n            <jats:italic>n<\/jats:italic>\n            ), where\n            <jats:italic>n<\/jats:italic>\n            is the number of states and\n            <jats:italic>m<\/jats:italic>\n            is the number of transitions of a Kripke structure. This algorithm can also be used to determine branching bisimulation in\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>m<\/jats:italic>\n            (log |\n            <jats:italic>Act<\/jats:italic>\n            | + log\n            <jats:italic>n<\/jats:italic>\n            )) time, where\n            <jats:italic>Act<\/jats:italic>\n            is the set of actions in a labeled transition system.\n          <\/jats:p>\n          <jats:p>\n            Theoretically, our algorithm substantially improves upon existing algorithms, which all have time complexity of the form\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>mn<\/jats:italic>\n            ) at best. Moreover, it has better or equal space complexity. Practical results confirm these findings: they show that our algorithm can outperform existing algorithms by several orders of magnitude, especially when the Kripke structures are large.\n          <\/jats:p>\n          <jats:p>\n            The importance of our algorithm stretches far beyond stuttering equivalence and branching bisimulation. The known\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>mn<\/jats:italic>\n            ) algorithms were already far more efficient (both in space and time) than most other algorithms to determine behavioral equivalences (including weak bisimulation), and therefore they were often used as an essential preprocessing step. This new algorithm makes this use of stuttering equivalence and branching bisimulation even more attractive.\n          <\/jats:p>","DOI":"10.1145\/3060140","type":"journal-article","created":{"date-parts":[[2017,6,26]],"date-time":"2017-06-26T12:13:22Z","timestamp":1498479202000},"page":"1-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":34,"title":["An\n            <i>O<\/i>\n            (\n            <i>m<\/i>\n            log\n            <i>n<\/i>\n            ) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation"],"prefix":"10.1145","volume":"18","author":[{"given":"Jan Friso","family":"Groote","sequence":"first","affiliation":[{"name":"Eindhoven University of Technology, MB Eindhoven, The Netherlands"}]},{"given":"David N.","family":"Jansen","sequence":"additional","affiliation":[{"name":"Radboud Universiteit Nijmegen"}]},{"given":"Jeroen J. A.","family":"Keiren","sequence":"additional","affiliation":[{"name":"Open University of the Netherlands and Radboud Universiteit Nijmegen, The Netherlands"}]},{"given":"Anton J.","family":"Wijs","sequence":"additional","affiliation":[{"name":"Eindhoven University of Technology, MB Eindhoven, The Netherlands"}]}],"member":"320","published-online":{"date-parts":[[2017,6,23]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Ullman","author":"Aho Alfred V.","year":"1974","unstructured":"Alfred V. Aho , John E. Hopcroft , and Jeffrey D . Ullman . 1974 . The Design and Analysis of Computer Algorithms. Addison-Wesley , Reading, MA. Alfred V. Aho, John E. Hopcroft, and Jeffrey D. Ullman. 1974. The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading, MA."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2016.127"},{"key":"e_1_2_1_3_1","volume-title":"Special issue: PDMC","author":"Blom Stefan","year":"2003","unstructured":"Stefan Blom and Simona Orzan . 2003. Distributed branching bisimulation reduction of state spaces. Electron. Notes Theor. Comput. Sci. 80, 1 , Special issue: PDMC 2003 , Parallel and distributed model checking (2003), 99--113. Stefan Blom and Simona Orzan. 2003. Distributed branching bisimulation reduction of state spaces. Electron. Notes Theor. Comput. Sci. 80, 1, Special issue: PDMC 2003, Parallel and distributed model checking (2003), 99--113."},{"key":"e_1_2_1_4_1","volume-title":"Electronic Proceedings in Theoretical Computer Science","volume":"14","author":"Blom Stefan","unstructured":"Stefan Blom and Jaco van de Pol. 2009. Distributed branching bisimulation minimization by inductive signatures. In Parallel and Distributed Methods in verifiCation (PDMC\u201909), Lubos Brim and Jaco van de Pol (Eds.) . Electronic Proceedings in Theoretical Computer Science , Vol. 14 . Open Publ. Assoc., 32--46. Stefan Blom and Jaco van de Pol. 2009. Distributed branching bisimulation minimization by inductive signatures. In Parallel and Distributed Methods in verifiCation (PDMC\u201909), Lubos Brim and Jaco van de Pol (Eds.). Electronic Proceedings in Theoretical Computer Science, Vol. 14. Open Publ. Assoc., 32--46."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90098-9"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/2133036.2133137"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_15"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32943-2_16"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/201019.201032"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_19"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(90)90071-K"},{"key":"e_1_2_1_12_1","volume-title":"CADP 2011: A toolbox for the construction and analysis of distributed processes. Softw. Tools Technol. Transf. 15, 2, Special issue: TACAS 2011","author":"Garavel Hubert","year":"2012","unstructured":"Hubert Garavel , Fr\u00e9d\u00e9ric Lang , Radu Mateescu , and Wendelin Serwe . 2012 . CADP 2011: A toolbox for the construction and analysis of distributed processes. Softw. Tools Technol. Transf. 15, 2, Special issue: TACAS 2011 (2012), 98--107. Hubert Garavel, Fr\u00e9d\u00e9ric Lang, Radu Mateescu, and Wendelin Serwe. 2012. CADP 2011: A toolbox for the construction and analysis of distributed processes. Softw. Tools Technol. Transf. 15, 2, Special issue: TACAS 2011 (2012), 98--107."},{"key":"e_1_2_1_13_1","first-page":"4","article-title":"Computation tree logic with deadlock detection","volume":"5","author":"van Glabbeek Rob J.","year":"2009","unstructured":"Rob J. van Glabbeek , Bas Luttik , and Nikola Tr\u010dka . 2009 . Computation tree logic with deadlock detection . Logical Methods Comput. Sci. 5 , 4 (Dec. 2009), 1--24. Rob J. van Glabbeek, Bas Luttik, and Nikola Tr\u010dka. 2009. Computation tree logic with deadlock detection. Logical Methods Comput. Sci. 5, 4 (Dec. 2009), 1--24.","journal-title":"Logical Methods Comput. Sci."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/233551.233556"},{"volume-title":"Modeling and Analysis of Communicating Systems. MIT Pr","author":"Groote Jan Friso","key":"e_1_2_1_15_1","unstructured":"Jan Friso Groote and Mohammad Reza Mousavi . 2014. Modeling and Analysis of Communicating Systems. MIT Pr ., Cambridge, MA . Jan Friso Groote and Mohammad Reza Mousavi. 2014. Modeling and Analysis of Communicating Systems. MIT Pr., Cambridge, MA."},{"volume-title":"Automata, Languages and Programming (ICALP\u201990)","author":"Groote Jan Friso","key":"e_1_2_1_16_1","unstructured":"Jan Friso Groote and Frits Vaandrager . 1990. An efficient algorithm for branching bisimulation and stuttering equivalence . In Automata, Languages and Programming (ICALP\u201990) , M. S. Paterson (Ed.). LNCS, Vol . 443. Springer , Berlin, 626--638. Jan Friso Groote and Frits Vaandrager. 1990. An efficient algorithm for branching bisimulation and stuttering equivalence. In Automata, Languages and Programming (ICALP\u201990), M. S. Paterson (Ed.). LNCS, Vol. 443. Springer, Berlin, 626--638."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_40"},{"volume-title":"Theory of Machines and Computations","author":"Hopcroft John E.","key":"e_1_2_1_18_1","unstructured":"John E. Hopcroft . 1971. An nlogn algorithm for minimizing states in a finite automaton . In Theory of Machines and Computations , Z. Kohavi and A. Paz (Eds.). Academic Press , New York , 189--196. John E. Hopcroft. 1971. An nlogn algorithm for minimizing states in a finite automaton. In Theory of Machines and Computations, Z. Kohavi and A. Paz (Eds.). Academic Press, New York, 189--196."},{"key":"e_1_2_1_19_1","volume-title":"Keiren","author":"Jansen David N.","year":"2016","unstructured":"David N. Jansen and Jeroen J. A . Keiren . 2016 . Stuttering Equivalence Is Too Slow&excl; arXiv E-print 1603.05789. http:\/\/arxiv.org\/abs\/1603.05789. David N. Jansen and Jeroen J. A. Keiren. 2016. Stuttering Equivalence Is Too Slow&excl; arXiv E-print 1603.05789. http:\/\/arxiv.org\/abs\/1603.05789."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90025-D"},{"key":"e_1_2_1_21_1","first-page":"83","article-title":"Semantical considerations on modal logic","volume":"16","author":"Kripke Saul","year":"1963","unstructured":"Saul Kripke . 1963 . Semantical considerations on modal logic . Acta Philosophica Fennica 16 (1963), 83 -- 94 . Saul Kripke. 1963. Semantical considerations on modal logic. Acta Philosophica Fennica 16 (1963), 83--94.","journal-title":"Acta Philosophica Fennica"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2009.47"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/539036"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1137\/0216062"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2008.01.001"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxs156"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02424-5_9"},{"key":"e_1_2_1_28_1","volume-title":"25th International Symposium on Theoretical Aspects of Computer Science (STACS\u201908)","volume":"1","author":"Valmari Antti","year":"2008","unstructured":"Antti Valmari and Petri Lehtinen . 2008 . Efficient minimization of DFAs with partial transition functions . In 25th International Symposium on Theoretical Aspects of Computer Science (STACS\u201908) , Susanne Albers and Pascal Weil (Eds.). LIPIcs , Vol. 1 . Schloss Dagstuhl, Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 645--656. Antti Valmari and Petri Lehtinen. 2008. Efficient minimization of DFAs with partial transition functions. In 25th International Symposium on Theoretical Aspects of Computer Science (STACS\u201908), Susanne Albers and Pascal Weil (Eds.). LIPIcs, Vol. 1. Schloss Dagstuhl, Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 645--656."},{"volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201904), Kurt Jensen and Andreas Podelski (Eds.). LNCS","author":"Virtanen Heikki","key":"e_1_2_1_29_1","unstructured":"Heikki Virtanen , Henri Hansen , Antti Valmari , Juha Nieminen , and Timo Erkkil\u00e4 . 2004. Tampere verification tool . In Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201904), Kurt Jensen and Andreas Podelski (Eds.). LNCS , Vol. 2988 . Springer , Berlin , 153--157. Heikki Virtanen, Henri Hansen, Antti Valmari, Juha Nieminen, and Timo Erkkil\u00e4. 2004. Tampere verification tool. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201904), Kurt Jensen and Andreas Podelski (Eds.). LNCS, Vol. 2988. Springer, Berlin, 153--157."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0023-x"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_29"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3060140","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3060140","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:03:19Z","timestamp":1750215799000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3060140"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,4,30]]},"references-count":31,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,4,30]]}},"alternative-id":["10.1145\/3060140"],"URL":"https:\/\/doi.org\/10.1145\/3060140","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2017,4,30]]},"assertion":[{"value":"2016-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-06-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}