From generic partition refinement to weighted tree automata minimization. (English) Zbl 07395149

Summary: Partition refinement is a method for minimizing automata and transition systems of various types. Recently, we have developed a partition refinement algorithm that is generic in the transition type of the given system and matches the run time of the best known algorithms for many concrete types of systems, e.g. deterministic automata as well as ordinary, weighted, and probabilistic (labelled) transition systems. Genericity is achieved by modelling transition types as functors on sets, and systems as coalgebras. In the present work, we refine the run time analysis of our algorithm to cover additional instances, notably weighted automata and, more generally, weighted tree automata. For weights in a cancellative monoid we match, and for non-cancellative monoids such as (the additive monoid of) the tropical semiring even substantially improve, the asymptotic run time of the best known algorithms. We have implemented our algorithm in a generic tool that is easily instantiated to concrete system types by implementing a simple refinement interface. Moreover, the algorithm and the tool are modular, and partition refiners for new types of systems are obtained easily by composing pre-implemented basic functors. Experiments show that even for complex system types, the tool is able to handle systems with millions of transitions.


68-XX Computer science
Full Text: DOI arXiv


[1] Adams, S., Efficient Sets: A Balancing Act, J Funct Program, 3, 4, 553-561 (1993)
[2] Awodey S (2010) Category Theory, volume 52 of Oxford Logic Guides. Oxford University Press, Oxford, 2 edition
[3] Berkholz, C.; Bonsma, PS; Grohe, M., Tight Lower and Upper Bounds for the Complexity of Canonical Colour Refinement, Theory Comput Syst, 60, 4, 581-614 (2017) · Zbl 1368.68219
[4] Björklund J, Cleophas L (2020) Aggregation-Based Minimization of Finite State Automata. Acta Informatica, January 2020 · Zbl 07362509
[5] 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-585 · Zbl 1087.68583
[6] Baier, C.; Engelen, B.; Majster-Cederbaum, M., Deciding bisimilarity and similarity for probabilistic processes, J Comput Syst Sci, 60, 187-231 (2000) · Zbl 1073.68690
[7] Bunte, O.; Groote, JF; Keiren Jeroen, JA; Laveaux, M.; Neele, T.; de Vink, Erik P.; Wesselink, W.; Wijs, A.; Willemse Tim, AC, The mCRL2 Toolset for Analysing Concurrent Systems: Improvements in Expressivity and Usability, Tools and Algorithms for the Construction and Analysis of Systems, TACAS, 2019, 21-39 (2019)
[8] Bojańczyk, M., Klin, B., Lasota, S.: Automata Theory in Nominal Sets. Log Methods Comput Sci 10(3), (2014) · Zbl 1338.68140
[9] Blom S, Orzan S (2006) Distributed Branching Bisimulation Reduction of State Spaces. In: Parallel and Distributed Model Checking, PDMC 2003, volume 89 of ENTCS. Elsevier, pp. 99-113 · Zbl 1271.68133
[10] Blom, S.; Orzan, S., A Distributed Algorihm for Strong Bisimulation Reduction of State Spaces, J Softw Tools Technol Transfer, 7, 1, 74-86 (2005)
[11] 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 - 75 · Zbl 1270.68186
[12] Buchholz, P., Bisimulation Relations for Weighted Automata, Theor Comput Sci, 393, 109-123 (2008) · Zbl 1136.68032
[13] Cormen, T.; Leiserson, C.; Rivest, R., Introduction to Algorithms (1990), Cambridge: MIT Press, Cambridge · Zbl 1158.68538
[14] Ciardo, G.; Trivedi, KS, A Decomposition Approach for Stochastic Reward Net Models, Perform Evaluat, 18, 1, 37-59 (1993) · Zbl 0788.68105
[15] Deifel H-P (2019) Implementation and Evaluation of Efficient Partition Refinement Algorithms. Master’s thesis, Friedrich-Alexander Universität Erlangen-Nürnberg, https://hpdeifel.de/master-thesis-deifel.pdf
[16] Derisavi, S.; Hermanns, H.; Sanders, W., Optimal state-space lumping in Markov chains, Inf Process Lett, 87, 6, 309-315 (2003) · Zbl 1189.68039
[17] Dorsch U, Milius S, Schröder L, Wißmann T (2017) Efficient Coalgebraic Partition Refinement. In Concurrency Theory, CONCUR 2017, volume 85 of LIPIcs, pp. 32:1-32:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik · Zbl 1442.68112
[18] Deifel H-P, Milius S, Schröder L, Wißmann T (2019) Generic Partition Refinement and Weighted Tree Automata. In: ter Beek Maurice H, McIver Annabelle, Oliveira José N editors, Formal Methods - The Next 30 Years, Cham, 10. Springer, pp. 280-297
[19] Dovier, A.; Piazza, C.; Policriti, A., An efficient algorithm for computing bisimulation equivalence, Theor Comput Sci, 311, 1-3, 221-256 (2004) · Zbl 1070.68101
[20] Esik, Z.; Maletti, A., The Category of Simulations for Weighted Tree Automata, Int J Found Comput Sci, 22, 1845-1859, 12 (2011) · Zbl 1244.68046
[21] 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-429 · Zbl 1064.68523
[22] Groote JF, Jansen DN, Keiren Jeroen JA, Wijs Anton (2017) An O(mlogn) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation. ACM Trans Comput Log 18(2):13:1-13:34 · Zbl 1367.68211
[23] Gries, D., Describing an Algorithm by Hopcroft, Acta Informatica, 2, 97-109 (1973) · Zbl 0242.94042
[24] Groote, JF; Verduzco, JR; de Vink, Erik P., An Efficient Algorithm to Determine Probabilistic Bisimulation, Algorithms, 11, 9, 131 (2018) · Zbl 1461.68133
[25] Högberg 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-241 · Zbl 1202.68228
[26] Högberg, J.; Maletti, A.; May, J., Backward and Forward Bisimulation Minimization of Tree Automata, Theor Comput Sci, 410, 3539-3552 (2009) · Zbl 1194.68139
[27] Hopcroft John (1971) An \(n \log n\) Algorithm for Minimizing States in a Finite Automaton. In: Theory of Machines and Computations. Academic Press, pp. 189-196
[28] Huynh, D.; Tian, L., On Some Equivalence Relations for Probabilistic Processes, Fund Inform, 17, 211-234 (1992) · Zbl 0766.68099
[29] 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-591
[30] 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-20, 2012. IEEE Computer Society, pp. 203-204
[31] 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-26, 2002, Proceedings, volume 2399 of Lecture Notes in Computer Science. Springer, pp. 169-187 · Zbl 1065.68583
[32] Knuutila, T., Re-describing an algorithm by Hopcroft, Theor Comput Sci, 250, 333-363 (2001) · Zbl 0952.68077
[33] Kanellakis, P.; Smolka, S., CCS expressions, finite state processes, and three problems of equivalence, Inf Comput, 86, 1, 43-68 (1990) · Zbl 0705.68063
[34] Klin, B.; Sassone, V., Structural Operational Semantics for Stochastic and Weighted Transition Systems, Inf Comput, 227, 58-83 (2013) · Zbl 1358.68214
[35] 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-24, 1994. ACM, pp. 24-35
[36] Milner R (1980) A Calculus of Communicating Systems, volume 92 of LNCS. Springer · Zbl 0452.68027
[37] 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-113 · Zbl 1160.68423
[38] Park D (1981) Concurrency and Automata on Infinite Sequences. In Theoretical Computer Science, 5th GI-Conference, volume 104 of LNCS. Springer, pp. 167-183
[39] 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-440
[40] 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; Proceedings of the Main Conference, Rochester, New York, April 2007. Association for Computational Linguistics, pp. 404-411
[41] Paige, R.; Tarjan, R., Three Partition Refinement Algorithms, SIAM J Comput, 16, 6, 973-989 (1987) · Zbl 0654.68072
[42] Ranzato, F.; Tapparo, F., Generalizing the Paige-Tarjan Algorithm by Abstract Interpretation, Inf Comput, 206, 620-651 (2008) · Zbl 1197.68054
[43] Jan, Rutten, Universal Coalgebra: A Theory of Systems, Theor Comput Sci, 249, 3-80 (2000) · Zbl 0951.68038
[44] 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) · Zbl 1262.18002
[45] Segala R (1995) Modelling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT
[46] Schröder L, Kozen D, Milius S, Wißmann T (2017) Nominal automata with name binding. In: Foundations of Software Science and Computation Structures, FOSSACS 2017, volume 10203 of LNCS, pp. 124-142 · Zbl 06720987
[47] Valmari A (2009) Bisimilarity minimization in \((m \log n)\) time. In: Applications and Theory of Petri Nets, PETRI NETS 2009, volume 5606 of LNCS. Springer, pp. 123-142 · Zbl 1242.68186
[48] Valmari, A., Simple bisimilarity minimization in \((m \log n)\) time, Fund Inform, 105, 3, 319-339 (2010) · Zbl 1209.68344
[49] van Dijk, T.; van de Pol, J., Multi-Core Symbolic Bisimulation Minimization, J Softw Tools Technol Transfer, 20, 2, 157-177 (2018)
[50] Valmari A, Franceschinis G (2010) Simple \((m\log n)\) time Markov chain lumping. In: Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010, volume 6015 of LNCS. Springer, pp. 38-52 · Zbl 1284.68437
[51] van Glabbeek R (2001) The Linear Time—Branching Time Spectrum I; the Semantics of Concrete, Sequential Processes. In: Bergstra J, Ponse A, Smolka S (2001) editors, Handbook of Process Algebra. Elsevier, pp. 3-99 · Zbl 1035.68073
[52] Wißmann, T., Dorsch, U., Milius, S.: Schröder L (2020) Efficient and Modular Coalgebraic Partition Refinement. Logical Methods in Computer Science 16(1), (January 2020) · Zbl 1442.68113
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.