Document Open Access Logo

Comparing Labelled Markov Decision Processes

Authors Stefan Kiefer , Qiyi Tang

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2020.49.pdf
  • Filesize: 0.58 MB
  • 16 pages

Document Identifiers

Author Details

Stefan Kiefer
  • Department of Computer Science, University of Oxford, UK
Qiyi Tang
  • Department of Computer Science, University of Oxford, UK

Funding

  • Kiefer, Stefan: Supported by a Royal Society University Fellowship.

Acknowledgements

We thank the anonymous reviewers of this paper for their constructive feedback.

Cite AsGet BibTex

Stefan Kiefer and Qiyi Tang. Comparing Labelled Markov Decision Processes. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 49:1-49:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSTTCS.2020.49

Abstract

A labelled Markov decision process 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 of equivalence checking for the verification of anonymity, we study the algorithmic comparison of two labelled MDPs, in particular, whether there exist strategies such that the MDPs become equivalent/inequivalent, both in terms of trace equivalence and in terms of probabilistic bisimilarity. We provide the first polynomial-time algorithms for computing memoryless strategies to make the two labelled MDPs inequivalent if such strategies exist. We also study the computational complexity of qualitative problems about making the total variation distance and the probabilistic bisimilarity distance less than one or equal to one.

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
  • Behavioural metrics

Metrics

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

Related Versions

References

  1. Sanjeev Arora, Rong Ge, Ravi Kannan, and Ankur Moitra. Computing a nonnegative matrix factorization - provably. In STOC, pages 145-162. ACM, 2012. Google Scholar
  2. 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
  3. Michael Benedikt, Rastislav Lenhardt, and James Worrell. LTL model checking of interval Markov chains. In Nir Piterman and Scott A. Smolka, editors, Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, volume 7795 of Lecture Notes in Computer Science, pages 32-46. Springer, 2013. Google Scholar
  4. Patrick Billingsley. Probability and measure. Wiley Series in Probability and Statistics. Wiley, New York, NY, USA, 3rd edition, 1995. Google Scholar
  5. John Canny. Some algebraic and geometric computations in PSPACE. In STOC, pages 460-467, 1988. Google Scholar
  6. Souymodip Chakraborty and Joost-Pieter Katoen. Model checking of open interval Markov chains. In Marco Gribaudo, Daniele Manini, and Anne Remke, editors, Analytical and Stochastic Modelling Techniques and Applications, pages 30-42. Springer International Publishing, 2015. Google Scholar
  7. Krishnendu Chatterjee, Koushik Sen, and Thomas A. Henzinger. Model-checking omega-regular properties of interval Markov chains. In Roberto M. Amadio, editor, Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29 - April 6, 2008. Proceedings, volume 4962 of Lecture Notes in Computer Science, pages 302-317. Springer, 2008. 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. Taolue Chen and Stefan Kiefer. On the total variation distance of labelled Markov chains. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, New York, NY, USA, 2014. ACM. Google Scholar
  10. Joel E. Cohen and Uriel G. Rothblum. Nonnegative ranks, decompositions, and factorizations of nonnegative matrices. Linear Algebra and its Applications, 190:149-168, 1993. Google Scholar
  11. 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
  12. Benoît Delahaye, Kim G. Larsen, Axel Legay, Mikkel L. Pedersen, and Andrzej Wasowski. Decision problems for interval Markov chains. In Adrian-Horia Dediu, Shunsuke Inenaga, and Carlos Martín-Vide, editors, Language and Automata Theory and Applications - 5th International Conference, LATA 2011, Tarragona, Spain, May 26-31, 2011. Proceedings, volume 6638 of Lecture Notes in Computer Science, pages 274-285. Springer, 2011. Google Scholar
  13. 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
  14. 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
  15. Josee Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled Markov processes. Theor. Comput. Sci., 318(3):323-354, 2004. Google Scholar
  16. L. Doyen, T.A. Henzinger, and J.-F. Raskin. Equivalence of labeled Markov chains. International Journal on Foundations of Computer Science, 19(3):549-563, 2008. Google Scholar
  17. Nathanaël Fijalkow, Stefan Kiefer, and Mahsa Shirmohammadi. Trace refinement in labelled Markov decision processes. Logical Methods in Computer Science, 16(2), 2020. Google Scholar
  18. 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
  19. Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, and Matthias Volk. The probabilistic model checker Storm, 2020. URL: http://arxiv.org/abs/arXiv:2002.07080.
  20. 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
  21. John G. Kemeny and J. Laurie Snell. Finite Markov Chains. Springer, 1976. Google Scholar
  22. S. Kiefer, A.S. Murawski, J. Ouaknine, B. Wachter, and J. Worrell. Language equivalence for probabilistic automata. In CAV, volume 6806 of LNCS, pages 526-540. Springer, 2011. Google Scholar
  23. S. Kiefer, A.S. Murawski, J. Ouaknine, B. Wachter, and J. Worrell. APEX: An analyzer for open probabilistic programs. In CAV, volume 7358 of LNCS, pages 693-698. Springer, 2012. Google Scholar
  24. Stefan Kiefer and Qiyi Tang. Comparing labelled markov decision processes, 2020. URL: http://arxiv.org/abs/2009.11643.
  25. M. Kwiatkowska, G. Norman, and D. 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
  26. Kim Guldstrand Larsen and Arne Skou. Bisimulation through probabilistic testing. Inf. Comput., 94(1):1-28, 1991. Google Scholar
  27. L. Li and Y. Feng. Quantum Markov chains: Description of hybrid systems, decidability of equivalence, and model checking linear-time properties. Information and Computation, 244:229-244, 2015. Google Scholar
  28. T.M. Ngo, M. Stoelinga, and M. Huisman. Confidentiality for probabilistic multi-threaded programs and its verification. In Engineering Secure Software and Systems, volume 7781 of LNCS, pages 107-122. Springer, 2013. Google Scholar
  29. A. Paz. Introduction to Probabilistic Automata. Academic Press, 1971. Google Scholar
  30. S. Peyronnet, M. de Rougemont, and Y. Strozecki. Approximate verification and enumeration problems. In ICTAC, volume 7521 of LNCS, pages 228-242. Springer, 2012. Google Scholar
  31. 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
  32. 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.
  33. M.-P. Schützenberger. On the definition of a family of automata. Information and Control, 4:245-270, 1961. Google Scholar
  34. Koushik Sen, Mahesh Viswanathan, and Gul Agha. Model-checking markov chains in the presence of uncertainties. In Holger Hermanns and Jens Palsberg, editors, Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006, Proceedings, volume 3920 of Lecture Notes in Computer Science, pages 394-410. Springer, 2006. Google Scholar
  35. Yaroslav Shitov. A universality theorem for nonnegative matrix factorizations, 2016. URL: http://arxiv.org/abs/1606.09068.
  36. 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.
  37. Qiyi Tang and Franck van Breugel. Deciding probabilistic bisimilarity distance one for probabilistic automata. Journal of Computer and System Sciences, 111:57-84, 2020. Google Scholar
  38. Wen-Guey Tzeng. A polynomial-time algorithm for the equivalence of probabilistic automata. SIAM Journal on Computing, 21(2):216-227, 1992. Google Scholar
  39. 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
  40. Stephen A. Vavasis. On the complexity of nonnegative matrix factorization. SIAM Journal on Optimization, 20(3):1364-1377, 2009. Google Scholar
  41. 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