Algorithms to Compute Probabilistic Bisimilarity Distances for Labelled Markov Chains
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.
labelled Markov chain
probabilistic bisimilarity
pseudometric
policy iteration
27:1-27:16
Regular Paper
Qiyi
Tang
Qiyi Tang
Franck
van Breugel
Franck van Breugel
10.4230/LIPIcs.CONCUR.2017.27
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.
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.
Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press, Cambridge, MA, USA, 2008.
Franck van Breugel. Probabilistic bisimilarity distances. To appear in ACM SIGLOG News, 2017.
Franck van Breugel, Babita Sharma, and James Worrell. Approximating a behavioural pseudometric without discount. Logical Methods in Computer Science, 4(2), April 2008.
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.
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.
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.
Anne Condon. The complexity of stochastic games. Information and Computation, 96(2):203-224, February 1992.
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.
Brian Davey and Hilary Priestley. Introduction to Lattices and Order. Cambridge University Press, Cambridge, United Kingdom, 2002.
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.
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.
Frank Hitchcock. The distribution of a product from several sources to numerous localities. Studies in Applied Mathematics, 20(1/4):224-230, April 1941.
Alan Hoffman and Richard Karp. On nonterminating stochastic games. Management Science, 12(5):359-370, January 1966.
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.
Leonid Khachiyan. A polynomial algorithm in linear programming. Soviet Mathematics Doklady, 20(1):191-194, 1979.
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.
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.
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.
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.
Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 1980.
James Orlin. A polynomial time primal network simplex algorithm for minimum cost flows. Mathematical Programming, 78(2):109-129, August 1997.
Prakash Panangaden. Labelled Markov Processes. Imperial College Press, London, United Kingdom, 2009.
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.
Alexander Schrijver. Theory of Linear and Integer Programming. John Wiley &Sons, Chichester, UK, 1986.
Lloyd Shapley. Stochastic games. Proceedings of the Academy of Sciences, 39(10):1095-1100, October 1953.
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.
Alfred Tarski. A decision method for elementary algebra and geometry. University of California Press, Berkeley, CA, USA, 1951.
Alfred Tarski. A lattice-theoretic fixed point theorem and its applications. Pacific Journal of Mathematics, 5(2):285-309, June 1955.
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.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode