nach oben

Theory of Computing Systems

Erschienen in:

08.01.2020

Dependences in Strategy Logic

verfasst von: Patrick Gardy, Patricia Bouyer, Nicolas Markey

Erschienen in: Theory of Computing Systems | Ausgabe 3/2020

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Vorheriger Artikel On Approximating the Stationary Distribution of Time-Reversible Markov Chains

Nächster Artikel Optimal Dislocation with Persistent Errors in Subquadratic Time

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

We name our fragment SL[EG]^♭ as it comes as a natural continuation after fragments SL[AG]^♭ [33], SL[BG]^♭ [30], and SL[CG]^♭ and SL[DG]^♭ [32].

Ågotnes, T., Goranko, V., Jamroga, W.: Alternating-time temporal logics with irrevocable strategies. In: Samet, D. (ed.) Proceedings of the 11th Conference on Theoretical Aspects of Rationality and Knowledge (TARK’07), pp. 15–24 (2007)

Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002). https://doi.org/10.1145/585265.585270 MathSciNetCrossRef

Aminof, B., Malvone, V., Murano, A., Rubin, S.: Graded modalities in strategy logic. Inf. Comput. 261(4), 634–649 (2018). https://doi.org/10.1016/j.ic.2018.02.021 MathSciNetCrossRef

Berthon, R., Maubert, B., Murano, A., Rubin, S., Vardi, M.Y.: Strategy logic with imperfect information. In: Proceedings of the 32th Annual Symposium on Logic in Computer Science (LICS’17), pp. 1–12. IEEE Comp. Soc. Press. https://doi.org/10.1109/LICS.2017.8005136 (2017)

Bouyer, P., Gardy, P., Markey, N.: Weighted strategy logic with boolean goals over one-counter games. In: Harsha, P., Ramalingam, G. (eds.) Proceedings of the 35th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’15), volume 45 of Leibniz International Proceedings in Informatics, Leibniz-Zentrum für Informatik . https://doi.org/10.4230/LIPIcs.FSTTCS.2015.69, pp 69–83 (2015)

Bouyer, P., Gardy, P., Markey, N.: On the semantics of strategy logic. Inf. Process. Lett. 116(2), 75–79 (2016). https://doi.org/10.1016/j.ipl.2015.10.004 MathSciNetCrossRef

Brenguier, R., Raskin, J.-F., Sankur, O.: Assume-admissible synthesis. Acta Inform. 54(1), 41–83 (2017). https://doi.org/10.1007/s00236-016-0273-2 MathSciNetCrossRef

Brihaye, T., Da Costa, A., Laroussinie, F., Markey, N.: ATL with strategy contexts and bounded memory. In: Artemov, S.N., Nerode, A. (eds.) Proceedings of the International Symposium Logical Foundations of Computer Science (LFCS’09), volume 5407 of Lecture Notes in Computer Science, pp 92–106. Springer (2009). https://doi.org/10.1007/978-3-540-92687-0_7

Čermák, P., Lomuscio, A., Mogavero, F., Murano, A.: MCMAS-SLK: A model checker for the verification of strategy logic specifications. In: Biere, A., Bloem, R. (eds.) Proceedings of the 26th International Conference on Computer Aided Verification (CAV’14), volume 8559 of Lecture Notes in Computer Science, pp 525–532. Springer (2014). https://doi.org/10.1007/978-3-319-08867-9_34

10.

Čermák, P., Lomuscio, A., Murano, A.: Verifying and synthesising multi-agent systems against one-goal strategy logic specifications. In: Bonet, B., Koenig, S. (eds.) Proceedings of the 29th AAAI Conference on Artificial Intelligence (AAAI’15), pp 2038–2044. AAAI Press (2015)

11.

Chatterjee, K., Henzinger, T.A., Piterman, N.: Strategy logic. In: Caires, L., Vasconcelos, V.T. (eds.) Proceedings of the 18th International Conference on Concurrency Theory (CONCUR’07), volume 4703 of Lecture Notes in Computer Science, pp 59–73. Springer (2007). https://doi.org/10.1007/978-3-540-74407-8_5

12.

Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D.C. (ed.) Proceedings of the 3rd Workshop on Logics of Programs (LOP’81), volume 131 of Lecture Notes in Computer Science, pp 52–71. Springer (1982). https://doi.org/10.1007/BFb0025774

13.

Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press, New York (2000)MATH

