Document Open Access Logo

Deciding Probabilistic Bisimilarity Distance One for Probabilistic Automata

Authors Qiyi Tang, Franck van Breugel

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2018.9.pdf
  • Filesize: 446 kB
  • 17 pages

Document Identifiers

Author Details

Qiyi Tang
  • Department of Computing, Imperial College, London, United Kingdom
Franck van Breugel
  • Department of Electrical Engineering and Computer Science, York University, Toronto, Canada

Funding

Natural Sciences and Engineering Research Council of Canada

Cite AsGet BibTex

Qiyi Tang and Franck van Breugel. Deciding Probabilistic Bisimilarity Distance One for Probabilistic Automata. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.CONCUR.2018.9

Abstract

Probabilistic bisimilarity, due to Segala and Lynch, is an equivalence relation that captures which states of a probabilistic automaton behave exactly the same. Deng, Chothia, Palamidessi and Pang proposed a robust quantitative generalization of probabilistic bisimilarity. Their probabilistic bisimilarity distances of states of a probabilistic automaton capture the similarity of their behaviour. The smaller the distance, the more alike the states behave. In particular, states are probabilistic bisimilar if and only if their distance is zero. Although the complexity of computing probabilistic bisimilarity distances for probabilistic automata has already been studied and shown to be in NP cap coNP and PPAD, we are not aware of any practical algorithm to compute those distances. In this paper we provide several key results towards algorithms to compute probabilistic bisimilarity distances for probabilistic automata. In particular, we present a polynomial time algorithm that decides distance one. Furthermore, we give an alternative characterization of the probabilistic bisimilarity distances as a basis for a policy iteration algorithm.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Markov processes
  • Theory of computation → Concurrency
Keywords
  • probabilistic automaton
  • probabilistic bisimilarity
  • distance

Metrics

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

