Document Open Access Logo

Pareto-Rational Verification

Authors Véronique Bruyère, Jean-François Raskin, Clément Tamines

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2022.33.pdf
  • Filesize: 0.76 MB
  • 20 pages

Document Identifiers

Author Details

Véronique Bruyère
  • Université de Mons (UMONS), Mons, Belgium
Jean-François Raskin
  • Université libre de Bruxelles (ULB), Brussels, Belgium
Clément Tamines
  • Université de Mons (UMONS), Mons, Belgium

Funding

This work is partially supported by the two PDR projects Subgame perfection in graph games and Rational (F.R.S.-FNRS), the ARC project Non-Zero Sum Game Graphs: Applications to Reactive Synthesis and Beyond (Fédération Wallonie-Bruxelles), the EOS project Verifying Learning Artificial Intelligence Systems (F.R.S.-FNRS and FWO), and the COST Action 16228 GAMENET (European Cooperation in Science and Technology).

Cite AsGet BibTex

Véronique Bruyère, Jean-François Raskin, and Clément Tamines. Pareto-Rational Verification. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 33:1-33:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CONCUR.2022.33

Abstract

We study the rational verification problem which consists in verifying the correctness of a system executing in an environment that is assumed to behave rationally. We consider the model of rationality in which the environment only executes behaviors that are Pareto-optimal with regard to its set of objectives, given the behavior of the system (which is committed in advance of any interaction). We examine two ways of specifying this behavior, first by means of a deterministic Moore machine, and then by lifting its determinism. In the latter case the machine may embed several different behaviors for the system, and the universal rational verification problem aims at verifying that all of them are correct when the environment is rational. For parity objectives, we prove that the Pareto-rational verification problem is co-NP-complete and that its universal version is in PSPACE and both NP-hard and co-NP-hard. For Boolean Büchi objectives, the former problem is Π₂𝖯-complete and the latter is PSPACE-complete. We also study the case where the objectives are expressed using LTL formulas and show that the first problem is PSPACE-complete, and that the second is 2EXPTIME-complete. Both problems are also shown to be fixed-parameter tractable for parity and Boolean Büchi objectives.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal methods
  • Theory of computation → Logic and verification
  • Theory of computation → Solution concepts in game theory
Keywords
  • Rational verification
  • Model-checking
  • Pareto-optimality
  • ω-regular objectives

Metrics

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

Related Versions

