Document Open Access Logo

Computing Probabilistic Bisimilarity Distances for Probabilistic Automata

Authors Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare, Qiyi Tang, Franck van Breugel

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2019.9.pdf
  • Filesize: 0.6 MB
  • 17 pages

Document Identifiers

Author Details

Giorgio Bacci
  • Department of Computer Science, Aalborg University, DK
Giovanni Bacci
  • Department of Computer Science, Aalborg University, DK
Kim G. Larsen
  • Department of Computer Science, Aalborg University, DK
Radu Mardare
  • Department of Computer Science, Aalborg University, DK
Qiyi Tang
  • Department of Computing, Imperial College, London, UK
Franck van Breugel
  • DisCoVeri Group, Dept. of Electrical Engineering and Computer Science, York University, Canada

Funding

Giovanni Bacci and Kim G. Larsen are funded by the ERC-Project LASSO, Radu Mardare is funded by the ASAP Project, Franck van Breugel is supported by Natural Sciences and Engineering Research Council of Canada.

Cite AsGet BibTex

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare, Qiyi Tang, and Franck van Breugel. Computing Probabilistic Bisimilarity Distances for Probabilistic Automata. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.CONCUR.2019.9

Abstract

The probabilistic bisimilarity distance of Deng et al. has been proposed as a robust quantitative generalization of Segala and Lynch’s probabilistic bisimilarity for probabilistic automata. In this paper, we present a novel characterization of the bisimilarity distance as the solution of a simple stochastic game. The characterization gives us an algorithm to compute the distances by applying Condon’s simple policy iteration on these games. The correctness of Condon’s approach, however, relies on the assumption that the games are stopping. Our games may be non-stopping in general, yet we are able to prove termination for this extended class of games. Already other algorithms have been proposed in the literature to compute these distances, with complexity in UP cap coUP and PPAD. Despite the theoretical relevance, these algorithms are inefficient in practice. To the best of our knowledge, our algorithm is the first practical solution. In the proofs of all the above-mentioned results, an alternative presentation of the Hausdorff distance due to Mémoli plays a central rôle.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
  • Theory of computation → Models of computation
  • Mathematics of computing → Probability and statistics
Keywords
  • Probabilistic automata
  • Behavioural metrics
  • Simple stochastic games
  • Simple policy iteration algorithm

Metrics

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

Related Versions

