Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Formal Methods

FM 2019: Formal Methods – The Next 30 Years pp 280–297Cite as

Generic Partition Refinement and Weighted Tree Automata

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11800))

Abstract

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.

Work by S. Milius, L. Schröder, and T. Wißmann forms part of the DFG project COAX (MI 717/5-2 and SCHR 1118/12-2).

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Adams, S.: Efficient sets - a balancing act. J. Funct. Program. 3(4), 553–561 (1993)

    Article  Google Scholar 

  2. Baier, C., Engelen, B., Majster-Cederbaum, M.: Deciding bisimilarity and similarity for probabilistic processes. J. Comput. Syst. Sci. 60, 187–231 (2000)

    Article  MathSciNet  Google Scholar 

  3. Bartels, F., Sokolova, A., de Vink, E.: A hierarchy of probabilistic system types. In: Coagebraic Methods in Computer Science, CMCS 2003, ENTCS, vol. 82, pp. 57–75. Elsevier (2003)

    Google Scholar 

  4. Bergamini, D., Descoubes, N., Joubert, C., Mateescu, R.: BISIMULATOR: a modular tool for on-the-fly equivalence checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 581–585. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31980-1_42

    Chapter  MATH  Google Scholar 

  5. Berkholz, C., Bonsma, P.S., Grohe, M.: Tight lower and upper bounds for the complexity of canonical colour refinement. Theory Comput. Syst. 60(4), 581–614 (2017)

    Article  MathSciNet  Google Scholar 

  6. Blom, S., Orzan, S.: Distributed branching bisimulation reduction of state spaces. In: Parallel and Distributed Model Checking, PDMC 2003, ENTCS, vol. 89, pp. 99–113. Elsevier (2003)

    Google Scholar 

  7. Blom, S., Orzan, S.: A distributed algorihm for strong bisimulation reduction of state spaces. J. Softw. Tools Technol. Transf. 7(1), 74–86 (2005)

    Article  Google Scholar 

  8. Bojańczyk, M., Klin, B., Lasota, S.: Automata theory in nominal sets. Log. Methods Comput. Sci. 10(3) (2014)

    Google Scholar 

  9. Buchholz, P.: Bisimulation relations for weighted automata. Theor. Comput. Sci. 393, 109–123 (2008)

    Article  MathSciNet  Google Scholar 

  10. Bunte, O., et al.: The mCRL2 toolset for analysing concurrent systems. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 21–39. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17465-1_2

    Chapter  Google Scholar 

  11. Deifel, H.-P.: Implementation and evaluation of efficient partition refinement algorithms. Master’s thesis, Friedrich-Alexander Universität Erlangen-Nürnberg (2019). https://hpdeifel.de/master-thesis-deifel.pdf

  12. Deifel, H.-P., Milius, S., Schröder, L., Wißmann, T.: Generic partition refinement and weighted tree automata (2019). https://arxiv.org/abs/1811.08850

  13. Derisavi, S., Hermanns, H., Sanders, W.: Optimal state-space lumping in Markov chains. Inf. Process. Lett. 87(6), 309–315 (2003)

    Article  MathSciNet  Google Scholar 

  14. Dorsch, U., Milius, S., Schröder, L., Wißmann, T.: Efficient coalgebraic partition refinement. In: Concurrency Theory, CONCUR 2017, LIPIcs, pp. 32:1–32:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

    Google Scholar 

  15. Dovier, A., Piazza, C., Policriti, A.: An efficient algorithm for computing bisimulation equivalence. Theor. Comput. Sci. 311(1–3), 221–256 (2004)

    Article  MathSciNet  Google Scholar 

  16. Garavel, H., Hermanns, H.: On combining functional verification and performance evaluation using CADP. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 410–429. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45614-7_23

    Chapter  Google Scholar 

  17. Gries, D.: Describing an algorithm by Hopcroft. Acta Informatica 2, 97–109 (1973)

    Article  MathSciNet  Google Scholar 

  18. Groote, J., Jansen, D., Keiren, J., Wijs, A.: An O(m log n) algorithm for computing stuttering equivalence and branching bisimulation. ACM Trans. Comput. Log. 18(2), 13:1–13:34 (2017)

    Google Scholar 

  19. Groote, J., Verduzco, J., de Vink, E.: An efficient algorithm to determine probabilistic bisimulation. Algorithms 11(9), 131 (2018)

    Article  MathSciNet  Google Scholar 

  20. Högberg, J., Maletti, A., May, J.: Bisimulation minimisation for weighted tree automata. In: Harju, T., Karhumäki, J., Lepistö, A. (eds.) DLT 2007. LNCS, vol. 4588, pp. 229–241. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73208-2_23

    Chapter  Google Scholar 

  21. Högberg, J., Maletti, A., May, J.: Backward and forward bisimulation minimization of tree automata. Theor. Comput. Sci. 410, 3539–3552 (2009)

    Article  MathSciNet  Google Scholar 

  22. 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)

    Google Scholar 

  23. Huynh, D., Tian, L.: On some equivalence relations for probabilistic processes. Fund. Inf. 17, 211–234 (1992)

    MathSciNet  MATH  Google Scholar 

  24. Kanellakis, P., Smolka, S.: CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. 86(1), 43–68 (1990)

    Article  MathSciNet  Google Scholar 

  25. Klin, B., Sassone, V.: Structural operational semantics for stochastic and weighted transition systems. Inf. Comput. 227, 58–83 (2013)

    Article  MathSciNet  Google Scholar 

  26. Knuutila, T.: Re-describing an algorithm by Hopcroft. Theor. Comput. Sci. 250, 333–363 (2001)

    Article  MathSciNet  Google Scholar 

  27. Paige, R., Tarjan, R.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973–989 (1987)

    Article  MathSciNet  Google Scholar 

  28. PRISM: Benchmarks FMS and WLAN. http://www.prismmodelchecker.org/casestudies/fms.php, wlan.php. Accessed 16 Nov 2018

  29. Ranzato, F., Tapparo, F.: Generalizing the Paige-Tarjan algorithm by abstract interpretation. Inf. Comput. 206, 620–651 (2008)

    Article  MathSciNet  Google Scholar 

  30. Rutten, J.: Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249, 3–80 (2000)

    Article  MathSciNet  Google Scholar 

  31. Schröder, L., Kozen, D., Milius, S., Wißmann, T.: Nominal automata with name binding. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 124–142. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54458-7_8

    Chapter  Google Scholar 

  32. Segala, R.: Modelling and verification of randomized distributed real-time systems. Ph.D. thesis, MIT (1995)

    Google Scholar 

  33. Valmari, A.: Bisimilarity minimization in o(m logn) time. In: Franceschinis, G., Wolf, K. (eds.) PETRI NETS 2009. LNCS, vol. 5606, pp. 123–142. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02424-5_9

    Chapter  Google Scholar 

  34. Valmari, A.: Simple bisimilarity minimization in O(m logn) time. Fund. Inform. 105(3), 319–339 (2010)

    Article  MathSciNet  Google Scholar 

  35. Valmari, A., Franceschinis, G.: Simple O(m logn) time Markov chain lumping. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 38–52. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12002-2_4

    Chapter  Google Scholar 

  36. van Dijk, T., van de Pol, J.: Multi-core symbolic bisimulation minimization. J. Softw. Tools Technol. Transf. 20(2), 157–177 (2018)

    Article  Google Scholar 

  37. Wißmann, T., Dorsch, U., Milius, S., Schröder, L.: Efficient and modular coalgebraic partition refinement (2019). https://arxiv.org/abs/1806.05654

Download references

Author information

Authors and Affiliations

  1. Friedrich-Alexander-Universität Erlangen-Nürnberg, Erlangen, Germany

    Hans-Peter Deifel, Stefan Milius, Lutz Schröder & Thorsten Wißmann

Authors
  1. Hans-Peter Deifel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stefan Milius
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Lutz Schröder
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Thorsten Wißmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Thorsten Wißmann .

Editor information

Editors and Affiliations

  1. Consiglio Nazionale delle Ricerche, Pisa, Italy

    Maurice H. ter Beek

  2. Macquarie University, Sydney, NSW, Australia

    Annabelle McIver

  3. University of Minho, Braga, Portugal

    José N. Oliveira

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Deifel, HP., Milius, S., Schröder, L., Wißmann, T. (2019). Generic Partition Refinement and Weighted Tree Automata. In: ter Beek, M., McIver, A., Oliveira, J. (eds) Formal Methods – The Next 30 Years. FM 2019. Lecture Notes in Computer Science(), vol 11800. Springer, Cham. https://doi.org/10.1007/978-3-030-30942-8_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-30942-8_18

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-30941-1

  • Online ISBN: 978-3-030-30942-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation