Abstract
Temporal logics are a well investigated formalism for the specification, verification, and synthesis of reactive systems. Within this family, alternating temporal logic, Atl *, has been introduced as a useful generalization of classical linear- and branching-time temporal logics by allowing temporal operators to be indexed by coalitions of agents. Classically, temporal logics are memoryless: once a path in the computation tree is quantified at a given node, the computation that has led to that node is forgotten. Recently, mCtl * has been defined as a memoryful variant of Ctl *, where path quantification is memoryful. In the context of multi-agent planning, memoryful quantification enables agents to “relent” and change their goals and strategies depending on their past history. In this paper, we define mAtl *, a memoryful extension of Atl *, in which a formula is satisfied at a certain node of a path by taking into account both the future and the past. We study the expressive power of mAtl *, its succinctness, as well as related decision problems. We also investigate the relationship between memoryful quantification and past modalities and show their equivalence. We show that both the memoryful and the past extensions come without any computational price; indeed, we prove that both the satisfiability and the model-checking problems are 2ExpTime-Complete, as they are for Atl *.
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
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-Time Temporal Logic. JACM 49(5), 672–713 (2002)
Daniele, M., Traverso, P., Vardi, M.Y.: Strong Cyclic Planning Revisited. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS, vol. 1809, pp. 35–48. Springer, Heidelberg (2000)
Emerson, E.A., Halpern, J.Y.: “Sometimes” and “Not Never” Revisited: On Branching Versus Linear Time. JACM 33(1), 151–178 (1986)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge (1995)
Gabbay, D.M.: The Declarative Past and Imperative Future: Executable Temporal Logic for Interactive Systems. In: Banieqbal, B., Pnueli, A., Barringer, H. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 409–448. Springer, Heidelberg (1989)
Jamroga, W.: Strategic Planning Through Model Checking of ATL Formulae. In: Rutkowski, L., Siekmann, J.H., Tadeusiewicz, R., Zadeh, L.A. (eds.) ICAISC 2004. LNCS (LNAI), vol. 3070, pp. 879–884. Springer, Heidelberg (2004)
Janin, D., Walukiewicz, I.: Automata for the Modal μ-Calculus and Related Results. In: Hájek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol. 969, pp. 552–562. Springer, Heidelberg (1995)
Kupferman, O., Pnueli, A.: Once and For All. In: LICS 1995, pp. 25–35. IEEE Computer Society, Los Alamitos (1995)
Kupferman, O., Vardi, M.Y.: Memoryful Branching-Time Logic. In: LICS 2006, pp. 265–274. IEEE Computer Society, Los Alamitos (2006)
Kupferman, O., Vardi, M.Y., Wolper, P.: An Automata Theoretic Approach to Branching-Time Model Checking. JACM 47(2), 312–360 (2000)
Laroussinie, F., Markey, N., Schnoebelen, P.: Temporal Logic with Forgettable Past. In: LICS 2002, pp. 383–392. IEEE Computer Society, Los Alamitos (2002)
Lichtenstein, O., Pnueli, A., Zuck, L.D.: The Glory of the Past. In: LP 1985, pp. 196–218 (1985)
Muller, D.E., Schupp, P.E.: Alternating Automata on Infinite Trees. TCS 54(2-3), 267–276 (1987)
Muller, D.E., Schupp, P.E.: Simulating Alternating Tree Automata by Nondeterministic Automata: New Results and New Proofs of Theorems of Rabin, McNaughton and Safra. TCS 141, 69–107 (1995)
Niebert, P., Peled, D., Pnueli, A.: Discriminative Model Checking. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 504–516. Springer, Heidelberg (2008)
Osborne, M.J., Rubinstein, A.: A course in game theory. MIT Press, Cambridge (1994)
Pistore, M., Vardi, M.Y.: The Planning Spectrum - One, Two, Three, Infinity. In: JAIR 2007, vol. 30, pp. 101–132 (2007)
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)
Schewe, S., Finkbeiner, B.: Satisfiability and Finite Model Property for the Alternating-Time μ-Calculus. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 591–605. Springer, Heidelberg (2006)
Vardi, M.Y.: A Temporal Fixpoint Calculus. In: POPL 1988, pp. 250–259 (1988)
van der Hoek, W., Wooldridge, M.: Tractable multiagent planning for epistemic goals. In: AAMAS 2002, pp. 1167–1174 (2002)
Vardi, M.Y., Wolper, P.: Automata-Theoretic Techniques for Modal Logics of Programs. JCSS 32(2), 183–221 (1986)
Woolridge, M.J.: Introduction to Multiagent Systems. John Wiley & Sons, Chichester (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mogavero, F., Murano, A., Vardi, M.Y. (2010). Relentful Strategic Reasoning in Alternating-Time Temporal Logic. In: Clarke, E.M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2010. Lecture Notes in Computer Science(), vol 6355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17511-4_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-17511-4_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17510-7
Online ISBN: 978-3-642-17511-4
eBook Packages: Computer ScienceComputer Science (R0)