Document Open Access Logo

A Near-Linear-Time Algorithm for Weak Bisimilarity on Markov Chains

Authors David N. Jansen , Jan Friso Groote , Ferry Timmers, Pengfei Yang

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.8.pdf
  • Filesize: 0.62 MB
  • 20 pages

Document Identifiers

Author Details

David N. Jansen
  • State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China
Jan Friso Groote
  • Department of Mathematics and Computer Science, Eindhoven University of Technology, The Netherlands
Ferry Timmers
  • Department of Mathematics and Computer Science, Eindhoven University of Technology, The Netherlands
Pengfei Yang
  • State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China
  • University of Chinese Academy of Sciences, Beijing, China

Funding

  • Jansen, David N.: This research is partly done during a visit to Eindhoven University of Technology, The Netherlands. This author is supported by the National Natural Science Foundation of China, Grants No. 61761136011 and 61532019.
  • Groote, Jan Friso: This research is partly done during a visit to the State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, P.R. China.

Cite AsGet BibTex

David N. Jansen, Jan Friso Groote, Ferry Timmers, and Pengfei Yang. A Near-Linear-Time Algorithm for Weak Bisimilarity on Markov Chains. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CONCUR.2020.8

Abstract

This article improves the time bound for calculating the weak/branching bisimulation minimisation quotient on state-labelled discrete-time Markov chains from O(m n) to an expected-time O(m log⁴ n), where n is the number of states and m the number of transitions. For these results we assume that the set of state labels AP is small (|AP| ∈ O(m/n log⁴ n)). It follows the ideas of Groote et al. (ACM ToCL 2017) in combination with an efficient algorithm to handle decremental strongly connected components (Bernstein et al., STOC 2019).

Subject Classification

ACM Subject Classification
  • Theory of computation → Random walks and Markov chains
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Probabilistic computation
  • Software and its engineering → Formal software verification
Keywords
  • Behavioural Equivalence
  • weak Bisimulation
  • Markov Chain

Metrics

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

