Document Open Access Logo

Causally Deterministic Markov Decision Processes

Authors S. Akshay , Tobias Meggendorfer , P. S. Thiagarajan

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2024.6.pdf
  • Filesize: 0.94 MB
  • 22 pages

Document Identifiers

Author Details

S. Akshay
  • Indian Institute of Technology Bombay, Mumbai, India
Tobias Meggendorfer
  • Lancaster University Leipzig, Germany
P. S. Thiagarajan
  • The University of North Carolina at Chapel Hill, NC, USA
  • Chennai Mathematical Institute, India

Funding

  • Akshay, S.: Partially supported by Google India Research Award 2023 and SBI Foundation Hub for Data and Analytics.

Cite AsGet BibTex

S. Akshay, Tobias Meggendorfer, and P. S. Thiagarajan. Causally Deterministic Markov Decision Processes. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 6:1-6:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CONCUR.2024.6

Abstract

Probabilistic systems are often modeled using factored versions of Markov decision processes (MDPs), where the states are composed out of the local states of components and each transition involves only a small subset of the components. Concurrency arises naturally in such systems. Our goal is to exploit concurrency when analyzing factored MDPs (FMDPs). To do so, we first formulate FMDPs in a way that aids this goal and port several notions from concurrency theory to the probabilistic setting of MDPs. In particular, we provide a concurrent semantics for FMDPs based on the classical notion of event structures, thereby cleanly separating causality, concurrency, and conflicts that arise from stochastic choices. We further identify the subclass of causally deterministic FMDPs (CMDPs), where non-determinism arises solely due to concurrency. Using our event structure semantics, we show that in CMDPs, local reachability properties can be computed using a "greedy" strategy. Finally, we implement our ideas in a prototype and apply it to four models, confirming the potential for substantial improvements over state-of-the-art methods.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
Keywords
  • MDPs
  • distribution
  • causal determinism

Metrics

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

Supplementary Materials

