Relentful Strategic Reasoning in Alternating-Time Temporal Logic

  • Fabio Mogavero
  • Aniello Murano
  • Moshe Y. Vardi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6355)


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 *.


Model Check Temporal Logic Multiagent System Atomic Proposition State Formula 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [AHK02]
    Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-Time Temporal Logic. JACM 49(5), 672–713 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  2. DTV00.
    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)CrossRefGoogle Scholar
  3. EH86.
    Emerson, E.A., Halpern, J.Y.: “Sometimes” and “Not Never” Revisited: On Branching Versus Linear Time. JACM 33(1), 151–178 (1986)MathSciNetCrossRefzbMATHGoogle Scholar
  4. FHMV95.
    Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge (1995)zbMATHGoogle Scholar
  5. Gab87.
    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)CrossRefGoogle Scholar
  6. Jam04.
    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)CrossRefGoogle Scholar
  7. JW95.
    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)CrossRefGoogle Scholar
  8. KP95.
    Kupferman, O., Pnueli, A.: Once and For All. In: LICS 1995, pp. 25–35. IEEE Computer Society, Los Alamitos (1995)Google Scholar
  9. KV06.
    Kupferman, O., Vardi, M.Y.: Memoryful Branching-Time Logic. In: LICS 2006, pp. 265–274. IEEE Computer Society, Los Alamitos (2006)Google Scholar
  10. KVW00.
    Kupferman, O., Vardi, M.Y., Wolper, P.: An Automata Theoretic Approach to Branching-Time Model Checking. JACM 47(2), 312–360 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  11. LMS02.
    Laroussinie, F., Markey, N., Schnoebelen, P.: Temporal Logic with Forgettable Past. In: LICS 2002, pp. 383–392. IEEE Computer Society, Los Alamitos (2002)Google Scholar
  12. LPZ85.
    Lichtenstein, O., Pnueli, A., Zuck, L.D.: The Glory of the Past. In: LP 1985, pp. 196–218 (1985)Google Scholar
  13. MS87.
    Muller, D.E., Schupp, P.E.: Alternating Automata on Infinite Trees. TCS 54(2-3), 267–276 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  14. MS95.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  15. NPP08.
    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)CrossRefGoogle Scholar
  16. OR94.
    Osborne, M.J., Rubinstein, A.: A course in game theory. MIT Press, Cambridge (1994)zbMATHGoogle Scholar
  17. PV07.
    Pistore, M., Vardi, M.Y.: The Planning Spectrum - One, Two, Three, Infinity. In: JAIR 2007, vol. 30, pp. 101–132 (2007)Google Scholar
  18. Sch08.
    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)CrossRefGoogle Scholar
  19. SF06.
    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)CrossRefGoogle Scholar
  20. Var88.
    Vardi, M.Y.: A Temporal Fixpoint Calculus. In: POPL 1988, pp. 250–259 (1988)Google Scholar
  21. vdHWW02.
    van der Hoek, W., Wooldridge, M.: Tractable multiagent planning for epistemic goals. In: AAMAS 2002, pp. 1167–1174 (2002)Google Scholar
  22. VW86.
    Vardi, M.Y., Wolper, P.: Automata-Theoretic Techniques for Modal Logics of Programs. JCSS 32(2), 183–221 (1986)MathSciNetzbMATHGoogle Scholar
  23. WW01.
    Woolridge, M.J.: Introduction to Multiagent Systems. John Wiley & Sons, Chichester (2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Fabio Mogavero
    • 1
    • 2
  • Aniello Murano
    • 1
  • Moshe Y. Vardi
    • 2
  1. 1.Universitá degli Studi di Napoli ”Federico II”NapoliItaly
  2. 2.Department of Computer ScienceRice UniversityHoustonU.S.A.

Personalised recommendations