Document Open Access Logo

Efficient Coalgebraic Partition Refinement

Authors Ulrich Dorsch, Stefan Milius, Lutz Schröder, Thorsten Wißmann

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2017.32.pdf
  • Filesize: 0.61 MB
  • 16 pages

Document Identifiers

Author Details

Ulrich Dorsch
Stefan Milius
Lutz Schröder
Thorsten Wißmann

Cite AsGet BibTex

Ulrich Dorsch, Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Efficient Coalgebraic Partition Refinement. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 32:1-32:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CONCUR.2017.32

Abstract

We present a generic partition refinement algorithm that quotients coalgebraic systems by behavioural equivalence, an important task in reactive verification; coalgebraic generality implies in particular that we cover not only classical relational systems but also various forms of weighted systems. Under assumptions on the type functor that allow representing its finite coalgebras in terms of nodes and edges, our algorithm runs in time O(m log n) where n and m are the numbers of nodes and edges, respectively. Instances of our generic algorithm thus match the runtime of the best known algorithms for unlabelled transition systems, Markov chains, and deterministic automata (with fixed alphabets), and improve the best known algorithms for Segala systems.
Keywords
  • markov chains
  • deterministic finite automata
  • partition refinement
  • generic algorithm
  • paige-tarjan algorithm
  • transition systems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Jiří Adámek. Introduction to coalgebra. Theory Appl. Categ., 14:157-199, 2005. Google Scholar
  2. Jiří Adámek, Horst Herrlich, and George Strecker. Abstract and Concrete Categories. Wiley Interscience, 1990. Google Scholar
  3. Christel Baier, Bettina Engelen, and Mila Majster-Cederbaum. Deciding bisimilarity and similarity for probabilistic processes. J. Comput. Syst. Sci., 60:187-231, 2000. Google Scholar
  4. Falk Bartels, Ana Sokolova, and Erik de Vink. A hierarchy of probabilistic system types. In Coagebraic Methods in Computer Science, CMCS 2003, volume 82 of ENTCS, pages 57 - 75. Elsevier, 2003. Google Scholar
  5. Stefan Blom and Simona Orzan. A distributed algorithm for strong bisimulation reduction of state spaces. STTT, 7(1):74-86, 2005. Google Scholar
  6. Peter Buchholz. Bisimulation relations for weighted automata. Theoret. Comput. Sci., 393:109-123, 2008. Google Scholar
  7. Stefano Cattani and Roberto Segala. Decision algorithms for probabilistic bisimulation. In Concurrency Theory, CONCUR 2002, volume 2421 of LNCS, pages 371-385. Springer, 2002. Google Scholar
  8. Salem Derisavi, Holger Hermanns, and William Sanders. Optimal state-space lumping in markov chains. Inf. Process. Lett., 87(6):309-315, 2003. Google Scholar
  9. Josee Desharnais, Abbas Edalat, and Prakash Panangaden. Bisimulation for labelled markov processes. Inf. Comput., 179(2):163-193, 2002. Google Scholar
  10. Agostino Dovier, Carla Piazza, and Alberto Policriti. An efficient algorithm for computing bisimulation equivalence. Theor. Comput. Sci., 311(1-3):221-256, 2004. Google Scholar
  11. Kathi Fisler and Moshe Vardi. Bisimulation minimization and symbolic model checking. Formal Methods in System Design, 21(1):39-78, 2002. Google Scholar
  12. David Gries. Describing an algorithm by Hopcroft. Acta Informatica, 2:97-109, 1973. Google Scholar
  13. Heinz-Peter Gumm and Tobias Schröder. Monoid-labelled transition systems. In Coalgebraic Methods in Computer Science, CMCS 2001, volume 44 of ENTCS, pages 185-204, 2001. Google Scholar
  14. John Hopcroft. An n log n algorithm for minimizing states in a finite automaton. In Theory of Machines and Computations, pages 189-196. Academic Press, 1971. Google Scholar
  15. Dung Huynh and Lu Tian. On some equivalence relations for probabilistic processes. Fund. Inform., 17:211-234, 1992. Google Scholar
  16. Bart Jacobs. Introduction to Coalgebras: Towards Mathematics of States and Observations. Cambridge University Press, 2017. Google Scholar
  17. Bart Jacobs and Jan Rutten. A tutorial on (co)algebras and (co)induction. Bull. EATCS, 62:222-259, 1997. Google Scholar
  18. Paris C. Kanellakis and Scott A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput., 86(1):43-68, 1990. Google Scholar
  19. Joost-Pieter Katoen, Tim Kemna, Ivan Zapreev, and David Jansen. Bisimulation minimisation mostly speeds up probabilistic model checking. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2007, volume 4424 of LNCS, pages 87-101. Springer, 2007. Google Scholar
  20. Bartek Klin. Structural operational semantics for weighted transition systems. In Jens Palsberg, editor, Semantics and Algebraic Specification: Essays Dedicated to Peter D. Mosses on the Occasion of His 60th Birthday, volume 5700 of LNCS, pages 121-139. Springer, 2009. Google Scholar
  21. Timo Knuutila. Re-describing an algorithm by Hopcroft. Theor. Comput. Sci., 250:333 - 363, 2001. Google Scholar
  22. Barbara König and Sebastian Küpper. Generic partition refinement algorithms for coalgebras and an instantiation to weighted automata. In Theoretical Computer Science, IFIP TCS 2014, volume 8705 of LNCS, pages 311-325. Springer, 2014. Google Scholar
  23. Kim Guldstrand Larsen and Arne Skou. Bisimulation through probabilistic testing. Inf. Comput., 94:1-28, 1991. Google Scholar
  24. Robin Milner. A Calculus of Communicating Systems, volume 92 of LNCS. Springer, 1980. Google Scholar
  25. Robert Paige and Pobert E. Tarjan. Three partition refinement algorithms. SIAM J. Comput., 16(6):973-989, 1987. Google Scholar
  26. David Park. Concurrency and automata on infinite sequences. In Theoretical Computer Science, 5th GI-Conference, volume 104 of LNCS, pages 167-183. Springer, 1981. Google Scholar
  27. Francesco Ranzato and Francesco Tapparo. Generalizing the Paige-Tarjan algorithm by abstract interpretation. Inf. Comput., 206:620-651, 2008. Google Scholar
  28. Jan Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249:3-80, 2000. Google Scholar
  29. Lutz Schröder and Dirk Pattinson. Modular algorithms for heterogeneous modal logics via multi-sorted coalgebra. Math. Struct. Comput. Sci., 21(2):235-266, 2011. Google Scholar
  30. Roberto Segala. Modelling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology, 1995. Google Scholar
  31. Antti Valmari. Bisimilarity minimization in 𝒪(m log n) time. In Applications and Theory of Petri Nets, PETRI NETS 2009, volume 5606 of LNCS, pages 123-142. Springer, 2009. Google Scholar
  32. Antti Valmari and Giuliana Franceschinis. Simple 𝒪(mlog n) time Markov chain lumping. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010, volume 6015 of LNCS, pages 38-52. Springer, 2010. Google Scholar
  33. Johann van Benthem. Modal Correspondence Theory. PhD thesis, Universiteit van Amsterdam, 1977. Google Scholar
  34. Ron van der Meyden and Chenyi Zhang. Algorithmic verification of noninterference properties. In Views on Designing Complex Architectures, VODCA 2006, volume 168 of ENTCS, pages 61-75. Elsevier, 2007. Google Scholar
  35. James Worrell. On the final sequence of a finitary set functor. Theor. Comput. Sci., 338:184-199, 2005. Google Scholar
  36. Lijun Zhang, Holger Hermanns, Friedrich Eisenbrand, and David Jansen. Flow Faster: Efficient decision algorithms for probabilistic simulations. Log. Meth. Comput. Sci., 4(4), 2008. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact