Document Open Access Logo

Plan Logic

Authors Dylan Bellier , Massimo Benerecetti , Fabio Mogavero , Sophie Pinchinat

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2024.9.pdf
  • Filesize: 0.79 MB
  • 18 pages

Document Identifiers

Author Details

Dylan Bellier
  • Univ Rennes, IRISA, CNRS, France
Massimo Benerecetti
  • Università degli Studi di Napoli Federico II, Italy
Fabio Mogavero
  • Università degli Studi di Napoli Federico II, Italy
Sophie Pinchinat
  • Univ Rennes, IRISA, CNRS, France

Cite As Get BibTex

Dylan Bellier, Massimo Benerecetti, Fabio Mogavero, and Sophie Pinchinat. Plan Logic. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.FSTTCS.2024.9

Abstract

When reasoning about games, one is often interested in verifying more intricate strategic properties than the mere existence of a winning strategy for a given coalition. Several languages, among which the very expressive Strategy Logic (SL), have been proposed that explicitly quantify over strategies in order to express and verify such properties. However, quantifying over strategies poses serious issues: not only does this lead to a non-elementary model-checking problem, but the classic Tarskian semantics is not fully adequate, both from a conceptual and practical viewpoint, since it does not guarantee the realisability of the strategies involved.
In this paper, we follow a different approach and introduce Plan Logic (PL), a logic that takes plans, i.e., sequences of actions, as first-class citizens instead of strategies. Since plans are much simpler objects than strategies, it becomes easier to enforce realisability. In this setting, we can recover strategic reasoning by means of a compositional hyperteams semantics, inspired by the well-known team semantics. We show that the Conjunctive-Goal and Disjunctive-Goal fragments of SL are captured by PL, with an effective polynomial translation. This result relies on the definition of a suitable game-theoretic semantics for the two fragments. We also investigate the model-checking problem for PL. For the full prenex fragment, the problem is shown to be fixed-parameter-tractable: it is polynomial in the size of the model, when the formula is fixed, and 2-ExpTimeC in the size of the formula. For the Conjunctive-Goal and Disjunctive-Goal fragments of PL this result can be improved to match the optimal polynomial complexity in the size of the model, regardless of the size of the formula.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Complexity theory and logic
Keywords
  • Logic for strategic reasoning
  • Strategy Logic
  • Realisable strategies
  • Strategies vs. plans
  • Hyperteam semantics

Metrics

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

References

  1. E. Acar, M. Benerecetti, and F. Mogavero. Satisfiability in Strategy Logic Can Be Easier than Model Checking. In AAAI'19, pages 2638-2645. AAAI Press, 2019. URL: https://doi.org/10.1609/AAAI.V33I01.33012638.
  2. R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-Time Temporal Logic. In FOCS'97, pages 100-109. IEEECS, 1997. Google Scholar
  3. R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-Time Temporal Logic. JACM, 49(5):672-713, 2002. URL: https://doi.org/10.1145/585265.585270.
  4. D. Bellier, M. Benerecetti, D. Della Monica, and F. Mogavero. Alternating (In)Dependence-Friendly Logic. APAL, 174(10):103315:1-58, 2023. Google Scholar
  5. D. Bellier, M. Benerecetti, D. Della Monica, and F. Mogavero. Good-for-Game QPTL: An Alternating Hodges Semantics. TOCL, 24(1):4:1-57, 2023. URL: https://doi.org/10.1145/3565365.
  6. P. Bouyer, P. Gardy, and N. Markey. Weighted Strategy Logic with Boolean Goals Over One-Counter Games. In FSTTCS'15, LIPIcs 45, pages 69-83. Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  7. K. Chatterjee, T.A. Henzinger, and N. Piterman. Strategy Logic. In CONCUR'07, LNCS 4703, pages 59-73. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74407-8_5.
  8. K. Chatterjee, T.A. Henzinger, and N. Piterman. Strategy Logic. IC, 208(6):677-693, 2010. URL: https://doi.org/10.1016/J.IC.2009.07.004.
  9. D. Dams. Flat Fragments of CTL and CTL*: Separating the Expressive and Distinguishing Powers. LJIGPL, 7(1):55-78, 1999. URL: https://doi.org/10.1093/JIGPAL/7.1.55.
  10. S. Enqvist and V. Goranko. The Temporal Logic of Coalitional Goal Assignments in Concurrent Multiplayer Games. TOCL, 23(4):21:1-58, 2022. URL: https://doi.org/10.1145/3517128.
  11. P. Gardy, P. Bouyer, and N. Markey. Dependences in Strategy Logic. In STACS'18, LIPIcs 96, pages 34:1-15. Leibniz-Zentrum fuer Informatik, 2018. Google Scholar
  12. P. Gardy, P. Bouyer, and N. Markey. Dependences in Strategy Logic. TCS, 64(3):467-507, 2020. URL: https://doi.org/10.1007/S00224-019-09926-Y.
  13. V. Goranko and S. Vester. Optimal Decision Procedures for Satisfiability in Fragments of Alternating-time Temporal Logics. In AIML'14, pages 234-253. College Publications, 2014. URL: http://www.aiml.net/volumes/volume10/Goranko-Vester.pdf.
  14. W. Hodges. Compositional Semantics for a Language of Imperfect Information. LJIGPL, 5(4):539-563, 1997. URL: https://doi.org/10.1093/JIGPAL/5.4.539.
  15. O. Kupferman, M.Y. Vardi, and P. Wolper. An Automata Theoretic Approach to Branching-Time Model Checking. JACM, 47(2):312-360, 2000. URL: https://doi.org/10.1145/333979.333987.
  16. F. Mogavero, A. Murano, G. Perelli, and M.Y. Vardi. Reasoning About Strategies: On the Model-Checking Problem. TOCL, 15(4):34:1-42, 2014. Google Scholar
  17. F. Mogavero, A. Murano, G. Perelli, and M.Y. Vardi. Reasoning About Strategies: On the Satisfiability Problem. LMCS, 13(1:9):1-37, 2017. Google Scholar
  18. F. Mogavero, A. Murano, and M.Y. Vardi. Reasoning About Strategies. In FSTTCS'10, LIPIcs 8, pages 133-144. Leibniz-Zentrum fuer Informatik, 2010. Google Scholar
  19. S. Schewe. ATL* Satisfiability is 2ExpTime-Complete. In ICALP'08, LNCS 5126, pages 373-385. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70583-3_31.
  20. J.A. Väänänen. Dependence Logic: A New Approach to Independence Friendly Logic, volume 70 of London Mathematical Society Student Texts. CUP, 2007. 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 About DROPS Imprint Privacy Contact