{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:38:17Z","timestamp":1740109097241,"version":"3.37.3"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"4-5","license":[{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["MI 717\/5-2"],"award-info":[{"award-number":["MI 717\/5-2"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["SCHR 1118\/12-2"],"award-info":[{"award-number":["SCHR 1118\/12-2"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["393541319\/GRK2475\/1-2019"],"award-info":[{"award-number":["393541319\/GRK2475\/1-2019"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["MI 717\/5-2"],"award-info":[{"award-number":["MI 717\/5-2"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["393541319\/GRK2475\/1-2019"],"award-info":[{"award-number":["393541319\/GRK2475\/1-2019"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["SCHR 1118\/12-2"],"award-info":[{"award-number":["SCHR 1118\/12-2"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["393541319\/GRK2475\/1-2019"],"award-info":[{"award-number":["393541319\/GRK2475\/1-2019"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2021,8]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Partition refinement is a method for minimizing automata and transition systems of various types. Recently,\nwe have developed a partition refinement algorithm that is generic in the transition type of the given system\nand matches the run time of the best known algorithms for many concrete types of systems, e.g. deterministic\nautomata as well as ordinary, weighted, and probabilistic (labelled) transition systems. Genericity is achieved by\nmodelling transition types as functors on sets, and systems as coalgebras. In the present work, we refine the run\ntime analysis of our algorithm to cover additional instances, notably weighted automata and, more generally,\nweighted tree automata. For weights in a cancellative monoid we match, and for non-cancellative monoids such\nas (the additive monoid of) the tropical semiring even substantially improve, the asymptotic run time of the best\nknown algorithms. We have implemented our algorithm in a generic tool that is easily instantiated to concrete\nsystem types by implementing a simple refinement interface. Moreover, the algorithm and the tool are modular,\nand partition refiners for new types of systems are obtained easily by composing pre-implemented basic functors.\nExperiments show that even for complex system types, the tool is able to handle systems with millions of\ntransitions.<\/jats:p>","DOI":"10.1007\/s00165-020-00526-z","type":"journal-article","created":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T16:06:50Z","timestamp":1616515610000},"page":"695-727","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["From generic partition refinement to weighted tree automata minimization"],"prefix":"10.1145","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8993-6486","authenticated-orcid":false,"given":"Thorsten","family":"Wi\u00dfmann","sequence":"first","affiliation":[{"name":"Friedrich-Alexander-Universit\u00e4t Erlangen-N\u00fcrnberg, Erlangen, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9542-9664","authenticated-orcid":false,"given":"Hans-Peter","family":"Deifel","sequence":"additional","affiliation":[{"name":"Friedrich-Alexander-Universit\u00e4t Erlangen-N\u00fcrnberg, Erlangen, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2021-1644","authenticated-orcid":false,"given":"Stefan","family":"Milius","sequence":"additional","affiliation":[{"name":"Friedrich-Alexander-Universit\u00e4t Erlangen-N\u00fcrnberg, Erlangen, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3146-5906","authenticated-orcid":false,"given":"Lutz","family":"Schr\u00f6der","sequence":"additional","affiliation":[{"name":"Friedrich-Alexander-Universit\u00e4t Erlangen-N\u00fcrnberg, Erlangen, Germany"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000885"},{"key":"e_1_2_1_2_2_2","unstructured":"Awodey S (2010) Category Theory volume 52 of Oxford Logic Guides. Oxford University Press Oxford 2 edition"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-016-9686-0"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Bj\u00f6rklund J Cleophas L (2020) Aggregation-Based Minimization of Finite State Automata. Acta Informatica January 2020","DOI":"10.1007\/s00236-019-00363-5"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Bergamini D Descoubes N Joubert C Mateescu R (2005) BISIMULATOR: A Modular Tool for on-the-Fly Equivalence Checking. In: Tools and Algorithms for the Construction and Analysis of Systems TACAS 2005 volume 3440 of LNCS . Springer pp 581\u2013585","DOI":"10.1007\/978-3-540-31980-1_42"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1999.1683"},{"key":"e_1_2_1_2_7_2","first-page":"21","article-title":"The mCRL2 Toolset for Analysing Concurrent Systems: Improvements in Expressivity and Usability","volume":"2019","author":"Bunte O","year":"2019","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems, TACAS"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Boja\u0144czyk M. Klin B. Lasota S.: Automata Theory in Nominal Sets. Log Methods Comput Sci 10 (3) (2014)","DOI":"10.2168\/LMCS-10(3:4)2014"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Blom S Orzan S (2006) Distributed Branching Bisimulation Reduction of State Spaces. In: Parallel and Distributed Model Checking PDMC 2003 volume\u00a089 of ENTCS. Elsevier pp. 99\u2013113","DOI":"10.1016\/S1571-0661(05)80099-4"},{"issue":"1","key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1007\/s10009-004-0159-4","article-title":"A Distributed Algorihm for Strong Bisimulation Reduction of State Spaces","volume":"7","author":"Blom S","year":"2005","journal-title":"J Softw Tools Technol Transfer"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Bartels F Sokolova A de Vink E (2003) A Hierarchy of Probabilistic System Types. In: Coagebraic Methods in Computer Science CMCS 2003 volume 82 of ENTCS. Elsevier pp. 57 \u2013 75","DOI":"10.1016\/S1571-0661(04)80632-7"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.11.018"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.5555\/80156"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/0166-5316(93)90026-Q"},{"key":"e_1_2_1_2_15_2","unstructured":"Deifel H-P (2019) Implementation and Evaluation of Efficient Partition Refinement Algorithms. Master's thesis Friedrich-Alexander Universit\u00e4t Erlangen-N\u00fcrnberg https:\/\/hpdeifel.de\/master-thesis-deifel.pdf"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(03)00343-0"},{"key":"e_1_2_1_2_17_2","unstructured":"Dorsch U Milius S Schr\u00f6der L Wi\u00dfmann T (2017) Efficient Coalgebraic Partition Refinement. In  Concurrency Theory CONCUR 2017 volume 85 of LIPIcs pp. 32:1\u201332:16. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Deifel H-P Milius S Schr\u00f6der L Wi\u00dfmann T (2019) Generic Partition Refinement and Weighted Tree Automata. In: ter Beek Maurice H McIver Annabelle Oliveira Jos\u00e9 N editors Formal Methods \u2013 The Next 30 Years Cham 10. Springer pp. 280\u2013297","DOI":"10.1007\/978-3-030-30942-8_18"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00361-X"},{"issue":"1845","key":"e_1_2_1_2_20_2","first-page":"12","article-title":"The Category of Simulations for Weighted Tree Automata","volume":"22","author":"Esik Z","year":"2011","journal-title":"Int J Found Comput Sci"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Garavel H Hermanns H (2002) On Combining Functional Verification and Performance Evaluation Using CADP. In: Formal Methods Europe FME 2002 volume 2391 of LNCS. Springer pp. 410\u2013429","DOI":"10.1007\/3-540-45614-7_23"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Groote JF Jansen DN Keiren Jeroen JA Wijs Anton (2017) An O ( m log n ) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation. ACM Trans Comput Log 18(2):13:1\u201313:34","DOI":"10.1145\/3060140"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264025"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.3390\/a11090131"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"H\u00f6gberg J Maletti A May J (2007) Bisimulation Minimisation for Weighted Tree Automata. In: Developments in Language Theory DLT 2007 volume 4588 of LNCS. Springer pp. 229\u2013241","DOI":"10.1007\/978-3-540-73208-2_23"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.03.022"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Hopcroft John (1971) An nlogn Algorithm for Minimizing States in a Finite Automaton. In: Theory of Machines and Computations. Academic Press pp. 189\u2013196","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"key":"e_1_2_1_2_28_2","first-page":"211","article-title":"On Some Equivalence Relations for Probabilistic Processes","volume":"17","author":"Huynh D","year":"1992","journal-title":"Fund Inform"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M Norman G Parker D (2011) PRISM 4.0: Verification of Probabilistic Real-Time Systems. In: Computer Aided Verification CAV 2011 volume 6806 of  LNCS. Springer pp. 585\u2013591","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Kwiatkowska MZ Norman G Parker D (2012) The PRISM Benchmark Suite. In: Ninth International Conference on Quantitative Evaluation of Systems QEST 2012 London United Kingdom September 17\u201320 2012. IEEE Computer Society pp. 203\u2013204","DOI":"10.1109\/QEST.2012.14"},{"key":"e_1_2_1_2_31_2","unstructured":"Kwiatkowska MZ Norman G Sproston J (2002) Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol. In: Holger Hermanns and Roberto Segala editors Process Algebra and Probabilistic Methods Performance Modeling and Verification Second Joint International Workshop PAPM-PROBMIV 2002 Copenhagen Denmark July 25\u201326 2002 Proceedings volume 2399 of Lecture Notes in Computer Science. Springer pp. 169\u2013187"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00150-4"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90025-D"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2013.04.001"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Launchbury J Peyton J Simon L (1994) Lazy functional state threads. In Sarkar Vivek Ryder Barbara G Soffa Mary Lou editors Proceedings of the ACM SIGPLAN'94 Conference on Programming Language Design and Implementation (PLDI) Orlando Florida USA June 20\u201324 1994. ACM pp. 24\u201335","DOI":"10.1145\/178243.178246"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Milner R (1980) A Calculus of Communicating Systems volume 92 of LNCS. Springer","DOI":"10.1007\/3-540-10235-3"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"May J Knight K (2006) Tiburon: A Weighted Tree Automata Toolkit. In: Ibarra OH Yen H-C editors Implementation and Application of Automata Berlin Heidelberg pp. 102\u2013113","DOI":"10.1007\/11812128_11"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Park D (1981) Concurrency and Automata on Infinite Sequences. In  Theoretical Computer Science 5th GI-Conference volume 104 of  LNCS. Springer pp. 167\u2013183","DOI":"10.1007\/BFb0017309"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Petrov S Barrett L Thibaux R Klein D (2006) Learning Accurate Compact and Interpretable Tree Annotation. In: Proceedings of the 21st International Conference on Computational Linguistics and 44th Annual Meeting of the Association for Computational Linguistics Sydney Australia July 2006. Association for Computational Linguistics pp. 433\u2013440","DOI":"10.3115\/1220175.1220230"},{"key":"#cr-split#-e_1_2_1_2_40_2.1","unstructured":"Petrov S Klein D (2007) Improved Inference for Unlexicalized Parsing. In Human Language Technologies 2007: The Conference of the North American Chapter of the Association for Computational Linguistics"},{"key":"#cr-split#-e_1_2_1_2_40_2.2","unstructured":"Proceedings of the Main Conference Rochester New York April 2007. Association for Computational Linguistics pp. 404-411"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"publisher","DOI":"10.1137\/0216062"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2008.01.001"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Silva A. Bonchi F. Bonsangue M.M. Rutten Jan J.M.M.: Generalizing determinization from automata to coalgebras. Log Methods Comput Sci 9 (1) (2013)","DOI":"10.2168\/LMCS-9(1:9)2013"},{"key":"e_1_2_1_2_45_2","unstructured":"Segala R (1995) Modelling and Verification of Randomized Distributed Real-Time Systems. PhD thesis MIT"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Schr\u00f6der L Kozen D Milius S Wi\u00dfmann T (2017) Nominal automata with name binding. In: Foundations of Software Science and Computation Structures FOSSACS 2017 volume 10203 of LNCS pp. 124\u2013142","DOI":"10.1007\/978-3-662-54458-7_8"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"Valmari A (2009) Bisimilarity minimization in (mlogn) time. In: Applications and Theory of Petri Nets PETRI NETS 2009 volume 5606 of LNCS. Springer pp. 123\u2013142","DOI":"10.1007\/978-3-642-02424-5_9"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"publisher","DOI":"10.5555\/2010413.2010419"},{"issue":"2","key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/s10009-017-0468-z","article-title":"Multi-Core Symbolic Bisimulation Minimization","volume":"20","author":"van Dijk T","year":"2018","journal-title":"J Softw Tools Technol Transfer"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"Valmari A Franceschinis G (2010) Simple (mlogn) time Markov chain lumping. In: Tools and Algorithms for the Construction and Analysis of Systems TACAS 2010 volume 6015 of LNCS. Springer pp. 38\u201352","DOI":"10.1007\/978-3-642-12002-2_4"},{"key":"#cr-split#-e_1_2_1_2_51_2.1","unstructured":"van Glabbeek R (2001) The Linear Time-Branching Time Spectrum I"},{"key":"#cr-split#-e_1_2_1_2_51_2.2","unstructured":"the Semantics of Concrete Sequential Processes. In: Bergstra J Ponse A Smolka S (2001) editors Handbook of Process Algebra. Elsevier pp. 3-99"},{"key":"e_1_2_1_2_52_2","unstructured":"Wi\u00dfmann T. Dorsch U. Milius S.: Schr\u00f6der L (2020) Efficient and Modular Coalgebraic Partition Refinement. Logical Methods in Computer Science 16 (1) (January 2020)"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-020-00526-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00165-020-00526-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-020-00526-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-020-00526-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:22:24Z","timestamp":1641486144000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-020-00526-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8]]},"references-count":54,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["10.1007\/s00165-020-00526-z"],"URL":"https:\/\/doi.org\/10.1007\/s00165-020-00526-z","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2021,8]]},"assertion":[{"value":"28 February 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 October 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 December 2020","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 March 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}