References

  1. Christel Baier and Holger Hermanns. Weak bisimulation for fully probabilistic processes. In Orna Grumberg, editor, Computer aided verification: CAV, volume 1254 of LNCS, pages 119-130. Springer, Berlin, 1997. URL: https://doi.org/10.1007/3-540-63166-6_14.
  2. Christel Baier and Holger Hermanns. Weak bisimulation for fully probabilistic processes. Technical Report TR-CTIT-12, Center for Telematics and Information Technology, Enschede, The Netherlands, 1999. URL: https://research.utwente.nl/files/26732523/00000015.pdf.
  3. Christel Baier, Joost-Pieter Katoen, Holger Hermanns, and Verena Wolf. Comparative branching-time semantics for Markov chains. Information and computation, 200(2):149-214, 2005. URL: https://doi.org/10.1016/j.ic.2005.03.001.
  4. Aaron Bernstein, Maximilian Probst, and Christian Wulff-Nilsen. Decremental strongly-connected components and single-source reachability in near-linear time. In Moses Charikar and Edith Cohen, editors, STOC'19: Proceedings of the 51st annual ACM SIGACT symposium on theory of computing, pages 365-376. ACM, New York, 2019. URL: https://doi.org/10.1145/3313276.3316335.
  5. M. C. Browne, E. M. Clarke, and O. Grümberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical computer science, 59(1-2):115-131, 1988. URL: https://doi.org/10.1016/0304-3975(88)90098-9.
  6. Sjoerd Cranen, Jeroen J.A. Keiren, and Tim A.C. Willemse. A cure for stuttering parity games. In Abhik Roychoudhury and Meenakshi D'Souza, editors, Theoretical aspects of computing - ICTAC 2012, volume 7521 of LNCS, pages 198-212. Springer, Heidelberg, 2012. URL: https://doi.org/10.1007/978-3-642-32943-2_16.
  7. Salem Derisavi, Holger Hermanns, and William H. Sanders. Optimal state-space lumping in Markov chains. Information processing letters, 87(6):309-315, 2003. URL: https://doi.org/10.1016/S0020-0190(03)00343-0.
  8. Shimon Even and Yossi Shiloach. An on-line edge-deletion problem. Journal of the ACM, 28(1):1-4, 1981. URL: https://doi.org/10.1145/322234.322235.
  9. Rob J. Glabbeekvan Glabbeek and Peter W. Weijland. Branching time and abstraction in bisimulation semantics. Journal of the ACM, 43(3):555-600, 1996. URL: https://doi.org/10.1145/233551.233556.
  10. Jan Friso Groote, David N. Jansen, Jeroen J. A. Keiren, and Anton Wijs. An O(m log n) algorithm for computing stuttering equivalence and branching bisimulation. ACM transactions on computational logic, 18(2):Article 13, 2017. URL: https://doi.org/10.1145/3060140.
  11. Jan Friso Groote and Frits Vaandrager. An efficient algorithm for branching bisimulation and stuttering equivalence. In M. S. Paterson, editor, Automata, languages and programming [ICALP], volume 443 of LNCS, pages 626-638. Springer, Berlin, 1990. URL: https://doi.org/10.1007/BFb0032063.
  12. 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.
  13. John Hopcroft. An n log n algorithm for minimizing states in a finite automaton. In Zvi Kohavi and Azaria Paz, editors, Theory of machines and computations, pages 189-196. Academic Press, New York, 1971. URL: https://doi.org/10.1016/B978-0-12-417750-5.50022-1.
  14. David N. Jansen, Jan Friso Groote, Jeroen J. A. Keiren, and Anton Wijs. An O(m log n) algorithm for branching bisimilarity on labelled transition systems. In Armin Biere and David Parker, editors, Tools and algorithms for the construction and analysis of systems: TACAS, volume 12079 of LNCS, pages 3-20. Springer, Cham, 2020. URL: https://doi.org/10.1007/978-3-030-45237-7_1.
  15. David N. Jansen, Lei Song, and Lijun Zhang. Revisiting weak simulation for substochastic Markov chains. In Kaustubh Joshi, Markus Siegle, Mariëlle Stoelinga, and Pedro D'Argenio, editors, Quantitative evaluation of systems: QEST, volume 8054 of LNCS, pages 209-224. Springer, Heidelberg, 2013. URL: https://doi.org/10.1007/978-3-642-40196-1_18.
  16. John G. Kemeny, J. Laurie Snell, and Anthony W. Knapp. Denumerable Markov chains. Van Nostrand, Princeton, NJ, 1966. Google Scholar
  17. Marino Miculan and Marco Peressotti. Deciding weak weighted bisimulation. In Dario Della Monica, Aniello Murano, Sasha Rubin, and Luigi Sauro, editors, ICTCS 2017 and CILC 2017: Italian conference on theoretical computer science and Italian conference on computational logic, volume 1949 of CEUR Workshop Proceedings, pages 126-137. CEUR-WS.org, 2017. URL: http://ceur-ws.org/Vol-1949/ICTCSpaper11.pdf.
  18. Robin Milner. A calculus of communicating systems, volume 92 of LNCS. Springer, Berlin, 1980. URL: https://doi.org/10.1007/3-540-10235-3.
  19. Andrea Turrini and Holger Hermanns. Polynomial time decision algorithms for probabilistic automata. Information and computation, 244:134-171, 2015. URL: https://doi.org/10.1016/j.ic.2015.07.004.
  20. Antti Valmari and Giuliana Franceschinis. Simple O(m log n) time Markov chain lumping. In Javier Esparza and Rupak Majumdar, editors, Tools and algorithms for the construction and analysis of systems: TACAS, volume 6015 of LNCS, pages 38-52. Springer, Berlin, 2010. URL: https://doi.org/10.1007/978-3-642-12002-2_4.
  21. Thuy Duong Vu. Deciding orthogonal bisimulation. Formal aspects of computing, 19(4):475-485, 2007. URL: https://doi.org/10.1007/s00165-007-0023-x.
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