Abstract
This paper is a study of Brihaye et al.’s ATL with strategy contexts. We focus on memory-less strategies and establish that the resulting logic is undecidable. An immediate corollary follows that the problem of satisfiability checking of every variant of ATL with strategy context introduced by Brihaye et al. is undecidable. We also relate ATL\(_{\textit{sc}}\) with memory-less strategies with ATL with explicit strategies, providing a decidable fragment.
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.
References
Ågotnes, T., Goranko, V., Jamroga, W.: Alternating-time temporal logics with irrevocable strategies. In: Proceedings of TARK 2007, pp. 15–24. ACM (2007)
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. The Journal of the ACM 49(5), 672–713 (2002)
Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. In: Perspectives Mathematical Logic. Springer (1997)
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 (2008)
Broersen, J., Herzig, A., Troquard, N.: A STIT-Extension of ATL. In: Fisher, M., van der Hoek, W., Konev, B., Lisitsa, A. (eds.) JELIA 2006. LNCS (LNAI), vol. 4160, pp. 69–81. Springer, Heidelberg (2006)
Da Costa, A., Laroussinie, F., Markey, N.: ATL with strategy contexts: Expressiveness and model checking. In: Proceedings of FSTTCS 2010. LIPIcs, vol. 8, pp. 120–132. Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik (2010)
Gabbay, D., Kurucz, A., Wolter, F., Zakharyaschev, M.: Many-dimensional modal logics: theory and applications. Studies in Logic, vol. 148. Elsevier Science (2003)
Gurevich, Y., Lewis, H.R.: The word problem for cancellation semigroups with zero. The Journal of Symbolic Logic 49(1), 184–191 (1984)
Halmos, P.: Algebraic logic, IV. Transactions of the AMS 86, 1–27 (1957)
Herzig, A., Schwarzentruber, F.: Properties of logics of individual and group agency. In: Proceedings of AiML 2008, pp. 133–149. College Publications (2008)
Horty, J.F.: Agency and Deontic Logic. Oxford University Press, Oxford (2001)
Johnson, J.: Nonfinitizability of classes of representable polyadic algebras. The Journal of Symbolic Logic 34(3), 344–352 (1969)
Kurucz, A.: S5 x S5 x S5 lacks the finite model property. In: Proceedings of AiML 2002, pp. 321–327. World Scientific (2002)
Laroussinie, F., Markey, N., Oreiby, G.: On the expressiveness and complexity of ATL. Logical Methods in Computer Science 4(2) (2008)
Maddux, R.: The equational theory of CA3 is undecidable. The Journal of Symbolic Logic 45(2), 311–316 (1980)
Marx, M.: Complexity of products of modal logics. Journal of Logic and Computation 9(2), 197–214 (1999)
Mortimer, M.: On languages with two variables. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 21, 135–140 (1975)
Troquard, N., Walther, D.: ATL with contexts: agency and explicit strategies. In: Proceedings of LAMAS@AAMAS 2012 (2012)
Walther, D., van der Hoek, W., Wooldridge, M.: Alternating-time temporal logic with explicit strategies. In: Proceedings of TARK 2007, pp. 269–278. ACM (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Troquard, N., Walther, D. (2012). On Satisfiability in ATL with Strategy Contexts. In: del Cerro, L.F., Herzig, A., Mengin, J. (eds) Logics in Artificial Intelligence. JELIA 2012. Lecture Notes in Computer Science(), vol 7519. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33353-8_31
Download citation
DOI: https://doi.org/10.1007/978-3-642-33353-8_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33352-1
Online ISBN: 978-3-642-33353-8
eBook Packages: Computer ScienceComputer Science (R0)