Document Open Access Logo

Strategies for MDP Bisimilarity Equivalence and Inequivalence

Authors Stefan Kiefer , Qiyi Tang

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2022.32.pdf
  • Filesize: 1.27 MB
  • 22 pages

Document Identifiers

Author Details

Stefan Kiefer
  • Department of Computer Science, University of Oxford, UK
Qiyi Tang
  • Department of Computer Science, University of Liverpool, UK

Funding

This project has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement 956123 (FOCETA).

Acknowledgements

We thank the anonymous reviewers of this paper for their constructive feedback.

Cite As Get BibTex

Stefan Kiefer and Qiyi Tang. Strategies for MDP Bisimilarity Equivalence and Inequivalence. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 32:1-32:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CONCUR.2022.32

Abstract

A labelled Markov decision process (MDP) is a labelled Markov chain with nondeterminism; i.e., together with a strategy a labelled MDP induces a labelled Markov chain. Motivated by applications to the verification of probabilistic noninterference in security, we study problems whether there exist strategies such that the labelled MDPs become bisimilarity equivalent/inequivalent. We show that the equivalence problem is decidable; in fact, it is EXPTIME-complete and becomes NP-complete if one of the MDPs is a Markov chain. Concerning the inequivalence problem, we show that (1) it is decidable in polynomial time; (2) if there are strategies for inequivalence then there are memoryless strategies for inequivalence; (3) such memoryless strategies can be computed in polynomial time.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
  • Theory of computation → Models of computation
  • Mathematics of computing → Probability and statistics
Keywords
  • Markov decision processes
  • Markov chains

Metrics

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

References

  1. Christel Baier. Polynomial time algorithms for testing probabilistic bisimulation and simulation. In Rajeev Alur and Thomas A. Henzinger, editors, Computer Aided Verification, pages 50-61, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg. Google Scholar
  2. Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to Algorithms. The MIT Press, 3rd edition, 2009. Google Scholar
  3. Benoît Delahaye. Consistency for parametric interval Markov chains. In Étienne André and Goran Frehse, editors, 2nd International Workshop on Synthesis of Complex Parameters, SynCoP 2015, April 11, 2015, London, United Kingdom, volume 44 of OASICS, pages 17-32. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. Google Scholar
  4. Salem Derisavi, Holger Hermanns, and William H. Sanders. Optimal state-space lumping in Markov chains. Inf. Process. Lett., 87(6):309-315, 2003. Google Scholar
  5. L. Doyen, T.A. Henzinger, and J.-F. Raskin. Equivalence of labeled Markov chains. International Journal on Foundations of Computer Science, 19(3):549-563, 2008. Google Scholar
  6. Nathanaël Fijalkow, Stefan Kiefer, and Mahsa Shirmohammadi. Trace refinement in labelled Markov decision processes. Logical Methods in Computer Science, 16(2), 2020. Google Scholar
  7. Ernst Moritz Hahn, Holger Hermanns, and Lijun Zhang. Probabilistic reachability for parametric Markov models. Int. J. Softw. Tools Technol. Transf., 13(1):3-19, 2011. Google Scholar
  8. Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, and Matthias Volk. The probabilistic model checker Storm, 2020. URL: http://arxiv.org/abs/arXiv:2002.07080.
  9. Bengt Jonsson and Kim Guldstrand Larsen. Specification and refinement of probabilistic processes. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), Amsterdam, The Netherlands, July 15-18, 1991, pages 266-277. IEEE Computer Society, 1991. Google Scholar
  10. John G. Kemeny and J. Laurie Snell. Finite Markov Chains. Van Nostrand, 1960. Google Scholar
  11. Stefan Kiefer and Qiyi Tang. Comparing labelled Markov decision processes. In Nitin Saxena and Sunil Simon, editors, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS, volume 182 of LIPIcs, pages 49:1-49:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2020.49.
  12. Dexter Kozen. Lower bounds for natural proof systems. In 18th Annual Symposium on Foundations of Computer Science (FOCS), pages 254-266. IEEE Computer Society, 1977. URL: https://doi.org/10.1109/SFCS.1977.16.
  13. Marta Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of probabilistic real-time systems. In G. Gopalakrishnan and S. Qadeer, editors, Proc. 23rd International Conference on Computer Aided Verification (CAV'11), volume 6806 of LNCS, pages 585-591. Springer, 2011. Google Scholar
  14. Kim Guldstrand Larsen and Arne Skou. Bisimulation through probabilistic testing. Inf. Comput., 94(1):1-28, 1991. Google Scholar
  15. Azaria Paz. Introduction to Probabilistic Automata. Academic Press, 1971. Google Scholar
  16. Andrei Popescu, Johannes Hölzl, and Tobias Nipkow. Formalizing probabilistic noninterference. In Georges Gonthier and Michael Norrish, editors, Certified Programs and Proofs - Third International Conference, volume 8307 of Lecture Notes in Computer Science, pages 259-275. Springer, 2013. URL: https://doi.org/10.1007/978-3-319-03545-1_17.
  17. Andrei Sabelfeld and David Sands. Probabilistic noninterference for multi-threaded programs. In Proceedings of the 13th IEEE Computer Security Foundations Workshop, pages 200-214. IEEE Computer Society, 2000. URL: https://doi.org/10.1109/CSFW.2000.856937.
  18. Marcel-Paul Schützenberger. On the definition of a family of automata. Information and Control, 4:245-270, 1961. Google Scholar
  19. Helmut Seidl. Haskell overloading is DEXPTIME-complete. Inf. Process. Lett., 52(2):57-60, 1994. URL: https://doi.org/10.1016/0020-0190(94)00130-8.
  20. Geoffrey Smith. Probabilistic noninterference through weak probabilistic bisimulation. In 16th IEEE Computer Security Foundations Workshop (CSFW-16 2003), pages 3-13. IEEE Computer Society, 2003. URL: https://doi.org/10.1109/CSFW.2003.1212701.
  21. Wen-Guey Tzeng. A polynomial-time algorithm for the equivalence of probabilistic automata. SIAM Journal on Computing, 21(2):216-227, 1992. Google Scholar
  22. Antti Valmari and Giuliana Franceschinis. Simple O(m logn) time Markov chain lumping. In Javier Esparza and Rupak Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6015 of Lecture Notes in Computer Science, pages 38-52. Springer, 2010. Google Scholar
  23. Tobias Winkler, Sebastian Junges, Guillermo A. Pérez, and Joost-Pieter Katoen. On the complexity of reachability in parametric markov decision processes. In Wan J. Fokkink and Rob van Glabbeek, editors, 30th International Conference on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands, volume 140 of LIPIcs, pages 14:1-14:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.14.
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 About DROPS Imprint Privacy Contact