Document Open Access Logo

Minimising the Probabilistic Bisimilarity Distance

Authors Stefan Kiefer , Qiyi Tang

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2024.32.pdf
  • Filesize: 0.82 MB
  • 18 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 work has been supported in part by the Engineering and Physical Sciences Research Council (EPSRC) through grant EP/X042596/1.

Acknowledgements

We thank the referees for their constructive feedback.

Cite AsGet BibTex

Stefan Kiefer and Qiyi Tang. Minimising the Probabilistic Bisimilarity Distance. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 32:1-32:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CONCUR.2024.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. The model is related to interval Markov chains. Motivated by applications to the verification of probabilistic noninterference in security, we study problems of minimising probabilistic bisimilarity distances of labelled MDPs, in particular, whether there exist strategies such that the probabilistic bisimilarity distance between the induced labelled Markov chains is less than a given rational number, both for memoryless strategies and general strategies. We show that the distance minimisation problem is ∃ℝ-complete for memoryless strategies and undecidable for general strategies. We also study the computational complexity of the qualitative problem about making the distance less than one. This problem is known to be NP-complete for memoryless strategies. We show that it is EXPTIME-complete for general strategies.

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

Related Versions

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. Patrick Billingsley. Probability and measure. Wiley Series in Probability and Statistics. Wiley, New York, NY, USA, 3rd edition, 1995. Google Scholar
  3. Vincent D. Blondel and Vincent Canterini. Undecidable problems for probabilistic automata of fixed dimension. Theory Comput. Syst., 36(3):231-245, 2003. URL: https://doi.org/10.1007/S00224-003-1061-2.
  4. John Canny. Some algebraic and geometric computations in PSPACE. In STOC, pages 460-467, 1988. Google Scholar
  5. Di Chen, Franck van Breugel, and James Worrell. On the complexity of computing probabilistic bisimilarity. In Lars Birkedal, editor, Foundations of Software Science and Computational Structures - 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, volume 7213 of Lecture Notes in Computer Science, pages 437-451. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28729-9_29.
  6. 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
  7. 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
  8. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labeled Markov systems. In Jos Baeten and Sjouke Mauw, editors, Proceedings of the 10th International Conference on Concurrency Theory, volume 1664 of Lecture Notes in Computer Science, pages 258-273, Eindhoven, The Netherlands, August 1999. Springer-Verlag. Google Scholar
  9. Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. Equivalence of labeled Markov chains. Int. J. Found. Comput. Sci., 19(3):549-563, 2008. URL: https://doi.org/10.1142/S0129054108005814.
  10. Nathanaël Fijalkow. Undecidability results for probabilistic automata. ACM SIGLOG News, 4(4):10-17, 2017. URL: https://doi.org/10.1145/3157831.3157833.
  11. 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
  12. Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, and Matthias Volk. The probabilistic model checker Storm, 2020. URL: https://arxiv.org/abs/arXiv:2002.07080.
  13. James W. Gray III. Probabilistic interference. In Proceedings of the 1990 IEEE Symposium on Security and Privacy, Oakland, California, USA, May 7-9, 1990, pages 170-179. IEEE Computer Society, 1990. URL: https://doi.org/10.1109/RISP.1990.63848.
  14. 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
  15. John G. Kemeny and J. Laurie Snell. Finite Markov Chains. Van Nostrand, 1960. Google Scholar
  16. 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.
  17. Stefan Kiefer and Qiyi Tang. Strategies for MDP Bisimilarity Equivalence and Inequivalence. In Bartek Klin, Sławomir Lasota, and Anca Muscholl, editors, 33rd International Conference on Concurrency Theory (CONCUR 2022), volume 243 of Leibniz International Proceedings in Informatics (LIPIcs), pages 32:1-32:22, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2022.32.
  18. Stefan Kiefer and Qiyi Tang. Minimising the probabilistic bisimilarity distance, 2024. URL: https://arxiv.org/abs/2406.19830.
  19. 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
  20. Kim Guldstrand Larsen and Arne Skou. Bisimulation through probabilistic testing. Inf. Comput., 94(1):1-28, 1991. Google Scholar
  21. Azaria Paz. Introduction to probabilistic automata. Academic Press, 2014. Google Scholar
  22. 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.
  23. James Renegar. On the computational complexity and geometry of the first-order theory of the reals. Parts I-III. Journal of Symbolic Computation, 13(3):255-352, 1992. Google Scholar
  24. Peter Y. A. Ryan, John D. McLean, Jonathan K. Millen, and Virgil D. Gligor. Non-interference: Who needs it? In 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 11-13 June 2001, Cape Breton, Nova Scotia, Canada, pages 237-238. IEEE Computer Society, 2001. URL: https://doi.org/10.1109/CSFW.2001.930149.
  25. 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.
  26. Marcus Schaefer. Realizability of graphs and linkages. In Thirty Essays on Geometric Graph Theory, pages 461-482. Springer, 2012. Google Scholar
  27. Marcus Schaefer and Daniel Stefankovic. Fixed points, Nash equilibria, and the existential theory of the reals. Theory Comput. Syst., 60(2):172-193, 2017. URL: https://doi.org/10.1007/s00224-015-9662-0.
  28. Marcel-Paul Schützenberger. On the definition of a family of automata. Information and Control, 4:245-270, 1961. Google Scholar
  29. 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.
  30. Qiyi Tang. Computing Probabilistic Bisimilarity Distances. Phd thesis, York University, Toronto, September 2018. Available at URL: https://yorkspace.library.yorku.ca/items/7640b6ad-edb3-4e60-8f09-3db33c817061.
  31. Qiyi Tang and Franck van Breugel. Deciding probabilistic bisimilarity distance one for labelled Markov chains. In Hana Chockler and Georg Weissenbacher, editors, Proceedings of the 30th International Conference on Computer Aided Verification, volume 10981 of Lecture Notes in Computer Science, pages 681-699, Oxford, UK, July 2018. Springer-Verlag. URL: https://doi.org/10.1007/978-3-319-96145-3_39.
  32. Wen-Guey Tzeng. A polynomial-time algorithm for the equivalence of probabilistic automata. SIAM Journal on Computing, 21(2):216-227, 1992. Google Scholar
  33. 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
  34. Franck van Breugel and James Worrell. Towards quantitative verification of probabilistic transition systems. In Fernando Orejas, Paul G. Spirakis, and Jan van Leeuwen, editors, Automata, Languages and Programming, 28th International Colloquium, ICALP 2001, Crete, Greece, July 8-12, 2001, Proceedings, volume 2076 of Lecture Notes in Computer Science, pages 421-432. Springer, 2001. URL: https://doi.org/10.1007/3-540-48224-5_35.
  35. 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 Imprint Privacy Contact