References

  1. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. On-the-Fly Exact Computation of Bisimilarity Distances. In 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2013, volume 7795 of LNCS, pages 1-15, 2013. URL: https://doi.org/10.1007/978-3-642-36742-7_1.
  2. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. Converging from Branching to Linear Metrics on Markov Chains. In 12th International Colloquium Theoretical Aspects of Computing, ICTAC 2015, volume 9399 of Lecture Notes in Computer Science, pages 349-367. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-25150-9_21.
  3. Giovanni Bacci, Giorgio Bacci, Kim G. Larsen, and Radu Mardare. On the Metric-Based Approximate Minimization of Markov Chains. In 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, volume 80 of LIPIcs, pages 104:1-104:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.104.
  4. Giovanni Bacci, Giorgio Bacci, Kim G. Larsen, and Radu Mardare. On the metric-based approximate minimization of Markov Chains. J. Log. Algebr. Meth. Program., 100:36-56, 2018. Google Scholar
  5. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008. Google Scholar
  6. Krishnendu Chatterjee, Luca de Alfaro, Rupak Majumdar, and Vishwanath Raman. Algorithms for Game Metrics. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2008, volume 2 of LIPIcs, pages 107-118. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2008. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2008.1745.
  7. Krishnendu Chatterjee, Luca de Alfaro, Rupak Majumdar, and Vishwanath Raman. Algorithms for Game Metrics (Full Version). Logical Methods in Computer Science, 6(3), 2010. URL: https://doi.org/10.2168/LMCS-6(3:13)2010.
  8. Di Chen, Franck van Breugel, and James Worrell. On the Complexity of Computing Probabilistic Bisimilarity. In 15th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2012, 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.
  9. Taolue Chen, Tingting Han, and Jian Lu. On Behavioral Metric for Probabilistic Systems: Definition and Approximation Algorithm. In 4th International Conference on Fuzzy Systems and Knowledge Discovery, FSKD 2007, pages 21-25. IEEE Computer Society, 2007. URL: https://doi.org/10.1109/FSKD.2007.426.
  10. Anne Condon. On Algorithms for Simple Stochastic Games. In Advances In Computational Complexity Theory, volume 13 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 51-72. DIMACS/AMS, 1990. Google Scholar
  11. Anne Condon. The Complexity of Stochastic Games. Inf. Comput., 96(2):203-224, 1992. URL: https://doi.org/10.1016/0890-5401(92)90048-K.
  12. Yuxin Deng, Tom Chothia, Catuscia Palamidessi, and Jun Pang. Metrics for Action-labelled Quantitative Transition Systems. Electr. Notes Theor. Comput. Sci., 153(2):79-96, 2006. URL: https://doi.org/10.1016/j.entcs.2005.10.033.
  13. Josee Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for Labelled Markov Processes. Theor. Comput. Sci., 318(3):323-354, 2004. URL: https://doi.org/10.1016/j.tcs.2003.09.013.
  14. Josée Desharnais, François Laviolette, and Mathieu Tracol. Approximate Analysis of Probabilistic Processes: Logic, Simulation and Games. In 5th International Conference on the Quantitative Evaluaiton of Systems, QEST 2008, pages 264-273. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/QEST.2008.42.
  15. Nathanaël Fijalkow, Bartek Klin, and Prakash Panangaden. Expressiveness of Probabilistic Modal Logics, Revisited. In 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, volume 80 of LIPIcs, pages 105:1-105:12. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.105.
  16. Hongfei Fu. Computing Game Metrics on Markov Decision Processes. In 39th International Colloquium on Automata, Languages, and Programming, ICALP 2012, volume 7392 of Lecture Notes in Computer Science, pages 227-238. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31585-5_23.
  17. Hongfei Fu. personal communication, 2013. Google Scholar
  18. Alessandro Giacalone, Chi-Chang Jou, and Scott A. 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. North-Holland, 1990. Google Scholar
  19. Felix Hausdorff. Grundzüge der Mengenlehre. Verlag Von Veit & Comp, Leipzig, 1914. Google Scholar
  20. Bengt Jonsson and Kim G. Larsen. Specification and Refinement of Probabilistic Processes. In 6th Annual Symposium on Logic in Computer Science, LICS 1991, pages 266-277. IEEE Computer Society, 1991. URL: https://doi.org/10.1109/LICS.1991.151651.
  21. Brendan Juba. On the Hardness of Simple Stochastic Games. Master’s thesis, Carnegie Mellon University, Pittsburgh, PA, USA, May 2005. Google Scholar
  22. Leonid Vitalevich Kantorovich. On the transfer of masses (in Russian). Doklady Akademii Nauk, 5(5-6):1-4, 1942. Translated in Management Science, 1958. Google Scholar
  23. Peter Kleinschmidt and Heinz Schannath. A Strongly Polynomial Algorithm for the Transportation Problem. Math. Program., 68:1-13, 1995. URL: https://doi.org/10.1007/BF01585755.
  24. Barbara König and Christina Mika-Michalski. (Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras. In 29th International Conference on Concurrency Theory, CONCUR 2018, volume 118 of LIPIcs, pages 37:1-37:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.37.
  25. Thomas Liggett and Steven A. Lippman. Stochastic Games with Perfect Information and Time Average Payoff. SIAM Review, 11(4):604-607, 1969. URL: https://doi.org/10.1137/1011093.
  26. Facundo Mémoli. Gromov-Wasserstein Distances and the Metric Approach to Object Matching. Foundations of Computational Mathematics, 11(4):417-487, 2011. URL: https://doi.org/10.1007/s10208-011-9093-5.
  27. Matteo Mio. On the Equivalence of Game and Denotational Semantics for the Probabilistic μ-calculus. Logical Methods in Computer Science, 8(2), 2012. URL: https://doi.org/10.2168/LMCS-8(2:7)2012.
  28. James B. Orlin. On the Simplex Algorithm for Networks and Generalized Networks, pages 166-178. Springer Berlin Heidelberg, 1985. URL: https://doi.org/10.1007/BFb0121050.
  29. Gabriel Peyré and Marco Cuturi. Computational Optimal Transport. Foundations and Trends in Machine Learning, 11(5-6):355-607, 2019. URL: https://doi.org/10.1561/2200000073.
  30. Martin L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, Inc., New York, NY, USA, 1st edition, 1994. Google Scholar
  31. Alexander Schrijver. Theory of Linear and Integer Programming. Wiley-Interscience series in Discrete Mathematics and Optimization. Wiley, 1999. Google Scholar
  32. Roberto Segala. Modeling and Verification of Randomized Distributed Real-time Systems. PhD thesis, Massachusetts Institute of Technology, Cambridge, MA, USA, 1995. Google Scholar
  33. Roberto Segala and Nancy A. Lynch. Probabilistic Simulations for Probabilistic Processes. In 5th International Conference on Concurrency Theory, CONCUR 1994, volume 836 of Lecture Notes in Computer Science, pages 481-496. Springer, 1994. URL: https://doi.org/10.1007/978-3-540-48654-1_35.
  34. Lloyd S. Shapley. Stochastic Games. Proceedings of the National Academy of Sciences, 39(10):1095-1100, 1953. URL: https://doi.org/10.1073/pnas.39.10.1095.
  35. James K. Strayer. Linear Programming and its Applications. Undergraduate Texts in Mathematics. Springer-Verlag, New York, NY, USA, 1989. URL: https://doi.org/10.1007/978-1-4612-1009-2.
  36. Qiyi Tang. Computing Probabilistic Bisimilarity Distances. PhD thesis, York University, Toronto, Canada, August 2018. Google Scholar
  37. Qiyi Tang and Franck van Breugel. Computing Probabilistic Bisimilarity Distances via Policy Iteration. In 27th International Conference on Concurrency Theory, CONCUR 2016, volume 59 of LIPIcs, pages 22:1-22:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2016.22.
  38. Qiyi Tang and Franck van Breugel. Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains. In 30th International Conference on Computer Aided Verification, CAV 2018, volume 10981 of Lecture Notes in Computer Science, pages 681-699. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-96145-3_39.
  39. Qiyi Tang and Franck van Breugel. Deciding Probabilistic Bisimilarity Distance One for Probabilistic Automata. In Sven Schewe and Lijun Zhang, editors, 29th International Conference on Concurrency Theory, CONCUR 2018, volume 118 of Leibniz International Proceedings in Informatics (LIPIcs), pages 9:1-9:17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.9.
  40. Franck van Breugel and James Worrell. The Complexity of Computing a Bisimilarity Pseudometric on Probabilistic Automata. In Horizons of the Mind. A Tribute to Prakash Panangaden - Essays Dedicated to Prakash Panangaden on the Occasion of His 60th Birthday, volume 8464 of Lecture Notes in Computer Science, pages 191-213. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-06880-0_10.
  41. Cédric Villani. Optimal Transport: Old and New. Grundlehren der mathematischen Wissenschaften. Springer, 2008. 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