Document Open Access Logo

Quantifying Bounds in Strategy Logic

Authors Nathanaël Fijalkow , Bastien Maubert , Aniello Murano, Sasha Rubin

PDF
Thumbnail PDF

File

LIPIcs.CSL.2018.23.pdf
  • Filesize: 0.62 MB
  • 23 pages

Document Identifiers

Author Details

Nathanaël Fijalkow
  • CNRS, LaBRI, Bordeaux, France, Alan Turing Institute of data science, London, United Kingdom
Bastien Maubert
  • University of Naples "Federico II", Naples, Italy
Aniello Murano
  • University of Naples "Federico II", Naples, Italy
Sasha Rubin
  • University of Naples "Federico II", Naples, Italy

Funding

  • Fijalkow, Nathanaël: This project has received funding from the Alan Turing Institute under EPSRC grant EP/N510129/1 and the DeLTA project (ANR-16-CE40-0007).
  • Maubert, Bastien: This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 709188.

Cite As Get BibTex

Nathanaël Fijalkow, Bastien Maubert, Aniello Murano, and Sasha Rubin. Quantifying Bounds in Strategy Logic. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 23:1-23:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CSL.2018.23

Abstract

Program synthesis constructs programs from specifications in an automated way. Strategy Logic (SL) is a powerful and versatile specification language whose goal is to give theoretical foundations for program synthesis in a multi-agent setting. One limitation of Strategy Logic is that it is purely qualitative. For instance it cannot specify quantitative properties of executions such as "every request is quickly granted", or quantitative properties of trees such as "most executions of the system terminate". In this work, we extend Strategy Logic to include quantitative aspects in a way that can express bounds on "how quickly" and "how many". We define Prompt Strategy Logic, which encompasses Prompt LTL (itself an extension of LTL with a prompt eventuality temporal operator), and we define Bounded-Outcome Strategy Logic which has a bounded quantifier on paths. We supply a general technique, based on the study of automata with counters, that solves the model-checking problems for both these logics.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Prompt LTL
  • Strategy Logic
  • Model checking
  • Automata with counters

Metrics

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

