Document Open Access Logo

Coalgebra Encoding for Efficient Minimization

Authors Hans-Peter Deifel , Stefan Milius , Thorsten Wißmann

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2021.28.pdf
  • Filesize: 0.78 MB
  • 19 pages

Document Identifiers

Author Details

Hans-Peter Deifel
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Stefan Milius
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Thorsten Wißmann
  • Radboud University Nijmegen, The Netherlands

Funding

  • Deifel, Hans-Peter: Supported by the Deutsche Forschungsgemeinschaft (DFG) as part of the Research and Training Group 2475 "Cybercrime and Forensic Computing" (393541319/GRK2475/1-2019).
  • Milius, Stefan: Supported by Deutsche Forschungsgemeinschaft (DFG) under project MI 717/5-2.
  • Wißmann, Thorsten: Supported by NWO TOP project 612.001.852.

Acknowledgements

We would like to thank the anonymous referees for their comments, which helped us to improve the presentation.

Cite AsGet BibTex

Hans-Peter Deifel, Stefan Milius, and Thorsten Wißmann. Coalgebra Encoding for Efficient Minimization. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.FSCD.2021.28

Abstract

Recently, we have developed an efficient generic partition refinement algorithm, which computes behavioural equivalence on a state-based system given as an encoded coalgebra, and implemented it in the tool CoPaR. Here we extend this to a fully fledged minimization algorithm and tool by integrating two new aspects: (1) the computation of the transition structure on the minimized state set, and (2) the computation of the reachable part of the given system. In our generic coalgebraic setting these two aspects turn out to be surprisingly non-trivial requiring us to extend the previous theory. In particular, we identify a sufficient condition on encodings of coalgebras, and we show how to augment the existing interface, which encapsulates computations that are specific for the coalgebraic type functor, to make the above extensions possible. Both extensions have linear run time.

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
  • Theory of computation → Logic and verification
Keywords
  • Coalgebra
  • Partition refinement
  • Transition systems
  • Minimization

Metrics

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

Related Versions