14.

Condurache, R., Filiot, E., Gentilini, R., Raskin, J.-F., Sangiorgi, D.: The complexity of rational synthesis. In: Chatzigiannakis, I., Mitzenmacher, M., Rabani, Y. (eds.) Proceedings of the 43rd International Colloquium on Automata, Languages and Programming (ICALP’16) – Part II, volume 55 of Leibniz International Proceedings in Informatics, pp 121:1–121:15. Leibniz-Zentrum Für Informatik (2016). https://doi.org/10.4230/LIPIcs.ICALP.2016.121

15.

Dima, C., Ţiplea, F.L.: Model-checking ATL under imperfect information and perfect recall semantics is undecidable. Research Report arXiv:http://arXiv.org/abs/1102.4225 (2011)

16.

Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: Proceedings of the 32nd Annual Symposium on Foundations of Computer Science (FOCS’91), pp. 368–377. IEEE Comp. Soc. Press. https://doi.org/10.1109/SFCS.1991.185392 (1991)

17.

Fijalkow, N., Maubert, B., Murano, A., Rubin, S.: Quantifying bounds in strategy logic. In: Ghica, D.R., Jung, A. (eds.) Proceedings of the 27th EACSL Annual Conference on Computer Science Logic (CSL’18), volume 119 of Leibniz International Proceedings in Informatics, pp 23:1–23:23. Leibniz-Zentrum Für Informatik (2018). https://doi.org/10.4230/LIPIcs.CSL.2018.23

18.

Fisman, D., Kupferman, O., Lustig, Y.: Rational synthesis. In: Esparza, J., Majumdar, R. (eds.) Proceedings of the 16th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS’10), volume 6015 of Lecture Notes in Computer Science, pp 190–204. Springer (2010). https://doi.org/10.1007/978-3-642-12002-2_16

19.

Gardy, P., Bouyer, P., Markey, N.: Dependences in strategy logic. In: Proceedings of the 35th Annual Symposium on Theoretical Aspects of Computer Science (STACS’18), volume 96 of Leibniz International Proceedings in Informatics, pp. 34:1–34:15. Leibniz-Zentrum Für Informatik (2018). https://doi.org/10.4230/LIPIcs.STACS.2018.34

20.

Goranko, V., van Drimmelen, G.: Complete axiomatization and decidability of alternating-time temporal logic. Theor. Comput. Sci. 353(1-3), 93–117 (2006)MathSciNetCrossRef

21.

Guelev, D.P., Dima, C.: Epistemic ATL with perfect recall, past and strategy contexts. In: Fisher, M., van der Torre, L.W.N., Dastani, M., Governatori, G. (eds.) Proceedings of the 13th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA’12), volume 7486 of Lecture Notes in Artificial Intelligence, pp 77–93. Springer (2012). https://doi.org/10.1007/978-3-642-32897-8_7

22.

Gutierrez, J., Harrenstein, P., Perelli, G., Wooldridge, M.: Nash equilibrium and bisimulation invariance. In: Meyer, R., Nestmann, U. (eds.) Proceedings of the 28th International Conference on Concurrency Theory (CONCUR’17), volume 85 of Leibniz International Proceedings in Informatics, pp 17:1–17:16. Leibniz-Zentrum Für Informatik (2017). https://doi.org/10.4230/LIPIcs.CONCUR.2017.17

23.

Henkin, L.: Some remarks on infinitely long formulas. In: Infinitistic Methods – Proceedings of the Symposium on Foundations of Mathematics, pp. 167–183. Pergamon Press (1961)

24.

Hintikka, J., Sandu, G.: Informational independence as a semantical phenomenon. In: Fenstad, J.E., Frolov, I.T., Hilppinen, R. (eds.) Proceedings of the 8th International Congress of Logic, Methodology and Philosophy of Science, volume 70 of Studies in Logic and the Foundations of Mathematics, pp 571–589, North-Holland (1989). https://doi.org/10.1016/S0049-237X(08)70066-1

25.

Huang, X., van der Meyden, R.: An epistemic strategy logic. ACM Trans. Comput. Log. 19(4), 26:1–26:45 (2018). https://doi.org/10.1145/3233769 MathSciNetCrossRef

26.

Kupferman, O., Perelli, G., Vardi, M.Y.: Synthesis with rational environments. Ann. Math. Artif. Intell. 78(1), 3–20 (2016). https://doi.org/10.1007/s10472-016-9508-8 MathSciNetCrossRef