References

  1. Shaull Almagor, Yoram Hirshfeld, and Orna Kupferman. Promptness in ω-regular automata. In ATVA, LNCS 6252, pages 22-36. Springer, 2010. Google Scholar
  2. Rajeev Alur, Kousha Etessami, Salvatore La Torre, and Doron Peled. Parametric temporal logic for “model measuring”. ACM Transactions on Computational Logic, 2(3):388-407, 2001. Google Scholar
  3. Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. Journal of the ACM, 49(5):672-713, 2002. URL: http://dx.doi.org/10.1145/585265.585270.
  4. Benjamin Aminof, Aniello Murano, Sasha Rubin, and Florian Zuleger. Prompt alternating-time epistemic logics. In KR, pages 258-267. AAAI Press, 2016. URL: http://www.aaai.org/ocs/index.php/KR/KR16/paper/view/12890.
  5. Mordechai Ben-Ari, Zohar Manna, and Amir Pnueli. The temporal logic of branching time. In POPL, pages 164-176, 1981. URL: http://dx.doi.org/10.1145/567532.567551.
  6. Raphaël Berthon, Bastien Maubert, and Aniello Murano. Decidability results for ATL* with imperfect information and perfect recall. In AAMAS, 2017. Google Scholar
  7. Raphaël Berthon, Bastien Maubert, Aniello Murano, Sasha Rubin, and Moshe Y. Vardi. Strategy logic with imperfect information. In LICS, 2017. Google Scholar
  8. Alessandro Bianco, Fabio Mogavero, and Aniello Murano. Graded computation tree logic. ACM Transactions on Computational Logic, 13(3):25:1-25:53, 2012. URL: http://dx.doi.org/10.1145/2287718.2287725.
  9. Patricia Bouyer, Patrick Gardy, and Nicolas Markey. Weighted strategy logic with boolean goals over one-counter games. In FSTTCS 2015, pages 69-83, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2015.69.
  10. Arnaud Carayol and Olivier Serre. How good is a strategy in a game with nature? In LICS, pages 609-620. IEEE Computer Society, 2015. Google Scholar
  11. Krishnendu Chatterjee and Nathanaël Fijalkow. Infinite-state games with finitary conditions. In CSL, pages 181-196, 2013. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2013.181.
  12. Krishnendu Chatterjee, Thomas A Henzinger, and Florian Horn. Finitary winning in ω-regular games. ACM Transactions on Computational Logic, 11(1):1, 2009. Google Scholar
  13. Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Strategy Logic. Information and Computation, 208(6):677-693, 2010. URL: http://dx.doi.org/10.1016/j.ic.2009.07.004.
  14. Thomas Colcombet. The theory of stabilisation monoids and regular cost functions. In ICALP, 2009. Google Scholar
  15. Thomas Colcombet. Fonctions régulières de coût. Habilitation Thesis, 2013. Google Scholar
  16. Thomas Colcombet. Regular cost functions, part I: logic and algebra over words. Logical Methods in Computer Science, 9(3), 2013. Google Scholar
  17. Thomas Colcombet and Nathanaël Fijalkow. The bridge between regular cost functions and ω-regular languages. In ICALP, pages 126:1-126:13, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.ICALP.2016.126.
  18. Thomas Colcombet and Christof Löding. Regular cost functions over finite trees. In LICS, pages 70-79, 2010. URL: http://dx.doi.org/10.1109/LICS.2010.36.
  19. E. Allen Emerson and Joseph Y. Halpern. "Sometimes" and "Not Never" revisited: On branching versus linear time. In POPL, pages 127-140, 1983. URL: http://dx.doi.org/10.1145/567067.567081.
  20. Nathanaël Fijalkow, Florian Horn, Denis Kuperberg, and Michał Skrzypczak. Trading bounds for memory in games with counters. In ICALP, pages 197-208, 2015. URL: http://dx.doi.org/10.1007/978-3-662-47666-6_16.
  21. Nathanaël Fijalkow and Martin Zimmermann. Cost-Parity and Cost-Street Games. In FSTTCS, volume LIPIcs 18, pages 124-135, 2012. Google Scholar
  22. Nathanaël Fijalkow and Martin Zimmermann. Parity and Streett games with costs. Logical Methods in Computer Science, 10(2), 2014. URL: http://dx.doi.org/10.2168/LMCS-10(2:14)2014.
  23. Tim French. Decidability of quantifed propositional branching time logics. In AJCAI'01, pages 165-176, 2001. URL: http://dx.doi.org/10.1007/3-540-45656-2_15.
  24. Patrick Gardy. Semantics of Strategy Logic. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, 2017. URL: https://tel.archives-ouvertes.fr/tel-01561802.
  25. Thomas A. Henzinger and Nir Piterman. Solving games without determinization. In CSL, pages 395-410, 2006. Google Scholar
  26. Sophia Knight and Bastien Maubert. Dealing with imperfect information in strategy logic. In SR, 2015. Google Scholar
  27. Denis Kuperberg. Linear temporal logic for regular cost functions. Logical Methods in Computer Science, 10(1), 2014. Google Scholar
  28. Denis Kuperberg and Michael Vanden Boom. On the expressive power of cost logics over infinite words. In ICALP, pages 287-298, 2012. Google Scholar
  29. Orna Kupferman. Augmenting branching temporal logics with existential quantification over atomic propositions. JLC, 9(2):135-147, 1999. URL: http://dx.doi.org/10.1093/logcom/9.2.135.
  30. Orna Kupferman, P. Madhusudan, P. S. Thiagarajan, and Moshe Y. Vardi. Open systems in reactive environments: Control and synthesis. In CONCUR, LNCS 1877, pages 92-107. Springer, 2000. Google Scholar
  31. Orna Kupferman, Giuseppe Perelli, and Moshe Y. Vardi. Synthesis with rational environments. Annals of Mathematics and Artificial Intelligence, 78(1):3-20, 2016. URL: http://dx.doi.org/10.1007/s10472-016-9508-8.
  32. Orna Kupferman, Nir Piterman, and Moshe Y Vardi. From liveness to promptness. Formal Methods in System Design, 34(2):83-103, 2009. Google Scholar
  33. Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2):312-360, 2000. URL: http://dx.doi.org/10.1145/333979.333987.
  34. François Laroussinie and Nicolas Markey. Quantified CTL: expressiveness and complexity. LMCS, 10(4), 2014. URL: http://dx.doi.org/10.2168/LMCS-10(4:17)2014.
  35. François Laroussinie and Nicolas Markey. Augmenting ATL with strategy contexts. Information and Computation, 245:98-123, 2015. Google Scholar
  36. Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Y. Vardi. Reasoning about strategies: On the model-checking problem. ACM Transactions on Computational Logic, 15(4):34:1-34:47, 2014. URL: http://dx.doi.org/10.1145/2631917.
  37. Fabio Mogavero, Aniello Murano, and Loredana Sorrentino. On promptness in parity games. Fundamenta Informaticae, 139(3):277-305, 2015. Google Scholar
  38. Amir Pnueli. The temporal logic of programs. In FOCS, pages 46-57, 1977. URL: http://dx.doi.org/10.1109/SFCS.1977.32.
  39. Amir Pnueli and Roni Rosner. On the synthesis of a reactive module. In POPL, pages 179-190, 1989. Google Scholar
  40. A Prasad Sistla. Theoretical Issues in the Design and Certification of Distributed Systems. PhD thesis, Harvard University, Cambridge, MA, USA, 1983. Google Scholar
  41. Martin Zimmermann. Optimal bounds in parametric LTL games. Theoretical Computer Science, 493:30-45, 2013. URL: http://dx.doi.org/10.1016/j.tcs.2012.07.039.
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