References

  1. Jiří Adámek, Filippo Bonchi, Barbara König, Mathias Hülsbusch, Stefan Milius, and Alexandra Silva. A coalgebraic perspective on minimization and determinization. In Lars Birkedal, editor, Proc. Foundations of Software Science and Computation Structures (FoSSaCS), volume 7213 of Lecture Notes Comput. Sci., pages 58-73. Springer, 2012. Google Scholar
  2. Jiří Adámek, Stefan Milius, and Lawrence S. Moss. Initial algebras, terminal coalgebras, and the theory of fixed points of functors. draft book, July 2020. URL: https://www8.cs.fau.de/ext/milius/publications/files/CoalgebraBook.pdf.
  3. Jiří Adámek, Stefan Milius, Lawrence S. Moss, and Lurdes Sousa. Well-pointed coalgebras. Log. Methods Comput. Sci., 9(2):1-51, 2014. Google Scholar
  4. Michael A. Arbib and Ernest G. Manes. Adjoint machines, state-behaviour machines, and duality. J. Pure Appl. Algebra, 6:313-344, 1975. Google Scholar
  5. Michael A. Arbib and Ernest G. Manes. Algebraic Approaches to Program Semantics. Texts and Monographs in Computer Science. Springer, 1986. Google Scholar
  6. Christel Baier, Bettina Engelen, and Mila Majster-Cederbaum. Deciding bisimilarity and similarity for probabilistic processes. J. Comput. Syst. Sci., 60:187-231, 2000. URL: https://doi.org/10.1006/jcss.1999.1683.
  7. Falk Bartels, Ana Sokolova, and Erik de Vink. A hierarchy of probabilistic system types. Theoretical Computer Science, 327:3-22, 2004. Google Scholar
  8. Damien Bergamini, Nicolas Descoubes, Christophe Joubert, and Radu Mateescu. 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 Lecture Notes in Comput. Sci., pages 581-585. Springer, 2005. URL: https://doi.org/10.1007/b107194.
  9. Christoph Berkholz, Paul S. Bonsma, and Martin Grohe. Tight lower and upper bounds for the complexity of canonical colour refinement. Theory Comput. Syst., 60(4):581-614, 2017. URL: https://doi.org/10.1007/s00224-016-9686-0.
  10. Nick Bezhanishvili, Marcello Bonsangue, Helle Hvid Hansen, Dexter Kozen, Clemens Kupke, Prakash Panangaden, and Alexandra Silva. Minimisation in logical form. Technical report, Cornell University, May 2020. available at URL: https://arxiv.org/abs/2005.11551.
  11. Stefan Blom and Simona Orzan. Distributed branching bisimulation reduction of state spaces. In Parallel and Distributed Model Checking, PDMC 2003, volume 89 of Electron. Notes Theor. Comput. Sci., pages 99-113. Elsevier, 2003. Google Scholar
  12. Stefan Blom and Simona Orzan. A distributed algorithm for strong bisimulation reduction of state spaces. STTT, 7(1):74-86, 2005. URL: https://doi.org/10.1007/s10009-004-0159-4.
  13. Mikołaj Bojańczyk, Bartek Klin, and Slawomir Lasota. Automata theory in nominal sets. Log. Methods Comput. Sci., 10(3), 2014. URL: https://doi.org/10.2168/LMCS-10(3:4)2014.
  14. Filippo Bonchi, Marcello Bonsangue, Helle Hvid Hansen, Prakash Panangaden, Jan Rutten, and Alexandra Silva. Algebra-coalgebra duality in Brzozowski’s minimization algorithm. ACM Trans. Comput. Log., 15(1):3:1-3:29, 2014. Google Scholar
  15. Filippo Bonchi, Marcello Bonsangue, Jan Rutten, and Alexandra Silva. Brzozowski’s algorithm (co)algebraically. In Robert L. Constable and Alexandra Silva, editors, Logic and Program Semantics, Kozen Festschrift, volume 7230 of Lecture Notes in Comput. Sci., pages 12-23. Springer, 2012. Google Scholar
  16. Janusz A. Brzozowski. Canonical regular expressions and minimal state graphs for definite events. In J. Fox, editor, Mathematical Theory of Automata, volume 12 of MRI Symposia Series, pages 529-561. Polytechnic Institute of Brooklyn, Polytechnic Press, 1962. Google Scholar
  17. Jin-Yi Cai, Martin Fürer, and Neil Immerman. An optimal lower bound on the number of variables for graph identification. Combinatorica, 12(4):389-410, December 1992. URL: https://doi.org/10.1007/bf01305232.
  18. Stefano Cattani and Roberto Segala. Decision algorithms for probabilistic bisimulation. In Concurrency Theory, CONCUR 2002, volume 2421 of Lecture Notes in Comput. Sci., pages 371-385. Springer, 2002. URL: https://doi.org/10.1007/3-540-45694-5.
  19. CoPaR: The Coalgebraic Partion Refiner, February 2021. Available at URL: https://git8.cs.fau.de/software/copar.
  20. Hans-Peter Deifel, Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Generic partition refinement and weighted tree automata. In Maurice H. ter Beek, Annabelle McIver, and José N. Oliveira, editors, Formal Methods - The Next 30 Years, pages 280-297, Cham, October 2019. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-30942-8_18.
  21. Hans-Peter Deifel, Stefan Milius, and Thorsten Wißmann. Coalgebra encoding for efficient minimization. full version with appendix. URL: http://arxiv.org/abs/2102.12842.
  22. Salem Derisavi, Holger Hermanns, and William Sanders. Optimal state-space lumping in markov chains. Inf. Process. Lett., 87(6):309-315, 2003. URL: https://doi.org/10.1016/S0020-0190(03)00343-0.
  23. Ulrich Dorsch, Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Efficient coalgebraic partition refinement. In Roland Meyer and Uwe Nestmann, editors, 28th International Conference on Concurrency Theory (CONCUR 2017), volume 85 of LIPIcs, pages 28:1-28:16. Schloss Dagstuhl, 2017. Google Scholar
  24. Hubert Garavel and Holger Hermanns. On combining functional verification and performance evaluation using CADP. In Formal Methods Europe, FME 2002, volume 2391 of Lecture Notes in Comput. Sci., pages 410-429. Springer, 2002. URL: https://doi.org/10.1007/3-540-45614-7.
  25. Jan Groote, David Jansen, Jeroen Keiren, and Anton Wijs. An O(mlogn) algorithm for computing stuttering equivalence and branching bisimulation. ACM Trans. Comput. Log., 18(2):13:1-13:34, 2017. URL: https://doi.org/10.1145/3060140.
  26. Jan Friso Groote, Jao Rivera Verduzco, and Erik P. de Vink. An efficient algorithm to determine probabilistic bisimulation. Algorithms, 11(9):131, 2018. URL: https://doi.org/10.3390/a11090131.
  27. H. Peter Gumm. Thomas Ihringer: Algemeine Algebra. Mit einem Anhang über Universelle Coalgebra von H. P. Gumm, volume 10 of Berliner Studienreihe zur Mathematik. Heldermann Verlag, 2003. Google Scholar
  28. H. Peter Gumm. From T-coalgebras to filter structures and transition systems. In José Luiz Fiadeiro, Neil Harman, Markus Roggenbach, and Jan Rutten, editors, Algebra and Coalgebra in Computer Science, volume 3629 of Lecture Notes in Comput. Sci., pages 194-212. Springer Berlin Heidelberg, 2005. URL: https://doi.org/10.1007/11548133_13.
  29. Johanna Högberg, Andreas Maletti, and Jonathan May. Backward and forward bisimulation minimization of tree automata. Theoret. Comput. Sci., 410:3539-3552, 2009. Google Scholar
  30. 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
  31. Dung Huynh and Lu Tian. On some equivalence relations for probabilistic processes. Fund. Inform., 17:211-234, 1992. Google Scholar
  32. 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 Lecture Notes in Comput. Sci., pages 87-101. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-71209-1.
  33. 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 Lecture Notes in Comput. Sci., pages 121-139. Springer, 2009. Google Scholar
  34. Barbara König and Sebastian Küppers. A generalized partition refinement algorithm, instantiated to language equivalence checking for weighted automata. Soft Comput., 22:1103-1120, 2018. Google Scholar
  35. Nick Nick Bezhanishvili, Clemens Kupke, and Prakash Panangaden. Minimization via duality. In Luke Ong and R. de Queiroz, editors, Proc. WoLLIC, volume 7456 of Lecture Notes in Comput. Sci. Springer, 2012. Google Scholar
  36. Robert Paige and Robert E. Tarjan. Three partition refinement algorithms. SIAM J. Comput., 16(6):973-989, 1987. Google Scholar
  37. Francesco Ranzato and Francesco Tapparo. Generalizing the Paige-Tarjan algorithm by abstract interpretation. Inf. Comput., 206:620-651, 2008. URL: https://doi.org/10.1016/j.ic.2008.01.001.
  38. Jurriaan Rot. Coalgebraic minimization of automata by initiality and finality. In Lars Birkedal, editor, Proc. MFPS, volume 325 of Electron. Notes Theor. Comput. Sci., pages 253-276. Elsevier, 2016. Google Scholar
  39. J.J.M.M. Rutten. Universal coalgebra: a theory of systems. Theoret. Comput. Sci., 249(1):3-80, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00056-6.
  40. Lutz Schröder, Dexter Kozen, Stefan Milius, and Thorsten Wißmann. Nominal automata with name binding. In Foundations of Software Science and Computation Structures, FOSSACS 2017, volume 10203 of Lecture Notes in Comput. Sci., pages 124-142, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7.
  41. Deian Tabakov and Moshe Vardi. Experimental evaluation of classical automata constructions. In G. Sutcliffe and A. Voronkov, editors, Proc. LPAR, volume 3835 of Lecture Notes in Artificial Intelligence, pages 396-411. Springer, 2005. Google Scholar
  42. Věra Trnková. On a descriptive classification of set functors I. Comment. Math. Univ. Carolin., 12:143-174, 1971. Google Scholar
  43. Antti Valmari. Bisimilarity minimization in 𝒪(m log n) time. In Applications and Theory of Petri Nets, PETRI NETS 2009, volume 5606 of Lecture Notes in Comput. Sci., pages 123-142. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02424-5.
  44. 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 Lecture Notes in Comput. Sci., pages 38-52. Springer, 2010. Google Scholar
  45. Tom van Dijk and Jaco van de Pol. Multi-core symbolic bisimulation minimization. J. Softw. Tools Technol. Transfer, 20(2):157-177, 2018. Google Scholar
  46. Boris Weisfeiler. On Construction and Identification of Graphs. Springer, 1976. URL: https://doi.org/10.1007/bfb0089374.
  47. Anton Wijs. Gpu accelerated strong and branching bisimilarity checking. In Christel Baier and Cesare Tinelli, editors, Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 9035 of Lecture Notes in Comput. Sci., pages 368-383. Springer, 2015. Google Scholar
  48. Thorsten Wißmann, Ulrich Dorsch, Stefan Milius, and Lutz Schröder. Efficient and modular coalgebraic partition refinement. Log. Methods. Comput. Sci., 16(1):8:1-8:63, 2020. Google Scholar
  49. Thorsten Wißmann, Stefan Milius, Jérémy Dubut, and Shin-ya Katsumata. A coalgebraic view on reachability. Comment. Math. Univ. Carolin., 60(4), 2019. Google Scholar
  50. Thorsten Wißmann. Coalgebraic Semantics and Minimization in Sets and Beyond. Phd thesis, Friedrich-Alexander-Universität Erlangen-Nürnberg (FAU), 2020. URL: https://opus4.kobv.de/opus4-fau/frontdoor/index/index/docId/14222.
  51. Thorsten Wißmann, Hans-Peter Deifel, Stefan Milius, and Lutz Schröder. From generic partition refinement to weighted tree automata minimization, 2020. accepted for publication in Formal Aspects of Computing; available online at https://arxiv.org/abs/2004.01250. URL: http://arxiv.org/abs/2004.01250.
  52. Lijun Zhang, Holger Hermanns, Friedrich Eisenbrand, and David Jansen. Flow Faster: Efficient decision algorithms for probabilistic simulations. Log. Meth. Comput. Sci., 4(4), 2008. URL: https://doi.org/10.2168/LMCS-4(4:6)2008.
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