Document Open Access Logo

Algorithms to Compute Probabilistic Bisimilarity Distances for Labelled Markov Chains

Authors Qiyi Tang, Franck van Breugel

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2017.27.pdf
  • Filesize: 499 kB
  • 16 pages

Document Identifiers

Author Details

Qiyi Tang
Franck van Breugel

Cite AsGet BibTex

Qiyi Tang and Franck van Breugel. Algorithms to Compute Probabilistic Bisimilarity Distances for Labelled Markov Chains. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 27:1-27:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CONCUR.2017.27

Abstract

In the late nineties, Desharnais, Gupta, Jagadeesan and Panangaden presented probabilistic bisimilarity distances on the states of a labelled Markov chain. This provided a quantitative generalisation of probabilistic bisimilarity introduced by Larsen and Skou a decade earlier. In the last decade, several algorithms to approximate and compute these probabilistic bisimilarity distances have been put forward. In this paper, we correct, improve and generalise some of these algorithms. Furthermore, we compare their performance experimentally.
Keywords
  • labelled Markov chain
  • probabilistic bisimilarity
  • pseudometric
  • policy iteration

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, March 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, July/August 1996. Springer-Verlag. Google Scholar
  3. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press, Cambridge, MA, USA, 2008. Google Scholar
  4. Franck van Breugel. Probabilistic bisimilarity distances. To appear in ACM SIGLOG News, 2017. Google Scholar
  5. Franck van Breugel, Babita Sharma, and James Worrell. Approximating a behavioural pseudometric without discount. Logical Methods in Computer Science, 4(2), April 2008. Google Scholar
  6. 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
  7. John Canny. Some algebraic and geometric computations in PSPACE. In Janos Simon, editor, Proceedings of the 20th Annual ACM Symposium on Theory of Computing, pages 460-467, Chicago, IL, USA, May 1988. ACM. Google Scholar
  8. 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, March/April 2012. Springer-Verlag. Google Scholar
  9. Anne Condon. The complexity of stochastic games. Information and Computation, 96(2):203-224, February 1992. Google Scholar
  10. Anne Condon. On algorithms for simple stochastic games. In Jin-Yi Cai, editor, Advances in Computational Complexity Theory, volume 13 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 51-73. American Mathematical Society, 1993. Google Scholar
  11. Brian Davey and Hilary Priestley. Introduction to Lattices and Order. Cambridge University Press, Cambridge, United Kingdom, 2002. Google Scholar
  12. 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
  13. 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, April 1990. North-Holland. Google Scholar
  14. Frank Hitchcock. The distribution of a product from several sources to numerous localities. Studies in Applied Mathematics, 20(1/4):224-230, April 1941. Google Scholar
  15. Alan Hoffman and Richard Karp. On nonterminating stochastic games. Management Science, 12(5):359-370, January 1966. Google Scholar
  16. 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, July 1991. IEEE. Google Scholar
  17. Leonid Khachiyan. A polynomial algorithm in linear programming. Soviet Mathematics Doklady, 20(1):191-194, 1979. Google Scholar
  18. Viktor Klee and Christoph Witzgall. Facets and vertices of transportation polytopes. In George B. Dantzig and Arthur F. 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, July/August 1967. AMS. Google Scholar
  19. Donald E. Knuth and Andrew C. Yao. The complexity of nonuniform random number generation. In J.F. Traub, editor, Proceedings of a Symposium on New Directions and Recent Results in Algorithms and Complexity, pages 375-428, Pittsburgh, April 1976. Academic Press. Google Scholar
  20. Marta Kwiatkowska, Gethin Norman, and David Parker. Prism 4.0: Verification of probabilistic real-time systems. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Proceedings of the 23rd International Conference on Computer Aided Verification, volume 6806 of Lecture Notes in Computer Science, pages 585-591, Snowbird, UT, USA, July 2011. Springer-Verlag. Google Scholar
  21. 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, January 1989. ACM. Google Scholar
  22. Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 1980. Google Scholar
  23. James Orlin. A polynomial time primal network simplex algorithm for minimum cost flows. Mathematical Programming, 78(2):109-129, August 1997. Google Scholar
  24. Prakash Panangaden. Labelled Markov Processes. Imperial College Press, London, United Kingdom, 2009. Google Scholar
  25. David Park. Concurrency and automata on infinite sequences. In Peter Deussen, editor, Proceedings of 5th GI-Conference on Theoretical Computer Science, volume 104 of Lecture Notes in Computer Science, pages 167-183, Karlsruhe, Germany, March 1981. Springer-Verlag. Google Scholar
  26. Alexander Schrijver. Theory of Linear and Integer Programming. John Wiley &Sons, Chichester, UK, 1986. Google Scholar
  27. Lloyd Shapley. Stochastic games. Proceedings of the Academy of Sciences, 39(10):1095-1100, October 1953. Google Scholar
  28. 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, August 2016. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Google Scholar
  29. Alfred Tarski. A decision method for elementary algebra and geometry. University of California Press, Berkeley, CA, USA, 1951. Google Scholar
  30. Alfred Tarski. A lattice-theoretic fixed point theorem and its applications. Pacific Journal of Mathematics, 5(2):285-309, June 1955. Google Scholar
  31. Xin Zhang and Franck van Breugel. Model checking randomized algorithms with Java PathFinder. In Proceedings of the 7th International Conference on the Quantitative Evaluation of Systems, pages 157-158, Williamsburg, VA, USA, September 2010. IEEE. 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