Document Open Access Logo

Dependences in Strategy Logic

Authors Patrick Gardy, Patricia Bouyer, Nicolas Markey

PDF
Thumbnail PDF

File

LIPIcs.STACS.2018.34.pdf
  • Filesize: 0.6 MB
  • 15 pages

Document Identifiers

Author Details

Patrick Gardy
Patricia Bouyer
Nicolas Markey

Cite AsGet BibTex

Patrick Gardy, Patricia Bouyer, and Nicolas Markey. Dependences in Strategy Logic. In 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 96, pp. 34:1-34:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.STACS.2018.34

Abstract

Strategy Logic (SL) is a very expressive temporal logic for specifying and verifying properties of multi-agent systems: in SL, one can quantify over strategies, assign them to agents, and express LTL properties of the resulting plays. Such a powerful framework has two drawbacks: First, model checking SL has non-elementary complexity; second, the exact semantics of SL is rather intricate, and may not correspond to what is expected. In this paper, we focus on strategy dependences in SL, by tracking how existentially-quantified strategies in a formula may (or may not) depend on other strategies selected in the formula, revisiting the approach of [Mogavero et al., Reasoning about strategies: On the model-checking problem, 2014]. We explain why elementary dependences, as defined by Mogavero et al., do not exactly capture the intended concept of behavioral strategies. We address this discrepancy by introducing timeline dependences, and exhibit a large fragment of SL for which model checking can be performed in 2-EXPTIME under this new semantics.
Keywords
  • strategic reasoning
  • strategy logic
  • dependences
  • behavioural strategies.

Metrics

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

