Abstract
Starting from the seminal work introducing Alternating Temporal Logic, formalisms for strategic reasoning have assumed a prominent role in multi-agent systems verification. Among the others, Strategy Logic (SL) allows to represent sophisticated solution concepts, by treating agent strategies as first-order objects.
A drawback from the high power of SL is to admit non-behavioral strategies: a choice of an agent, at a given point of a play, may depend on choices other agents can make in the future or in counterfactual plays. As the latter moves are unpredictable, such strategies cannot be easily implemented, making the use of the logic problematic in practice.
In this paper, we describe a hierarchy of SL fragments as syntactic restrictions of the recently defined Boolean-Goal Strategy Logic (SL[bg]). Specifically, we introduce Alternating-Goal Strategy Logic (SL[ag]) that, by imposing a suitable alternation over the nesting of the Boolean connectives in (SL[bg]), induces two dual chains of sets of formulas, the conjunctive and disjunctive ones. A formula belongs to the level i of the conjunctive chain if it just contains conjunctions of atomic goals together with a unique formula belonging to the disjunctive chain of level i − 1. The disjunctive chain is defined similarly. We formally prove that classic and behavioral semantics for (SL[ag]) coincide. Additionally, we study the related model-checking problem showing that it is 2ExpTime-complete.
Partially supported by the FP7 European Union project 600958-SHERPA, the Embedded System Cup Project B25B09090100007 (POR Campania FS 2007/2013, asse IV e asse V), and the OR.C.HE.S.T.R.A. MIUR PON project.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Ågotnes, T., Goranko, V., Jamroga, W.: Alternating-Time Temporal Logics with Irrevocable Strategies. In: TARK 2007, pp. 15–24 (2007)
Ågotnes, T., Walther, D.: A Logic of Strategic Ability Under Bounded Memory. JLLI 18(1), 55–77 (2009)
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-Time Temporal Logic. JACM 49(5), 672–713 (2002)
Brihaye, T., Da Costa, A., Laroussinie, F., Markey, N.: ATL with Strategy Contexts and Bounded Memory. In: Artemov, S., Nerode, A. (eds.) LFCS 2009. LNCS, vol. 5407, pp. 92–106. Springer, Heidelberg (2009)
Č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.) CAV 2014. LNCS, vol. 8559, pp. 525–532. Springer, Heidelberg (2014)
Chatterjee, K., Henzinger, T.A., Piterman, N.: Strategy Logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 59–73. Springer, Heidelberg (2007)
Chatterjee, K., Henzinger, T.A., Piterman, N.: Strategy Logic. IC 208(6), 677–693 (2010)
Emerson, E.A., Halpern, J.Y.: “Sometimes” and “Not Never” Revisited: On Branching Versus Linear Time. JACM 33(1), 151–178 (1986)
Finkbeiner, B., Schewe, S.: Coordination Logic. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 305–319. Springer, Heidelberg (2010)
Fisman, D., Kupferman, O., Lustig, Y.: Rational Synthesis. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 190–204. Springer, Heidelberg (2010)
Jamroga, W., Murano, A.: On Module Checking and Strategies. In: AAMAS 2014, pp. 701–708. International Foundation for Autonomous Agents and Multiagent Systems (2014)
Jamroga, W., Penczek, W.: Specification and Verification of Multi-Agent Systems. In: Bezhanishvili, N., Goranko, V. (eds.) ESSLLI 2010/2011. LNCS, vol. 7388, pp. 210–263. Springer, Heidelberg (2012)
Jamroga, W., van der Hoek, W.: Agents that Know How to Play. FI 63(2-3), 185–219 (2004)
Kupferman, O., Vardi, M.Y., Wolper, P.: Module Checking. IC 164(2), 322–344 (2001)
Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: A Model Checker for the Verification of Multi-Agent Systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 682–688. Springer, Heidelberg (2009)
Lomuscio, A., Raimondi, F.: mcmas: A Model Checker for Multi-agent Systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 450–454. Springer, Heidelberg (2006)
Lomuscio, A., Raimondi, F.: Model Checking Knowledge, Strategies, and Games in Multi-Agent Systems. In: AAMAS 2006, pp. 161–168. International Foundation for Autonomous Agents and Multiagent Systems (2006)
Lopes, A.D.C., Laroussinie, F., Markey, N.: ATL with Strategy Contexts: Expressiveness and Model Checking. In: FSTTCS 2010. LIPIcs, vol. 8, pp. 120–132. Leibniz-Zentrum fuer Informatik (2010)
Mogavero, F., Murano, A., Perelli, G., Vardi, M.Y.: Reasoning About Strategies: On the Model-Checking Problem. Technical report, arXiv (2011)
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.) CONCUR 2012. LNCS, vol. 7454, pp. 193–208. Springer, Heidelberg (2012)
Mogavero, F., Murano, A., Sauro, L.: On the Boundary of Behavioral Strategies. In: LICS 2013, pp. 263–272. IEEE Computer Society (2013)
Mogavero, F., Murano, A., Sauro, L.: Strategy Games: A Renewed Framework. In: AAMAS 2014, pp. 869–876. International Foundation for Autonomous Agents and Multiagent Systems (2014)
Mogavero, F., Murano, A., Vardi, M.Y.: Reasoning About Strategies. In: FSTTCS 2010. LIPIcs, vol. 8, pp. 133–144. Leibniz-Zentrum fuer Informatik (2010)
Mogavero, F., Murano, A., Vardi, M.Y.: Relentful Strategic Reasoning in Alternating-Time Temporal Logic. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16. LNCS (LNAI), vol. 6355, pp. 371–386. Springer, Heidelberg (2010)
Pinchinat, S.: A Generic Constructive Solution for Concurrent Games with Expressive Constraints on Strategies. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 253–267. Springer, Heidelberg (2007)
Pnueli, A.: The Temporal Logic of Programs. In: FOCS 1977, pp. 46–57. IEEE Computer Society (1977)
Sauro, L., Villata, S.: Dependency in Cooperative Boolean Games. JLC 23(2), 425–444 (2013)
Schewe, S.: ATL* Satisfiability is 2EXPTIME-Complete. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 373–385. Springer, Heidelberg (2008)
Schobbens, P.Y.: Alternating-Time Logic with Imperfect Recall 85(2), 82–93 (2004)
van der Hoek, W., Jamroga, W., Wooldridge, M.: A Logic for Strategic Reasoning. In: AAMAS 2005, pp. 157–164. Association for Computing Machinery (2005)
van der Hoek, W., Wooldridge, M.: Cooperation, Knowledge, and Time: Alternating-Time Temporal Epistemic Logic and its Applications. SL 75(1), 125–157 (2003)
Walther, D., van der Hoek, W., Wooldridge, M.: Alternating-Time Temporal Logic with Explicit Strategies. In: TARK 2007, pp. 269–278 (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Mogavero, F., Murano, A., Sauro, L. (2014). A Behavioral Hierarchy of Strategy Logic. In: Bulling, N., van der Torre, L., Villata, S., Jamroga, W., Vasconcelos, W. (eds) Computational Logic in Multi-Agent Systems. CLIMA 2014. Lecture Notes in Computer Science(), vol 8624. Springer, Cham. https://doi.org/10.1007/978-3-319-09764-0_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-09764-0_10
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-09763-3
Online ISBN: 978-3-319-09764-0
eBook Packages: Computer ScienceComputer Science (R0)