Document Open Access Logo

Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes

Authors Raphaël Berthon, Mickael Randour, Jean-François Raskin

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2017.121.pdf
  • Filesize: 0.65 MB
  • 15 pages

Document Identifiers

Author Details

Raphaël Berthon
Mickael Randour
Jean-François Raskin

Cite As Get BibTex

Raphaël Berthon, Mickael Randour, and Jean-François Raskin. Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 121:1-121:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.ICALP.2017.121

Abstract

The beyond worst-case synthesis problem was introduced recently by Bruyère et al. [BFRR14]: it aims at building system controllers that provide strict worst-case performance guarantees against an antagonistic environment while ensuring higher expected performance against a stochastic model of the environment. Our work extends the framework of [Bruyère/Filiot/Randour/Raskin, STACS 2014] and follow-up papers, which focused on quantitative objectives, by addressing the case of omega-regular conditions encoded as parity objectives, a natural way to represent functional requirements of systems.

We build strategies that satisfy a main parity objective on all plays, while ensuring a secondary one with sufficient probability. This setting raises new challenges in comparison to quantitative objectives, as one cannot easily mix different strategies without endangering the functional properties of the system. We establish that, for all variants of this problem, deciding the existence of a strategy lies in NP and in coNP, the same complexity class as classical parity games. Hence, our framework provides additional modeling power while staying in the same complexity class.

Subject Classification

Keywords
  • Markov decision processes
  • parity objectives
  • beyond worst-case synthesis

Metrics

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