References

  1. Giorgio Bacci, Giovanni Bacci, Kim Larsen, and Radu Mardare. On-the-fly exact computation of bisimilarity distances. In Nir Piterman and Scott Smolka, editors, Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 7795 of Lecture Notes in Computer Science, pages 1-15, Rome, Italy, 2013. Springer-Verlag. Google Scholar
  2. Christel Baier. Polynomial time algorithms for testing probabilistic bisimulation and simulation. In Rajeev Alur and Thomas Henzinger, editors, Proceedings of the 8th International Conference on Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 50-61, New Brunswick, NJ, USA, 1996. Springer-Verlag. Google Scholar
  3. Jaco de Bakker and Erik de Vink. Control flow semantics. MIT Press, Cambridge, MA, USA, 1996. Google Scholar
  4. Jaco de Bakker and Jeffery Zucker. Denotational semantics of concurrency. In Proceedings of the 14th Annual ACM Symposium on Theory of Computing, pages 153-158, San Francisco, 1982. ACM. Google Scholar
  5. Stefan Banach. Sur les opérations dans les ensembles abstraits et leurs applications aux equations intégrales. Fundamenta Mathematicae, 3:133-181, 1922. Google Scholar
  6. Franck van Breugel. Probabilistic bisimilarity distances. SIGLOG News, 4(4):33-51, 2017. Google Scholar
  7. Franck van Breugel and James Worrell. Towards quantitative verification of probabilistic systems. In Fernando Orejas, Paul Spirakis, and Jan van Leeuwen, editors, Proceedings of 28th International Colloquium on Automata, Languages and Programming, volume 2076 of Lecture Notes in Computer Science, pages 421-432, Crete, 2001. Springer-Verlag. Google Scholar
  8. Franck van Breugel and James Worrell. The complexity of computing a bisimilarity pseudometric on probabilistic automata. In Franck van Breugel, Elham Kashefi, Catuscia Palamidessi, and Jan Rutten, editors, Horizons of the Mind - A Tribute to Prakash Panangaden, volume 8464 of Lecture Notes in Computer Science, pages 191-213. Springer-Verlag, 2014. Google Scholar
  9. Di Chen, Franck van Breugel, and James Worrell. On the complexity of computing probabilistic bisimilarity. In Lars Birkedal, editor, Proceedings of the 15th International Conference on Foundations of Software Science and Computational Structures, volume 7213 of Lecture Notes in Computer Science, pages 437-451, Tallinn, Estonia, 2012. Springer-Verlag. Google Scholar
  10. Edmund Clarke, Orna Grumberg, and Doron Peled. Model checking. MIT Press, Cambridge, MA, USA, 1999. Google Scholar
  11. Brian Davey and Hilary Priestley. Introduction to lattices and order. Cambridge University Press, Cambridge, United Kingdom, 2002. Google Scholar
  12. Yuxin Deng, Tom Chothia, Catuscia Palamidessi, and Jun Pang. Metrics for action-labelled quantitative transition systems. In Antonio Cerone and Herbert Wiklicky, editors, Proceedings of the 3rd Workshop on Quantitative Aspects of Programming Languages, volume 153(2) of Electronic Notes in Theoretical Computer Science, pages 79-96, Edinburgh, Scotland, 2005. Elsevier. Google Scholar
  13. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. The metric analogue of weak bisimulation for probabilistic processes. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, pages 413-422, Copenhagen, Denmark, 2002. IEEE. Google Scholar
  14. Jerzy Filar and Koos Vrieze. Competitive Markov decision processes. Springer-Verlag, New York, NY, USA, 1997. Google Scholar
  15. Hongfei Fu. Computing game metrics on Markov decision processes. In Artur Czumaj, Kurt Mehlhorn, Andrew Pitts, and Roger Wattenhofer, editors, Proceedings of the 39th International Colloquium on Automata, Languages, and Programming, volume 7392 of Lecture Notes in Computer Science, pages 227-238, Warwick, UK, 2012. Springer-Verlag. Google Scholar
  16. Hongfei Fu. Personal communication, 2013. Google Scholar
  17. Alessandro Giacalone, Chi-Chang Jou, and Scott Smolka. Algebraic reasoning for probabilistic concurrent systems. In Proceedings of the IFIP WG 2.2/2.3 Working Conference on Programming Concepts and Methods, pages 443-458, Sea of Gallilee, Israel, 1990. North-Holland. Google Scholar
  18. Felix Hausdorff. Grundzüge der Mengenlehre. Von Veit &Comp., Leipzig, 1914. Google Scholar
  19. Alan Hoffman and Richard Karp. On nonterminating stochastic games. Management Science, 12(5):359-370, 1966. Google Scholar
  20. Ronald Howard. Dynamic Programming and Markov Processes. The MIT Press, Cambridge, MA, USA, 1960. Google Scholar
  21. Bengt Jonsson and Kim Larsen. Specification and refinement of probabilistic processes. In Proceedings of the 6th Annual Symposium on Logic in Computer Science, pages 266-277, Amsterdam, The Netherlands, 1991. IEEE. Google Scholar
  22. Leonid Kantorovich. On the transfer of masses (in Russian). Doklady Akademii Nauk, 5(1):1-4, 1942. Translated in Management Science, 5(1):1-4, 1958. Google Scholar
  23. Viktor Klee and Christoph Witzgall. Facets and vertices of transportation polytopes. In George Dantzig and Arthur Veinott, editors, Proceedings of 5th Summer Seminar on the Mathematis of the Decision Sciences, volume 11 of Lectures in Applied Mathematics, pages 257-282, Stanford, CA, USA, 1967. AMS. Google Scholar
  24. Bronisław Knaster. Un théorème sur les fonctions d'ensembles. Annales de la Société Polonaise de Mathématique, 6:133-134, 1928. Google Scholar
  25. Kim Larsen and Arne Skou. Bisimulation through probabilistic testing. In Proceedings of the 16th Annual ACM Symposium on Principles of Programming Languages, pages 344-352, Austin, TX, USA, 1989. ACM. Google Scholar
  26. James Orlin. A polynomial time primal network simplex algorithm for minimum cost flows. Mathematical Programming, 78(2):109-129, 1997. Google Scholar
  27. Roberto Segala. Modeling and verification of randomized distributed real-time systems. PhD thesis, Massachusetts Institute of Technology, Cambridge, MA, USA, 1995. Google Scholar
  28. Roberto Segala and Nancy Lynch. Probabilistic simulations for probabilistic processes. In Bengt Jonsson and Joachim Parrow, editors, Proceedings of the 5th International Conference on Concurrency Theory, volume 836 of Lecture Notes in Computer Science, pages 481-496, Uppsala, Sweden, 1994. Springer-Verlag. Google Scholar
  29. Denis Serre. Matrices: theory and applications. Springer-Verlag, New York, NY, USA, 2010. Google Scholar
  30. Colin Stirling. Bisimulation, modal logic and model checking games. Logic Journal of the IGPL, 7(1):103-124, 1999. Google Scholar
  31. Qiyi Tang and Franck van Breugel. Computing probabilistic bisimilarity distances via policy iteration. In Josée Desharnais and Radha Jagadeesan, editors, Proceedings of the 27th International Conference on Concurrency Theory, volume 59 of Leibniz International Proceedings in Informatics, pages 22:1-22:15, Quebec City, QC, Canada, 2016. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Google Scholar
  32. 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, 2018. Springer-Verlag. Google Scholar
  33. Alfred Tarski. A lattice-theoretic fixed point theorem and its applications. Pacific Journal of Mathematics, 5(2):285-309, 1955. Google Scholar
  34. Mathieu Tracol, Josée Desharnais, and Abir Zhioua. Computing distances between probabilistic automata. In Mieke Massink and Gethin Norman, editors, Proceedings 9th Workshop on Quantitative Aspects of Programming Languages, volume 57 of Electronic Proceedings in Theoretical Computer Science, pages 148-162, Saarbrücken, Germany, 2011. Elsevier. 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