References

  1. Alessandro Abate, Julian Gutierrez, Lewis Hammond, Paul Harrenstein, Marta Kwiatkowska, Muhammad Najib, Giuseppe Perelli, Thomas Steeples, and Michael J. Wooldridge. Rational verification: game-theoretic verification of multi-agent systems. Appl. Intell., 51(9):6569-6584, 2021. URL: https://doi.org/10.1007/s10489-021-02658-y.
  2. Rajeev Alur, Aldric Degorre, Oded Maler, and Gera Weiss. On omega-languages defined by mean-payoff conditions. In Luca de Alfaro, editor, Foundations of Software Science and Computational Structures, 12th International Conference, FOSSACS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, volume 5504 of Lecture Notes in Computer Science, pages 333-347. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00596-1_24.
  3. Christel Baier, Frantisek Blahoudek, Alexandre Duret-Lutz, Joachim Klein, David Müller, and Jan Strejcek. Generic emptiness check for fun and profit. In Yu-Fang Chen, Chih-Hong Cheng, and Javier Esparza, editors, Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, volume 11781 of Lecture Notes in Computer Science, pages 445-461. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-31784-3_26.
  4. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  5. Julien Bernet, David Janin, and Igor Walukiewicz. Permissive strategies: from parity games to safety games. RAIRO Theor. Informatics Appl., 36(3):261-275, 2002. URL: https://doi.org/10.1051/ita:2002013.
  6. Dietmar Berwanger. Admissibility in infinite games. In Wolfgang Thomas and Pascal Weil, editors, STACS 2007, 24th Annual Symposium on Theoretical Aspects of Computer Science, Aachen, Germany, February 22-24, 2007, Proceedings, volume 4393 of Lecture Notes in Computer Science, pages 188-199. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-70918-3_17.
  7. Roderick Bloem, Krishnendu Chatterjee, and Barbara Jobstmann. Graph games and reactive synthesis. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 921-962. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_27.
  8. Patricia Bouyer, Romain Brenguier, Nicolas Markey, and Michael Ummels. Pure Nash equilibria in concurrent deterministic games. Log. Methods Comput. Sci., 11(2), 2015. URL: https://doi.org/10.2168/LMCS-11(2:9)2015.
  9. Patricia Bouyer, Marie Duflot, Nicolas Markey, and Gabriel Renault. Measuring permissivity in finite games. In Mario Bravetti and Gianluigi Zavattaro, editors, CONCUR 2009 - Concurrency Theory, 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009. Proceedings, volume 5710 of Lecture Notes in Computer Science, pages 196-210. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04081-8_14.
  10. Patricia Bouyer, Erwin Fang, and Nicolas Markey. Permissive strategies in timed automata and games. Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 72, 2015. URL: https://doi.org/10.14279/tuj.eceasst.72.1015.
  11. 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: https://doi.org/10.1007/978-3-319-30000-9_1.
  12. Romain Brenguier and Jean-François Raskin. Pareto curves of multidimensional mean-payoff games. In Daniel Kroening and Corina S. Pasareanu, editors, Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II, volume 9207 of Lecture Notes in Computer Science, pages 251-267. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21668-3_15.
  13. Véronique Bruyère. Computer aided synthesis: A game-theoretic approach. In Émilie Charlier, Julien Leroy, and Michel Rigo, editors, Developments in Language Theory - 21st International Conference, DLT 2017, Liège, Belgium, August 7-11, 2017, Proceedings, volume 10396 of Lecture Notes in Computer Science, pages 3-35. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-62809-7_1.
  14. Véronique Bruyère. Synthesis of equilibria in infinite-duration games on graphs. ACM SIGLOG News, 8(2):4-29, 2021. URL: https://doi.org/10.1145/3467001.3467003.
  15. Véronique Bruyère, Baptiste Fievet, Jean-François Raskin, and Clément Tamines. Stackelberg-Pareto synthesis (extended version). CoRR, abs/2203.01285, 2022. URL: https://doi.org/10.48550/arXiv.2203.01285.
  16. Véronique Bruyère, Quentin Hautem, and Jean-François Raskin. On the complexity of heterogeneous multidimensional games. 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 11:1-11:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2016.11.
  17. Véronique Bruyère, Quentin Hautem, and Jean-François Raskin. Parameterized complexity of games with monotonically ordered omega-regular objectives. In Sven Schewe and Lijun Zhang, editors, 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, volume 118 of LIPIcs, pages 29:1-29:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.29.
  18. Véronique Bruyère, Jean-François Raskin, and Clément Tamines. Stackelberg-Pareto synthesis. In Serge Haddad and Daniele Varacca, editors, 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, volume 203 of LIPIcs, pages 27:1-27:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2021.27.
  19. Véronique Bruyère, Jean-François Raskin, and Clément Tamines. Pareto-rational verification. CoRR, abs/2202.13485, 2022. URL: http://arxiv.org/abs/2202.13485.
  20. Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. Generalized mean-payoff and energy games. In Kamal Lodaya and Meena Mahajan, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, December 15-18, 2010, Chennai, India, volume 8 of LIPIcs, pages 505-516. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2010.505.
  21. Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdzinski. Games with secure equilibria. Theor. Comput. Sci., 365(1-2):67-82, 2006. URL: https://doi.org/10.1016/j.tcs.2006.07.032.
  22. 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: https://doi.org/10.1007/978-3-540-71389-0_12.
  23. Krishnendu Chatterjee and Vishwanath Raman. Synthesizing protocols for digital contract signing. In Viktor Kuncak and Andrey Rybalchenko, editors, Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012. Proceedings, volume 7148 of Lecture Notes in Computer Science, pages 152-168. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-27940-9_11.
  24. Rodica Condurache, Emmanuel Filiot, Raffaella Gentilini, and Jean-François Raskin. The complexity of rational synthesis. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55 of LIPIcs, pages 121:1-121:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.ICALP.2016.121.
  25. Stephen A. Cook. The complexity of theorem-proving procedures. In Michael A. Harrison, Ranan B. Banerji, and Jeffrey D. Ullman, editors, Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, May 3-5, 1971, Shaker Heights, Ohio, USA, pages 151-158. ACM, 1971. URL: https://doi.org/10.1145/800157.805047.
  26. R.G. Downey and M.R. Fellows. Parameterized Complexity. Monographs in Computer Science. Springer New York, 2012. URL: https://books.google.be/books?id=HyTjBwAAQBAJ.
  27. E. Allen Emerson and Chin-Laung Lei. Modalities for model checking: Branching time logic strikes back. Sci. Comput. Program., 8(3):275-306, 1987. URL: https://doi.org/10.1016/0167-6423(87)90036-0.
  28. Javier Esparza, Jan Kretínský, Jean-François Raskin, and Salomon Sickert. From LTL and limit-deterministic Büchi automata to deterministic parity automata. In Axel Legay and Tiziana Margaria, editors, 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 I, volume 10205 of Lecture Notes in Computer Science, pages 426-442, 2017. URL: https://doi.org/10.1007/978-3-662-54577-5_25.
  29. Dana Fisman, Orna Kupferman, and Yoad Lustig. Rational synthesis. 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 190-204. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12002-2_16.
  30. 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. URL: https://doi.org/10.1007/3-540-36387-4.
  31. Erich Grädel and Michael Ummels. Solution Concepts and Algorithms for Infinite Multiplayer Games, pages 151-178. Amsterdam University Press, 2008. URL: http://www.jstor.org/stable/j.ctt46mwfz.11.
  32. Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, and Michael J. Wooldridge. Automated temporal equilibrium analysis: Verification and synthesis of multi-player games. Artif. Intell., 287:103353, 2020. URL: https://doi.org/10.1016/j.artint.2020.103353.
  33. Paul Hunter and Anuj Dawar. Complexity bounds for regular games. In Joanna Jedrzejowicz and Andrzej Szepietowski, editors, Mathematical Foundations of Computer Science 2005, 30th International Symposium, MFCS 2005, Gdansk, Poland, August 29 - September 2, 2005, Proceedings, volume 3618 of Lecture Notes in Computer Science, pages 495-506. Springer, 2005. URL: https://doi.org/10.1007/11549345_43.
  34. Richard M. Karp. Reducibility among combinatorial problems. In Raymond E. Miller and James W. Thatcher, editors, Proceedings of a symposium on the Complexity of Computer Computations, held March 20-22, 1972, at the IBM Thomas J. Watson Research Center, Yorktown Heights, New York, USA, The IBM Research Symposia Series, pages 85-103. Plenum Press, New York, 1972. URL: https://doi.org/10.1007/978-1-4684-2001-2_9.
  35. Steve Kremer and Jean-François Raskin. A game-based verification of non-repudiation and fair exchange protocols. J. Comput. Secur., 11(3):399-430, 2003. URL: http://content.iospress.com/articles/journal-of-computer-security/jcs185, URL: https://doi.org/10.3233/jcs-2003-11307.
  36. Orna Kupferman, Giuseppe Perelli, and Moshe Y. Vardi. Synthesis with rational environments. Ann. Math. Artif. Intell., 78(1):3-20, 2016. URL: https://doi.org/10.1007/s10472-016-9508-8.
  37. Orna Kupferman and Noam Shenwald. The complexity of LTL rational synthesis. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, volume 13243 of Lecture Notes in Computer Science, pages 25-45. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99524-9_2.
  38. Michael Luttenberger. Strategy iteration using non-deterministic strategies for solving parity games. CoRR, abs/0806.2923, 2008. URL: http://arxiv.org/abs/0806.2923.
  39. John F. Nash. Equilibrium points in n-person games. In PNAS, volume 36, pages 48-49. National Academy of Sciences, 1950. Google Scholar
  40. Christos H. Papadimitriou. Computational complexity. Addison-Wesley, 1994. Google Scholar
  41. Christos H. Papadimitriou and Mihalis Yannakakis. On the approximability of trade-offs and optimal access of web sources. In 41st Annual Symposium on Foundations of Computer Science, FOCS 2000, 12-14 November 2000, Redondo Beach, California, USA, pages 86-92. IEEE Computer Society, 2000. Google Scholar
  42. Nir Piterman. From nondeterministic Büchi and Streett automata to deterministic parity automata. Log. Methods Comput. Sci., 3(3), 2007. URL: https://doi.org/10.2168/LMCS-3(3:5)2007.
  43. Amir Pnueli and Roni Rosner. On the synthesis of a reactive module. In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989, pages 179-190. ACM Press, 1989. URL: https://doi.org/10.1145/75277.75293.
  44. Stéphane Riedweg and Sophie Pinchinat. You can always compute maximally permissive controllers under partial observation when they exist. In Proc. 2005 American Control Conference, Portland, Oregon, June 8-10 2005, volume 4, pages 2287-2292, Portland, Oregon, June 2005. Google Scholar
  45. Dorsa Sadigh, Shankar Sastry, Sanjit A. Seshia, and Anca D. Dragan. Planning for autonomous cars that leverage effects on human actions. In David Hsu, Nancy M. Amato, Spring Berman, and Sam Ade Jacobs, editors, Robotics: Science and Systems XII, University of Michigan, Ann Arbor, Michigan, USA, June 18 - June 22, 2016, 2016. URL: https://doi.org/10.15607/RSS.2016.XII.029.
  46. Reinhard Selten. Spieltheoretische Behandlung eines Oligopolmodells mit Nachfrageträgheit. Zeitschrift für die gesamte Staatswissenschaft, 121:301-324 and 667-689, 1965. Google Scholar
  47. A. Prasad Sistla and Edmund M. Clarke. The complexity of propositional linear temporal logics. J. ACM, 32(3):733-749, 1985. URL: https://doi.org/10.1145/3828.3837.
  48. A. Prasad Sistla, Moshe Y. Vardi, and Pierre Wolper. The complementation problem for Büchi automata with appplications to temporal logic. Theor. Comput. Sci., 49:217-237, 1987. URL: https://doi.org/10.1016/0304-3975(87)90008-9.
  49. Yaron Velner, Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Alexander Moshe Rabinovich, and Jean-François Raskin. The complexity of multi-mean-payoff and multi-energy games. Inf. Comput., 241:177-196, 2015. URL: https://doi.org/10.1016/j.ic.2015.03.001.
  50. Yaron Velner and Alexander Rabinovich. Church synthesis problem for noisy input. In Martin Hofmann, editor, Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, volume 6604 of Lecture Notes in Computer Science, pages 275-289. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-19805-2_19.
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