Abstract
Partition refinement is a method for minimizing automata and transition systems of various types. Recently we have developed a partition refinement algorithm and the tool CoPaR that is generic in the transition type of the input system and matches the theoretical run time of the best known algorithms for many concrete system types. Genericity is achieved by modelling transition types as functors on sets and systems as coalgebras. Experimentation has shown that memory consumption is a bottleneck for handling systems with a large state space, while running times are fast. We have therefore extended an algorithm due to Blom and Orzan, which is suitable for a distributed implementation to the coalgebraic level of genericity, and implemented it in CoPaR. Experiments show that this allows to handle much larger state spaces. Running times are low in most experiments, but there is a significant penalty for some.
Supported by the Deutsche Forschungsgemeinschaft (DFG) within the Research and Training Group 2475 “Cybercrime and Forensic Computing” (393541319/GRK2475/1-2019)
Supported by Deutsche Forschungsgemeinschaft (DFG) under project MI 717/7-1.
Chapter PDF
Similar content being viewed by others
References
Balcazar, J., Gabarro, J., Santha, M.: Deciding bisimilarity is \(P\)-complete. Form. Asp. Comput. 4(6A), 638–648 (1992)
Bartels, F., Sokolova, A., de Vink, E.: A hierarchy of probabilistic system types. In: Coalgebraic Methods in Computer Science, CMCS 2003. Electron. Notes Theor. Comput. Sci., vol. 82, pp. 57–75. Elsevier (2003)
Birkmann, F., Deifel, H.P., Milius, S.: Software and Benchmarks for Distributed Coalgebraic Partition Refinement (Jan 2022). https://doi.org/10.5281/zenodo.5907084
Blom, S., Haverkort, B.R., Kuntz, M., van de Pol, J.: Distributed Markovian bisimulation reduction aimed at CSL model checking. In: Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2008). Electron. Notes Theor. Comput. Sci., vol. 220, pp. 35–50. Elsevier (2008)
Blom, S., Orzan, S.: A distributed algorithm for strong bisimulation reduction of state spaces. In: Brim, L., Grumberg, O. (eds.) Proc. Parallel and Distributed Model Checking (PDMC). Electron. Notes Theor. Comput. Sci., vol. 68, pp. 523–538. Elsevier (2002)
Blom, S., Orzan, S.: Distributed branching bisimulation reduction of state spaces. In: Sokolsky, O., Viswanathan, M. (eds.) Proc. Parallel and Distributed Model Checking (PDMC). Electron. Notes Theor. Comput. Sci., vol. 89, pp. 99–113. Elsevier (2003)
Blom, S., Orzan, S.: Distributed state space minimization. In: Arts, T., Fokkink, W. (eds.) Proc. Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS). Electron. Notes Theor. Comput. Sci., vol. 80, pp. 109–123. Elsevier (2003)
Blom, S., Orzan, S.: A distributed algorithm for strong bisimulation reduction of state spaces. International Journal on Software Tools for Technology Transfer 7(1), 74–86 (2005). https://doi.org/10.1007/s10009-004-0159-4
Blom, S., Orzan, S.: Distributed state space minimization. International Journal on Software Tools for Technology Transfer 7(3), 280–291 (Jun 2005). https://doi.org/10.1007/s10009-004-0185-2
Buchholz, P.: Bisimulation relations for weighted automata. Theoret. Comput. Sci. 393, 109–123 (2008)
Deifel, H.P., Milius, S., Schröder, L., Wißmann, T.: Generic partition refinement and weighted tree automata. In: ter Beek et al., M. (ed.) Proc. International Symposium on Formal Methods (FM). Lecture Notes Comput. Sci., vol. 11800, pp. 280–297. Springer (2019)
Deifel, H.P., Milius, S., Wißmann, T.: Coalgebra encoding for efficient minimization. In: Kobayashi, N. (ed.) Proc. 6th International Conference on Formal Structures for Computation and Deduction (FSCD). LIPIcs, vol. 195, pp. 28:1–28:19. Schloss Dagstuhl (2021)
Derisavi, S., Hermanns, H., Sanders, W.: Optimal state-space lumping in Markov chains. Inf. Process. Lett. 87(6), 309–315 (2003)
Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled markov processes. Inform. Comput. 179(2), 163–193 (2002)
van Dijk, T., van de Pol, J.: Multi-core symbolic bisimulation minimisation. International Journal on Software Tools for Technology Transfer 20(2), 157–177 (Apr 2018). https://doi.org/10.1007/s10009-017-0468-z, http://springerlink.fh-diploma.de/10.1007/s10009-017-0468-z
Dorsch, U., Milius, S., Schröder, L., Wißmann, T.: Efficient coalgebraic partition refinement. In: Meyer, R., Nestmann, U. (eds.) Proc. 28th International Conference on Concurrency Theory (CONCUR). LIPIcs, vol. 85, pp. 28:1–28:16. Schloss Dagstuhl (2017)
van Glabbeek, R.: The linear time – branching time spectrum I; the semantics of concrete, sequential processes. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra, pp. 3–99. Elsevier (2001)
Gries, D.: Describing an algorithm by Hopcroft. Acta Informatica 2, 97–109 (1973)
Harris, T., Marlow, S., Peyton Jones, S.: Composable memory transactions. In: PPoPP ’05: Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming. pp. 48–60. ACM Press (January 2005), https://www.microsoft.com/en-us/research/publication/composable-memory-transactions/
Högberg (Björklund), J., Maletti, A., May, J.: Bisimulation minimisation for weighted tree automata. In: Developments in Language Theory, 11th International Conference, DLT 2007, Turku, Finland, July 3-6, 2007, Proceedings. Lecture Notes Comput. Sci., vol. 4588, pp. 229–241. Springer (2007). https://doi.org/10.1007/978-3-540-73208-2
Hopcroft, J.: An \(n \log n\) algorithm for minimizing states in a finite automaton. In: Theory of Machines and Computations. pp. 189–196. Academic Press (1971)
Huynh, D., Tian, L.: On some equivalence relations for probabilistic processes. Fund. Inform. 17, 211–234 (1992)
Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. Inform. Comput. 86(1), 43–68 (1990). https://doi.org/10.1016/0890-5401(90)90025-D
Knuutila, T.: Re-describing an algorithm by Hopcroft. Theoret. Comput. Sci. 250, 333–363 (2001)
König, B., Küpper, S.: Generic partition refinement algorithms for coalgebras and an instantiation to weighted automata. In: Theoretical Computer Science, IFIP TCS 2014. Lecture Notes Comput. Sci., vol. 8705, pp. 311–325. Springer (2014)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Computer Aided Verification, CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer (2011)
Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM benchmark suite. In: Ninth International Conference on Quantitative Evaluation of Systems, QEST 2012, London, United Kingdom, September 17-20, 2012. pp. 203–204. IEEE Computer Society (2012). https://doi.org/10.1109/QEST.2012.14
Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inform. Comput. 94(1), 1–28 (1991)
Milner, R.: A Calculus of Communicating Systems, Lecture Notes Comput. Sci., vol. 92. Springer (1980)
Milner, R.: Communication and Concurrency. International Series in Computer Science, Prentice Hall (1989)
Paige, R., Tarjan, R.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973–989 (1987)
Park, D.: Concurrency on automata and infinite sequences. In: Deussen, P. (ed.) Proc. Conf. on Theoretical Computer Science. Lecture Notes Comput. Sci., vol. 104, pp. 167–183 (1981)
Rajasekaran, S., Lee, I.: Parallel algorithms for relational coarsest partition problems. IEEE Trans. Parallel Distributed Syst. 9(7), 687–699 (1998). https://doi.org/10.1109/71.707548
Rutten, J.: Universal coalgebra: a theory of systems. Theoret. Comput. Sci. 249, 3–80 (2000)
Rutten, J., de Vink, E.: Bisimulation for probabilistic transition systems: a coalgebraic approach. Theoret. Comput. Sci. 221, 271–293 (1999)
Valmari, A.: Bisimilarity minimization in \(\cal{O}(m \log n)\) time. In: Applications and Theory of Petri Nets, PETRI NETS 2009. Lecture Notes Comput. Sci., vol. 5606, pp. 123–142. Springer (2009)
Valmari, A.: Simple bisimilarity minimization in o(m log n) time. Fundam. Inform. 105(3), 319–339 (2010). https://doi.org/10.3233/FI-2010-369
Valmari, A., Franceschinis, G.: Simple \(\cal{O}(m\log n)\) time Markov chain lumping. In: Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010. Lecture Notes Comput. Sci., vol. 6015, pp. 38–52. Springer (2010)
Vitter, J.S.: An efficient algorithm for sequential random sampling. ACM Trans. Math. Softw. 13(1), 58–67 (1987). https://doi.org/10.1145/23002.23003
Wimmer, R., Herbstritt, M., Hermanns, H., Strampp, K., Becker, B.: Sigref – A Symbolic Bisimulation Tool Box. In: Hutchison, D., Kanade, T., Kittler, J., Kleinberg, J.M., Mattern, F., Mitchell, J.C., Naor, M., Nierstrasz, O., Pandu Rangan, C., Steffen, B., Sudan, M., Terzopoulos, D., Tygar, D., Vardi, M.Y., Weikum, G., Graf, S., Zhang, W. (eds.) Automated Technology for Verification and Analysis, vol. 4218, pp. 477–492. Springer Berlin Heidelberg, Berlin, Heidelberg (2006). https://doi.org/10.1007/11901914_35
Wißmann, T., Deifel, H.P., Milius, S., Schröder, L.: From generic partition refinement to weighted tree automata minimization. Form. Asp. Comput. 33, 695–727 (2021)
Wißmann, T., Dorsch, U., Milius, S., Schröder, L.: Efficient and modular coalgebraic partition refinement. Log. Methods Comput. Sci. 16(1), 8:1–8:63 (2020)
Wißmann, T., Milius, S., Schröder, L.: Explaining behavioural inequivalence generically in quasilinear time. In: Haddad, S., Varacca, D. (eds.) Proc. 32nd International Conference on Concurrency Theory (CONCUR). LIPIcs, vol. 203, pp. 31:1–32:18. Schloss Dagstuhl (2021)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Birkmann, F., Deifel, HP., Milius, S. (2022). Distributed Coalgebraic Partition Refinement. In: Fisman, D., Rosu, G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022. Lecture Notes in Computer Science, vol 13244. Springer, Cham. https://doi.org/10.1007/978-3-030-99527-0_9
Download citation
DOI: https://doi.org/10.1007/978-3-030-99527-0_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99526-3
Online ISBN: 978-3-030-99527-0
eBook Packages: Computer ScienceComputer Science (R0)