References

  1. Shaull Almagor, Orna Kupferman, and Yaron Velner. Minimizing expected cost under hard boolean constraints, with applications to quantitative synthesis. In Josée Desharnais and Radha Jagadeesan, editors, 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada, volume 59 of LIPIcs, pages 9:1-9:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2016.9.
  2. Shaull Almagor, Orna Kupferman, and Yaron Velner. Minimizing expected cost under hard boolean constraints, with applications to quantitative synthesis. CoRR, abs/1604.07064, 2016. URL: http://arxiv.org/abs/1604.07064.
  3. Christel Baier, Marcus Größer, and Frank Ciesinski. Quantitative analysis under fairness constraints. In Zhiming Liu and Anders P. Ravn, editors, Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings, volume 5799 of Lecture Notes in Computer Science, pages 135-150. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-04761-9_12.
  4. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT press, 2008. Google Scholar
  5. Raphaël Berthon, Mickael Randour, and Jean-François Raskin. Threshold constraints with guarantees for parity objectives in Markov decision processes. CoRR, abs/1702.05472, 2017. URL: http://arxiv.org/abs/1702.05472.
  6. Gilles Brassard. A note on the complexity of cryptography (corresp.). IEEE Transactions on Information Theory, 25(2):232-233, 1979. Google Scholar
  7. Tomás Brázdil, Antonín Kucera, and Petr Novotný. Optimizing the expected mean payoff in energy Markov decision processes. In Cyrille Artho, Axel Legay, and Doron Peled, editors, Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings, volume 9938 of Lecture Notes in Computer Science, pages 32-49, 2016. URL: http://dx.doi.org/10.1007/978-3-319-46520-3_3.
  8. Romain Brenguier, Lorenzo Clemente, Paul Hunter, Guillermo A. Pérez, Mickael Randour, Jean-François Raskin, Ocan Sankur, and Mathieu Sassolas. Non-zero sum games for reactive synthesis. In Adrian-Horia Dediu, Jan Janousek, Carlos Martín-Vide, and Bianca Truthe, editors, Language and Automata Theory and Applications - 10th International Conference, LATA 2016, Prague, Czech Republic, March 14-18, 2016, Proceedings, volume 9618 of Lecture Notes in Computer Science, pages 3-23. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-30000-9_1.
  9. Véronique Bruyère, Emmanuel Filiot, Mickael Randour, and Jean-François Raskin. Expectations or guarantees? I want it all! A crossroad between games and MDPs. In Fabio Mogavero, Aniello Murano, and Moshe Y. Vardi, editors, Proceedings 2nd International Workshop on Strategic Reasoning, SR 2014, Grenoble, France, April 5-6, 2014, volume 146 of EPTCS, pages 1-8, 2014. URL: http://dx.doi.org/10.4204/EPTCS.146.1.
  10. Véronique Bruyère, Emmanuel Filiot, Mickael Randour, and Jean-François Raskin. Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games. In Ernst W. Mayr and Natacha Portier, editors, 31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014, March 5-8, 2014, Lyon, France, volume 25 of LIPIcs, pages 199-213. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2014.199.
  11. Véronique Bruyère, Quentin Hautem, and Mickael Randour. Window parity games: an alternative approach toward parity games with time bounds. In Domenico Cantone and Giorgio Delzanno, editors, Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016, Catania, Italy, 14-16 September 2016, volume 226 of EPTCS, pages 135-148, 2016. URL: http://dx.doi.org/10.4204/EPTCS.226.10.
  12. Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdzinski. Mean-payoff parity games. In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings, pages 178-187. IEEE Computer Society, 2005. URL: http://dx.doi.org/10.1109/LICS.2005.26.
  13. Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Generalized parity games. In Helmut Seidl, editor, Foundations of Software Science and Computational Structures, 10th International Conference, FOSSACS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24-April 1, 2007, Proceedings, volume 4423 of Lecture Notes in Computer Science, pages 153-167. Springer, 2007. URL: http://dx.doi.org/10.1007/978-3-540-71389-0_12.
  14. Lorenzo Clemente and Jean-François Raskin. Multidimensional beyond worst-case and almost-sure problems for mean-payoff objectives. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 257-268. IEEE Computer Society, 2015. URL: http://dx.doi.org/10.1109/LICS.2015.33.
  15. Alexandre David, Peter Gjøl Jensen, Kim Guldstrand Larsen, Axel Legay, Didier Lime, Mathias Grund Sørensen, and Jakob Haahr Taankvist. On time with minimal expected cost! In Franck Cassez and Jean-François Raskin, editors, Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014, Proceedings, volume 8837 of Lecture Notes in Computer Science, pages 129-145. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-11936-6_10.
  16. E. Allen Emerson, Charanjit S. Jutla, and A. Prasad Sistla. On model-checking for fragments of μ-calculus. In Costas Courcoubetis, editor, Computer Aided Verification, 5th International Conference, CAV'93, Elounda, Greece, June 28 - July 1, 1993, Proceedings, volume 697 of Lecture Notes in Computer Science, pages 385-396. Springer, 1993. URL: http://dx.doi.org/10.1007/3-540-56922-7_32.
  17. Jerzy Filar and Koos Vrieze. Competitive Markov decision processes. Springer, 1997. Google Scholar
  18. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001], volume 2500 of Lecture Notes in Computer Science. Springer, 2002. Google Scholar
  19. Marcin Jurdzinski. Deciding the winner in parity games is in UP ∩ co-UP. Inf. Process. Lett., 68(3):119-124, 1998. URL: http://dx.doi.org/10.1016/S0020-0190(98)00150-1.
  20. Christof Löding. Optimal bounds for transformations of omega-automata. In C. Pandu Rangan, Venkatesh Raman, and Ramaswamy Ramanujam, editors, Foundations of Software Technology and Theoretical Computer Science, 19th Conference, Chennai, India, December 13-15, 1999, Proceedings, volume 1738 of Lecture Notes in Computer Science, pages 97-109. Springer, 1999. URL: http://dx.doi.org/10.1007/3-540-46691-6_8.
  21. Mickael Randour. Automated synthesis of reliable and efficient systems through game theory: A case study. In Proc. of ECCS 2012, Springer Proceedings in Complexity XVII, pages 731-738. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-319-00395-5_90.
  22. Mickael Randour. Reconciling rationality and stochasticity: Rich behavioral models in two-player games. CoRR, abs/1603.05072, 2016. GAMES 2016, the 5th World Congress of the Game Theory Society, Maastricht, Netherlands. URL: http://arxiv.org/abs/1603.05072.
  23. Mickael Randour, Jean-François Raskin, and Ocan Sankur. Variations on the stochastic shortest path problem. In Deepak D'Souza, Akash Lal, and Kim Guldstrand Larsen, editors, Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings, volume 8931 of Lecture Notes in Computer Science, pages 1-18. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-46081-8_1.
  24. Mickael Randour, Jean-François Raskin, and Ocan Sankur. Percentile queries in multi-dimensional Markov decision processes. Formal Methods in System Design, 50(2):207-248, 2017. URL: http://dx.doi.org/10.1007/s10703-016-0262-7.
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 About DROPS Imprint Privacy Contact