References

  1. Samy Abbes and Albert Benveniste. True-concurrency probabilistic models: Branching cells and distributed probabilities for event structures. Information and Computation, 204(2):231-274, 2006. URL: https://doi.org/10.1016/j.ic.2005.10.001.
  2. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  3. Marco Beccuti, Giuliana Franceschinis, and Serge Haddad. Markov decision petri net and markov decision well-formed net formalisms. In Jetty Kleijn and Alexandre Yakovlev, editors, Petri Nets and Other Models of Concurrency - ICATPN 2007, 28th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, ICATPN 2007, Siedlce, Poland, June 25-29, 2007, Proceedings, volume 4546 of Lecture Notes in Computer Science, pages 43-62. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73094-1_6.
  4. Craig Boutilier, Richard Dearden, and Moisés Goldszmidt. Exploiting structure in policy construction. In Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, IJCAI 95, Montréal Québec, Canada, August 20-25 1995, 2 Volumes, pages 1104-1113. Morgan Kaufmann, 1995. URL: http://ijcai.org/Proceedings/95-2/Papers/012.pdf.
  5. Carlos E. Budde, Christian Dehnert, Ernst Moritz Hahn, Arnd Hartmanns, Sebastian Junges, and Andrea Turrini. JANI: quantitative model and tool interaction. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II, volume 10206 of Lecture Notes in Computer Science, pages 151-168, 2017. URL: https://doi.org/10.1007/978-3-662-54580-5_9.
  6. Luca de Alfaro. Formal verification of probabilistic systems. PhD thesis, Stanford University, USA, 1997. URL: https://searchworks.stanford.edu/view/3910936.
  7. Luca de Alfaro, Marta Z. Kwiatkowska, Gethin Norman, David Parker, and Roberto Segala. Symbolic model checking of probabilistic processes using mtbdds and the kronecker representation. In Susanne Graf and Michael I. Schwartzbach, editors, Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000, Proceedings, volume 1785 of Lecture Notes in Computer Science, pages 395-410. Springer, 2000. URL: https://doi.org/10.1007/3-540-46419-0_27.
  8. Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk. A storm is coming: A modern probabilistic model checker. In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, volume 10427 of Lecture Notes in Computer Science, pages 592-600. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63390-9_31.
  9. Volker Diekert and Grzegorz Rozenberg, editors. The Book of Traces. World Scientific, 1995. URL: https://doi.org/10.1142/2563.
  10. Javier Esparza. Decidability and complexity of Petri net problems - an introduction. In Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, the volumes are based on the Advanced Course on Petri Nets, held in Dagstuhl, September 1996, volume 1491 of Lecture Notes in Computer Science, pages 374-428. Springer, 1996. URL: https://doi.org/10.1007/3-540-65306-6_20.
  11. Javier Esparza and Keijo Heljanko. Unfoldings - A Partial-Order Approach to Model Checking. Monographs in Theoretical Computer Science. An EATCS Series. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-77426-6.
  12. Robert Givan, Thomas L. Dean, and Matthew Greig. Equivalence notions and model minimization in Markov decision processes. Artif. Intell., 147(1-2):163-223, 2003. URL: https://doi.org/10.1016/S0004-3702(02)00376-4.
  13. Marcus Größer and Christel Baier. Partial order reduction for Markov decision processes: A survey. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem P. de Roever, editors, Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures, volume 4111 of Lecture Notes in Computer Science, pages 408-427. Springer, 2005. URL: https://doi.org/10.1007/11804192_19.
  14. Carlos Guestrin, Daphne Koller, Ronald Parr, and Shobha Venkataraman. Efficient solution algorithms for factored MDPs. J. Artif. Intell. Res., 19:399-468, 2003. URL: https://doi.org/10.1613/JAIR.1000.
  15. Henri Hansen, Marta Z. Kwiatkowska, and Hongyang Qu. Partial order reduction for model checking Markov decision processes under unconditional fairness. In Eighth International Conference on Quantitative Evaluation of Systems, QEST 2011, Aachen, Germany, 5-8 September, 2011, pages 203-212. IEEE Computer Society, 2011. URL: https://doi.org/10.1109/QEST.2011.35.
  16. Mark Kattenbelt, Marta Z. Kwiatkowska, Gethin Norman, and David Parker. A game-based abstraction-refinement framework for Markov decision processes. Formal Methods Syst. Des., 36(3):246-280, 2010. URL: https://doi.org/10.1007/S10703-010-0097-6.
  17. Daphne Koller and Nir Friedman. Probabilistic Graphical Models - Principles and Techniques. MIT Press, 2009. URL: http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=11886.
  18. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of probabilistic real-time systems. In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 585-591. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22110-1_47.
  19. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. The PRISM benchmark suite. In Ninth International Conference on Quantitative Evaluation of Systems, QEST 2012, London, United Kingdom, September 17-20, 2012, pages 203-204. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/QEST.2012.14.
  20. Marco Ajmone Marsan, Gianfranco Balbo, Gianni Conte, Susanna Donatelli, and Giuliana Franceschinis. Modelling with generalized stochastic petri nets. SIGMETRICS Perform. Evaluation Rev., 26(2):2, 1998. URL: https://doi.org/10.1145/288197.581193.
  21. Antoni W. Mazurkiewicz. Introduction to trace theory. In Volker Diekert and Grzegorz Rozenberg, editors, The Book of Traces, pages 3-41. World Scientific, 1995. URL: https://doi.org/10.1142/9789814261456_0001.
  22. Tobias Meggendorfer. PET - A partial exploration tool for probabilistic verification. In Automated Technology for Verification and Analysis - 20th International Symposium, ATVA 2022, Virtual Event, October 25-28, 2022, Proceedings, volume 13505 of Lecture Notes in Computer Science, pages 320-326. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-19992-9_20.
  23. Tobias Meggendorfer. Causally deterministic markov decision processes, July 2024. URL: https://doi.org/10.5281/zenodo.12657579.
  24. Mogens Nielsen, Gordon D. Plotkin, and Glynn Winskel. Petri nets, event structures and domains, part I. Theor. Comput. Sci., 13:85-108, 1981. URL: https://doi.org/10.1016/0304-3975(81)90112-2.
  25. Martin L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics. Wiley, 1994. URL: https://doi.org/10.1002/9780470316887.
  26. Wolfgang Reisig. Understanding Petri Nets - Modeling Techniques, Analysis Methods, Case Studies. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-33278-4.
  27. Brigitte Rozoy and P. S. Thiagarajan. Event structures and trace monoids. Theor. Comput. Sci., 91(2):285-313, 1991. URL: https://doi.org/10.1016/0304-3975(91)90087-I.
  28. Ratul Saha, Javier Esparza, Sumit Kumar Jha, Madhavan Mukund, and P. S. Thiagarajan. Distributed Markov chains. In Deepak D'Souza, Akash Lal, and Kim Guldstrand Larsen, editors, Verification, Model Checking, and Abstract Interpretation, pages 117-134, Berlin, Heidelberg, 2015. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-662-46081-8_7.
  29. P. S. Thiagarajan and Shaofa Yang. A theory of distributed Markov chains. Fundam. Informaticae, 175(1-4):301-325, 2020. URL: https://doi.org/10.3233/FI-2020-1958.
  30. Daniele Varacca, Hagen Völzer, and Glynn Winskel. Probabilistic event structures and domains. Theoretical Computer Science, 358(2):173-199, 2006. Concurrency Theory (CONCUR 2004). URL: https://doi.org/10.1016/j.tcs.2006.01.015.
  31. Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo. Compositional probabilistic model checking with string diagrams of MDPs. In Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III, volume 13966 of Lecture Notes in Computer Science, pages 40-61. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-37709-9_3.
  32. Glynn Winskel and Mogens Nielsen. Models for concurrency, pages 1-148. Oxford University Press, Inc., USA, 1995. 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