27.

Laroussinie, F., Markey, N.: Augmenting ATL with strategy contexts. Inf. Comput. 245, 98–123 (2015). https://doi.org/10.1016/j.ic.2014.12.020 MathSciNetCrossRef

28.

Laroussinie, F., Markey, N., Oreiby, G.: On the expressiveness and complexity of ATL. Logical Methods in Computer Science 4(2:7), 1–25 (2008). https://doi.org/10.2168/LMCS-4(2:7)2008 MathSciNetCrossRefMATH

29.

Mogavero, F., Murano, A., Perelli, G., Vardi, M.Y.: What makes ATL^∗ decidable? A decidable fragment of strategy logic. In: Koutny, M., Ulidowski, I. (eds.) Proceedings of the 23rd International Conference on Concurrency Theory (CONCUR’12), volume 7454 of Lecture Notes in Computer Science, pp 193–208. Springer (2012)

30.

Mogavero, F., Murano, A., Perelli, G., Vardi, M.Y.: Reasoning about strategies: On the model-checking problem. ACM Trans. Comput. Log. 15(4), 34:1–34:47 (2014). https://doi.org/10.1145/2631917 MathSciNetCrossRef

31.

Mogavero, F., Murano, A., Perelli, G., Vardi, M.Y.: Reasoning about strategies: On the satisfiability problem. Logical Methods in Computer Science 13 (1:9), 1–37 (2017). https://doi.org/10.23638/LMCS-13(1:9)2017 MathSciNetCrossRefMATH

32.

Mogavero, F., Murano, A., Sauro, L.: 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 (2013)

33.

Mogavero, F., Murano, A., Sauro, L.: A behavioral hierarchy of strategy logic. In: Bulling, N., van der Torre, L.W.N., Villata, S., Jamroga, W., Vasconcelos, W.W. (eds.) Proceedings of the 15th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA’14), volume 8624 of Lecture Notes in Artificial Intelligence, pp 148–165. Springer (2014). https://doi.org/10.1007/978-3-319-09764-0_10

34.

Mogavero, F., Murano, A., Vardi, M.Y.: Reasoning about strategies. In: Lodaya, K., Mahajan, M. (eds.) Proceedings of the 30th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’10), volume 8 of Leibniz International Proceedings in Informatics, pp 133–144. Leibniz-Zentrum Für Informatik (2010). https://doi.org/10.4230/LIPIcs.FSTTCS.2010.133

35.

Mostowski, A.: Games with forbidden positions. Research report 78 university of Danzig (1991)

36.

Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS’77), pp. 46–57. IEEE Comp. Soc. Press. https://doi.org/10.1109/SFCS.1977.32 (1977)

37.

Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Proceedings of the 5th International Symposium on Programming (SOP’82), volume 137 of Lecture Notes in Computer Science, pp 337–351. Springer (1982). https://doi.org/10.1007/3-540-11494-7_22

38.

Väänänen, J.: Dependence Logic: A New Approach to Independence-Friendly Logic, volume 70 of London Mathematical Society Student Texts. Cambridge University Press, Cambridge (2007). https://doi.org/10.1017/CBO9780511611193

39.

Wang, F., Huang, C.-H., Yu, F.: A temporal logic for the interaction of strategies. In: Katoen, J.-P., König, B. (eds.) Proceedings of the 22nd International Conference on Concurrency Theory (CONCUR’11), volume 6901 of Lecture Notes in Computer Science, pp 466–481. Springer (2011)

Titel: Dependences in Strategy Logic
verfasst von: Patrick Gardy
Patricia Bouyer
Nicolas Markey
Publikationsdatum: 08.01.2020
Verlag: Springer US
Erschienen in: Theory of Computing Systems / Ausgabe 3/2020
Print ISSN: 1432-4350
Elektronische ISSN: 1433-0490
DOI: https://doi.org/10.1007/s00224-019-09926-y

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 3/2020

Optimal Dislocation with Persistent Errors in Subquadratic Time

On Approximating the Stationary Distribution of Time-Reversible Markov Chains

Computing Hitting Set Kernels By AC0-Circuits

Space-Efficient Algorithms for Longest Increasing Subsequence

Preface of the Special Issue on Theoretical Aspects of Computer Science (2018)

On the Tree Conjecture for the Network Creation Game