References

  1. Thomas Ågotnes, Valentin Goranko, and Wojciech Jamroga. Alternating-time temporal logics with irrevocable strategies. In Dov Samet, editor, Proceedings of the 11th Conference on Theoretical Aspects of Rationality and Knowledge (TARK'07), pages 15-24, 2007. Google Scholar
  2. Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672-713, 2002. URL: http://dx.doi.org/10.1145/585265.585270.
  3. Patricia Bouyer, Patrick Gardy, and Nicolas Markey. Weighted strategy logic with boolean goals over one-counter games. In Prahladh Harsha and G. Ramalingam, editors, 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2015, December 16-18, 2015, Bangalore, India, volume 45 of LIPIcs, pages 69-83. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2015.69.
  4. Patricia Bouyer, Patrick Gardy, and Nicolas Markey. On the semantics of strategy logic. Inf. Process. Lett., 116(2):75-79, 2016. URL: http://dx.doi.org/10.1016/j.ipl.2015.10.004.
  5. Romain Brenguier, Jean-François Raskin, and Ocan Sankur. Assume-admissible synthesis. Acta Inf., 54(1):41-83, 2017. URL: http://dx.doi.org/10.1007/s00236-016-0273-2.
  6. Thomas Brihaye, Arnaud Da Costa Lopes, François Laroussinie, and Nicolas Markey. ATL with strategy contexts and bounded memory. In Sergei N. Artëmov and Anil Nerode, editors, Logical Foundations of Computer Science, International Symposium, LFCS 2009, Deerfield Beach, FL, USA, January 3-6, 2009. Proceedings, volume 5407 of Lecture Notes in Computer Science, pages 92-106. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-540-92687-0_7.
  7. Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Strategy logic. In Luís Caires and Vasco Thudichum Vasconcelos, editors, CONCUR 2007 - Concurrency Theory, 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3-8, 2007, Proceedings, volume 4703 of Lecture Notes in Computer Science, pages 59-73. Springer, 2007. URL: http://dx.doi.org/10.1007/978-3-540-74407-8_5.
  8. Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Dexter Kozen, editor, Logics of Programs, Workshop, Yorktown Heights, New York, May 1981, volume 131 of Lecture Notes in Computer Science, pages 52-71. Springer, 1981. URL: http://dx.doi.org/10.1007/BFb0025774.
  9. Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model checking. MIT Press, 2000. Google Scholar
  10. 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 fuer Informatik, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.ICALP.2016.121.
  11. E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus and determinacy (extended abstract). In 32nd Annual Symposium on Foundations of Computer Science, San Juan, Puerto Rico, 1-4 October 1991, pages 368-377. IEEE Computer Society, 1991. URL: http://dx.doi.org/10.1109/SFCS.1991.185392.
  12. 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: http://dx.doi.org/10.1007/978-3-642-12002-2_16.
  13. Valentin Goranko and Govert van Drimmelen. Complete axiomatization and decidability of alternating-time temporal logic. Theoretical Computer Science, 353(1-3):93-117, mar 2006. Google Scholar
  14. Orna Kupferman, Giuseppe Perelli, and Moshe Y. Vardi. Synthesis with rational environments. Ann. Math. Artif. Intell., 78(1):3-20, 2016. URL: http://dx.doi.org/10.1007/s10472-016-9508-8.
  15. François Laroussinie and Nicolas Markey. Augmenting ATL with strategy contexts. Inf. Comput., 245:98-123, 2015. URL: http://dx.doi.org/10.1016/j.ic.2014.12.020.
  16. François Laroussinie, Nicolas Markey, and Ghassan Oreiby. On the expressiveness and complexity of ATL. Logical Methods in Computer Science, 4(2), 2008. URL: http://dx.doi.org/10.2168/LMCS-4(2:7)2008.
  17. Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Y. Vardi. What makes ATL^* decidable? A decidable fragment of strategy logic. In Maciej Koutny and Irek Ulidowski, editors, Proceedings of the 23rd International Conference on Concurrency Theory (CONCUR'12), volume 7454 of Lecture Notes in Computer Science, pages 193-208. Springer-Verlag, sep 2012. Google Scholar
  18. Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Y. Vardi. Reasoning about strategies: On the model-checking problem. ACM Trans. Comput. Log., 15(4):34:1-34:47, 2014. URL: http://dx.doi.org/10.1145/2631917.
  19. Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Y. Vardi. Reasoning about strategies: on the satisfiability problem. Logical Methods in Computer Science, 13(1), 2017. URL: http://dx.doi.org/10.23638/LMCS-13(1:9)2017.
  20. Fabio Mogavero, Aniello Murano, and Luigi Sauro. On the boundary of behavioral strategies. In Proceedings of the 28th Annual Symposium on Logic in Computer Science (LICS'13), pages 263-272. IEEE Comp. Soc. Press, jun 2013. Google Scholar
  21. Fabio Mogavero, Aniello Murano, and Luigi Sauro. A behavioral hierarchy of strategy logic. In Nils Bulling, Leendert W. N. van der Torre, Serena Villata, Wojtek Jamroga, and Wamberto Weber Vasconcelos, editors, Computational Logic in Multi-Agent Systems - 15th International Workshop, CLIMA XV, Prague, Czech Republic, August 18-19, 2014. Proceedings, volume 8624 of Lecture Notes in Computer Science, pages 148-165. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-09764-0_10.
  22. Fabio Mogavero, Aniello Murano, and Moshe Y. Vardi. Reasoning about strategies. 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 133-144. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2010. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2010.133.
  23. Andrzej Mostowski. Games with forbidden positions. Research Report 78, University of Danzig, 1991. Google Scholar
  24. Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pages 46-57. IEEE Computer Society, 1977. URL: http://dx.doi.org/10.1109/SFCS.1977.32.
  25. Jean-Pierre Queille and Joseph Sifakis. Specification and verification of concurrent systems in CESAR. In Mariangiola Dezani-Ciancaglini and Ugo Montanari, editors, International Symposium on Programming, 5th Colloquium, Torino, Italy, April 6-8, 1982, Proceedings, volume 137 of Lecture Notes in Computer Science, pages 337-351. Springer, 1982. URL: http://dx.doi.org/10.1007/3-540-11494-7_22.
  26. Farn Wang, Chung-Hao Huang, and Fang Yu. A temporal logic for the interaction of strategies. In Joost-Pieter Katoen and Barbara König, editors, Proceedings of the 22nd International Conference on Concurrency Theory (CONCUR'11), volume 6901 of Lecture Notes in Computer Science, pages 466-481. Springer-Verlag, sep 2011. 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