Nils Bulling
Skip Abstract Section
Abstract
In alternating-time temporal logic ATL*, agents with perfect recall assign choices to sequences of states, i.e., to possible finite histories of the game. However, when a nested strategic modality is interpreted, the new strategy does not take into account the previous sequence of events. It is as if agents collect their observations in the nested game again from scratch, thus, effectively forgetting what they observed before. Intuitively, it does not fit the assumption of agents having perfect recall of the past. In this article, we investigate the alternative semantics for ATL* where the past is not forgotten in nested games. We show that the standard semantics of ATL* coincides with the “truly perfect recall” semantics for agents with perfect information and in case of so-called “objective” abilities under uncertainty. On the other hand, the two semantics differ significantly for the most popular (“subjective”) notion of ability under imperfect information. The same applies to the standard vs. “truly perfect recall” semantics of ATL* with persistent strategies. We compare the relevant variants of ATL* by looking at their expressive power, sets of validities, and tractability of model checking.
- T. Ågotnes. 2006. Action and knowledge in alternating-time temporal logic. Synthese 149, 2 (2006), 377--409.Google Scholar
Cross Ref
- T. Ågotnes, V. Goranko, and W. Jamroga. 2007. Alternating-time temporal logics with irrevocable strategies. In Proceedings of TARK XI. ACM, 15--24. Google ScholarDigital Library
- T. Ågotnes, V. Goranko, W. Jamroga, and M. Wooldridge. 2015. Knowledge and ability. In Handbook of Epistemic Logic, H. P. van Ditmarsch, J. Y. Halpern, W. van der Hoek, and B. P. Kooi (Eds.). College Publications, 543--589.Google Scholar
- T. Ågotnes and D. Walther. 2009. A logic of strategic ability under bounded memory. Journal of Logic, Language and Information 18, 1 (2009), 55--77. Google ScholarDigital Library
- N. Alechina, B. Logan, N. H. Nga, and A. Rakib. 2009. Verifying properties of coalitional ability under resource bounds. In Proceedings of the Logics for Agents and Mobility (LAM’09). Muller, Berndt. Durham University.Google Scholar
- N. Alechina, B. Logan, H. N. Nguyen, and F. Raimondi. 2017. Model-checking for resource-bounded ATL with production and consumption of resources. J. Comput. System Sci. 88 (2017), 126--144.Google ScholarCross Ref
- N. Alechina, B. Logan, H. N. Nguyen, and A. Rakib. 2010. Resource-bounded alternating-time temporal logic. In Proceedings of International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS’10). International Foundation for Autonomous Agents and Multiagent Systems, 481--488. Google ScholarDigital Library
- N. Alechina, B. Logan, H. N. Nguyen, and A. Rakib. 2011. Logic for coalitions with bounded resources. Journal of Logic and Computation 21, 6 (2011), 907--937. Google ScholarDigital Library
- N. Alechina, B. Logan, and M. Whitsey. 2004. A complete and decidable logic for resource-bounded agents. In Proceedings of International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS’04). IEEE Computer Society, 606--613. Google ScholarDigital Library
- R. Alur, L. de Alfaro, R. Grossu, T. A. Henzinger, M. Kang, C. M. Kirsch, R. Majumdar, F. Y. C. Mang, and B.-Y. Wang. 2001. jMocha: A model-checking tool that exploits design structure. In Proceedings of International Conference on Software Engineering (ICSE’01). IEEE Computer Society Press, 835--836. Google ScholarDigital Library
- R. Alur, L. de Alfaro, T. A. Henzinger, S. C. Krishnan, F. Y. C. Mang, S. Qadeer, S. K. Rajamani, and S. Tasiran. 2000. MOCHA: Modularity in Model Checking. Technical Report. University of Berkeley.Google Scholar
- R. Alur, T. A. Henzinger, and O. Kupferman. 1997. Alternating-time temporal logic. In Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS’97). IEEE Computer Society Press, 100--109. Google ScholarDigital Library
- R. Alur, T. A. Henzinger, and O. Kupferman. 2002. Alternating-time temporal logic. J. ACM 49 (2002), 672--713. Google ScholarDigital Library
- Francesco Belardinelli. 2014. Reasoning about knowledge and strategies: Epistemic strategy logic. In Proceedings of the 2nd International Workshop on Strategic Reasoning (SR’14), Grenoble, France, April 5-6, 2014.27--33.Google ScholarCross Ref
- F. Belardinelli, A. Lomuscio, A. Murano, and S. Rubin. 2017. Verification of multi-agent systems with imperfect information and public actions. In Proceedings of AAMAS. International Foundation for Autonomous Agents and Multiagent Systems, 1268--1276. Google ScholarDigital Library
- N. Belnap and M. Perloff. 1988. Seeing to it that: A canonical form for agentives. Theoria 54 (1988), 175--199.Google ScholarCross Ref
- R. Berthon, B. Maubert, A. Murano, S. Rubin, and M. Y. Vardi. 2017. Strategy logic with imperfect information. In Proceedings of LICS. IEEE, 1--12.Google Scholar
- D. Berwanger and L. Kaiser. 2010. Information tracking in games on graphs. Journal of Logic, Language and Information 19, 4 (2010), 395--412. Google ScholarDigital Library
- D. Berwanger, L. Kaiser, and B. Puchala. 2011. A perfect-information construction for coordination in games. In Proceedings of FSTTCS. LIPiCS, Leibniz-Zentrum für Informatik, 387--398.Google Scholar
- D. Berwanger and A. B. Mathew. 2014. Infinite games with finite knowledge gaps. CoRR abs/1411.5820 (2014). http://arxiv.org/abs/1411.5820 Google ScholarDigital Library
- D. Berwanger, A. B. Mathew, and M. van den Bogaard. 2015. Hierarchical information patterns and distributed strategy synthesis. In Proceedings of ATVA, Lecture Notes in Computer Science, Vol. 9364. Springer, Berlin, 378--393.Google Scholar
- T. Brihaye, A. Da Costa Lopes, F. Laroussinie, and N. Markey. 2009. ATL with strategy contexts and bounded memory. In Proceedings of LFCS, Lecture Notes in Computer Science, Vol. 5407. Springer, Berlin, 92--106. Google ScholarDigital Library
- N. Bulling and J. Dix. 2010. Modelling and verifying coalitions using argumentation and ATL. Inteligencia Artificial 14, 46 (March 2010), 45--73.Google ScholarCross Ref
- N. Bulling and B. Farwer. 2010. Expressing properties of resource-bounded systems: The logics RTL<sup>*</sup> and RTL. In Proceedings of Computational Logic in Multi-Agent Systems (CLIMA’10), Lecture Notes in Computer Science, Vol. 6214. Springer, Berlin, 22--45. Google ScholarDigital Library
- N. Bulling and B. Farwer. 2010. On the (un-)decidability of model checking resource-bounded agents. In Proceedings of ECAI (Frontiers in Artificial Intelligence and Applications), Vol. 215. IOS Press, 567--572. Google ScholarDigital Library
- N. Bulling and W. Jamroga. 2014. Comparing variants of strategic ability: How uncertainty and memory influence general properties of games. Journal of Autonomous Agents and Multi-Agent Systems 28, 3 (2014), 474--518. Google ScholarDigital Library
- N. Bulling, W. Jamroga, and J. Dix. 2008. Reasoning about temporal properties of rational play. Annals of Mathematics and Artificial Intelligence 53, 1–4 (2008), 51--114. Google ScholarDigital Library
- N. Bulling, W. Jamroga, and M. Popovici. 2013. Agents with truly perfect recall in alternating-time temporal logic (extended abstract). In Proceedings of AAMAS’13. International Foundation for Autonomous Agents and Multiagent Systems, 1561--1562. Google ScholarDigital Library
- N. Bulling, W. Jamroga, and M. Popovici. 2014. Agents with truly perfect recall: Expressivity and validities. In Proceedings of ECAI’14. IOS Press, 177--182. Google ScholarDigital Library
- S. Busard. 2017. Symbolic Model Checking of Multi-Modal Logics: Uniform Strategies and Rich Explanations. Ph.D. Dissertation. Universite Catholique de Louvain.Google Scholar
- S. Busard, C. Pecheur, H. Qu, and F. Raimondi. 2014. Improving the model checking of strategies under partial observability and fairness constraints. In Formal Methods and Software Engineering. Lecture Notes in Computer Science, Vol. 8829. Springer, Berlin, 27--42.Google Scholar
- S. Busard, C. Pecheur, H. Qu, and F. Raimondi. 2015. Reasoning about memoryless strategies under partial observability and unconditional fairness constraints. Information and Computation 242 (2015), 128--156. Google ScholarDigital Library
- K. Chatterjee, L. Doyen, T. A. Henzinger, and J.-F. Raskin. 2007. Algorithms for omega-regular games of incomplete information. Logical Methods in Computer Science 3, 3 (2007).Google Scholar
- K. Chatterjee, T.A. Henzinger, and N. Piterman. 2010. Strategy logic. Information and Computation 208, 6 (2010), 677--693. Google ScholarDigital Library
- B. F. Chellas. 1969. The Logical Form of Imperatives. Ph.D. Dissertation. Stanford University.Google Scholar
- T. Chen, V. Forejt, M. Kwiatkowska, D. Parker, and A. Simaitis. 2013. PRISM-games: A model checker for stochastic multi-player games. In Proceedings of Tools and Algorithms for Construction and Analysis of Systems (TACAS’13), Lecture Notes in Computer Science, Vol. 7795. Springer, Berlin, 185--191. Google ScholarDigital Library
- E. M. Clarke and B.-H. Schlingloff. 2001. Model checking. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov (Eds.). Elsevier, 1635--1790. Google ScholarDigital Library
- R. Diaconu and C. Dima. 2012. Model-checking alternating-time temporal logic with strategies based on common knowledge is undecidable. Applied Artificial Intelligence 26, 4 (2012), 331--348. Google ScholarDigital Library
- C. Dima, C. Enea, and D. P. Guelev. 2010. Model-checking an alternating-time temporal logic with knowledge, imperfect information, perfect recall and communicating coalitions. In Proceedings of Games, Automata, Logics and Formal Verification (GandALF’10). 103--117.Google Scholar
- C. Dima and F. L. Tiplea. 2011. Model-checking ATL under imperfect information and perfect recall semantics is undecidable. CoRR abs/1102.4225 (2011).Google Scholar
- E. A. Emerson and J. Y. Halpern. 1986. “Sometimes” and “Not Never” revisited: On branching versus linear time temporal logic. J. ACM 33, 1 (1986), 151--178. Google ScholarDigital Library
- R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. 1995. Reasoning about Knowledge. MIT Press, Cambridge, MA. Google ScholarDigital Library
- D. P. Guelev and C. Dima. 2008. Model-checking strategic ability and knowledge of the past of communicating coalitions. In Proceedings of DALT. 75--90.Google Scholar
- D. P. Guelev and C. Dima. 2012. Epistemic ATL with perfect recall, past and strategy contexts. In Proceedings of Computational Logic in Multi-Agent Systems (CLIMA’12), Lecture Notes in Computer Science, Vol. 7486. Springer, Berlin, 77--93.Google Scholar
- D. P. Guelev, C. Dima, and C. Enea. 2011. An alternating-time temporal logic with knowledge, perfect recall and past: Axiomatisation and model-checking. Journal of Applied Non-Classical Logics 21, 1 (2011), 93--131.Google ScholarCross Ref
- P. Hawke. 2010. Coordination, almost perfect information and strategic ability. In Proceedings of LAMAS. Kluwer Academic Publishers.Google Scholar
- X. Huang and R. van der Meyden. 2014. Symbolic model checking epistemic strategy logic. In Proceedings of AAAI Conference on Artificial Intelligence. AAAI Press, 1426--1432. Google ScholarDigital Library
- W. Jamroga and T. Ågotnes. 2007. Constructive knowledge: What agents can achieve under incomplete information. Journal of Applied Non-Classical Logics 17, 4 (2007), 423--475.Google ScholarCross Ref
- W. Jamroga, M. Knapik, and D. Kurpiewski. 2017. Fixpoint approximation of strategic abilities under imperfect information. In Proceedings of the 16th International Conference on Autonomous Agents and Multiagent Systems (AAMAS’17). IFAAMAS, 1241--1249. Google ScholarDigital Library
- W. Jamroga, W. Penczek, P. Dembiński, and A. Mazurkiewicz. 2018. Towards partial order reductions for strategic ability. In Proceedings of the 17th International Conference on Autonomous Agents and Multiagent Systems (AAMAS’18). International Foundation for Autonomous Agents and Multiagent Systems. To appear. Google ScholarDigital Library
- W. Jamroga and W. van der Hoek. 2004. Agents that know how to play. Fundamenta Informaticae 63, 2--3 (2004), 185--219. Google ScholarDigital Library
- W. Jamroga, W. van der Hoek, and M. Wooldridge. 2005. Intentions and strategies in game-like scenarios. In Progress in Artificial Intelligence: Proceedings of EPIA 2005, Carlos Bento, Amílcar Cardoso, and Gaël Dias (Eds.). Lecture Notes in Artificial Intelligence, Vol. 3808. Springer, Berlin, 512--523. Google ScholarDigital Library
- M. Kacprzak and W. Penczek. 2004. Unbounded model checking for alternating-time temporal logic. In Proceedings of International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS’04). IEEE Computer Society, 646--653. Google ScholarDigital Library
- P. Kaźmierczak, T. Ågotnes, and W. Jamroga. 2014. Multi-agency is coordination and (limited) communication. In Proceedings of PRIMA, Lecture Notes in Computer Science, Vol. 8861. Springer, Berlin, 91--106.Google Scholar
- A. Lomuscio, H. Qu, and F. Raimondi. 2015. MCMAS: An open-source model checker for the verification of multi-agent systems. International Journal on Software Tools for Technology Transfer (2015). Retrieved February 27, 2019 from Google ScholarDigital Library
- A. Lomuscio and F. Raimondi. 2006. MCMAS: A model checker for multi-agent systems. In Proceedings of Tools and Algorithms for Construction and Analysis of Systems (TACAS’06), Lecture Notes in Computer Science, Vol. 4314. Springer, Berlin, 450--454. Google ScholarDigital Library
- J. McCarthy and P. J. Hayes. 1969. Some philosophical problems from the standpoint of artificial intelligence. In Machine Intelligence 4, B. Meltzer and D. Michie (Eds.). Edinburgh University Press, 463--502.Google Scholar
- F. Mogavero, A. Murano, G. Perelli, and M. Y. Vardi. 2014. Reasoning about strategies: On the model-checking problem. ACM Transactions on Computational Logic 15, 4 (2014), 1--42. Google ScholarDigital Library
- F. Mogavero, A. Murano, and M. Y. Vardi. 2010. Reasoning about strategies. In Proceedings of FSTTCS. ACM, 133--144.Google Scholar
- F. Mogavero, A. Murano, and M. Y. Vardi. 2010. Relentful strategic reasoning in alternating-time temporal logic. In Proceedings of LPAR. Springer, 371--386. Google ScholarDigital Library
- R. C. Moore. 1985. A formal theory of knowledge and action. In Formal Theories of the Commonsense World, J. Hobbs and R. C. Moore (Eds.). Ablex Publishing Corp.Google Scholar
- R. C. Moore. 1977. Reasoning about knowledge and action. In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI’77). William Kaufmann, 223--227. Google ScholarDigital Library
- G. Peterson and J. Reif. 1979. Multiple-person alternation. In Proceedings of the 20th Annual Symposium on Foundations of Computer Science (FOCS’79). IEEE Computer Society Press, 348--363. Google ScholarDigital Library
- G. Peterson, J. Reif, and S. Azhar. 2001. Lower bounds for multiplayer noncooperative games of incomplete information. Computers and Mathematics with Applications 41, 7 (2001), 957--992.Google ScholarCross Ref
- J. Pilecki, M. A. Bednarczyk, and W. Jamroga. 2014. Synthesis and verification of uniform strategies for multi-agent systems. In Proceedings of CLIMA XV, Lecture Notes in Computer Science, Vol. 8624. Springer, Berlin, 166--182.Google Scholar
- A. Pnueli and R. Rosner. 1990. Distributed reactive systems are hard to synthesize. In Proceedings of the 31th Annual Symposium on Foundations of Computer Science (FOCS’90). IEEE Computer Society Press, 746--757. Google ScholarDigital Library
- G. Ryle. 1949. The Concept of Mind. Chicago University Press.Google Scholar
- P. Y. Schobbens. 2004. Alternating-time logic with imperfect recall. Electronic Notes in Theoretical Computer Science 85, 2 (2004), 82--93.Google ScholarCross Ref
- N. V. Shilov, N. O. Garanina, and K.-M. Choe. 2006. Update and abstraction in model checking of knowledge and branching time. Fundamenta Informaticae 72, 1-3 (2006), 347--361. Google ScholarDigital Library
- N. V. Shilov, N. O. Garanina, and N. A. Kalinina. 2004. Model checking knowledge, actions and fixpoints. In Proceedings of CS&P’’’04. Humboldt Universitat, 351--357.Google Scholar
- W. van der Hoek, W. Jamroga, and M. Wooldridge. 2005. A logic for strategic reasoning. In Proceedings of AAMAS’05. 157--164. Google ScholarDigital Library
- W. van der Hoek and M. Wooldridge. 2003. Cooperation, knowledge and time: Alternating-time temporal epistemic logic and its applications. Studia Logica 75, 1 (2003), 125--157.Google ScholarCross Ref
- R. van der Meyden and N. V. Shilov. 1999. Model checking knowledge and time in systems with perfect recall (extended abstract). In Proceedings of Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, Vol. 1738. Springer, Berlin, 432--445. Google ScholarDigital Library
- H. van Ditmarsch and S. Knight. 2014. Partial information and uniform strategies. In Proceedings of Computational Logic in Multi-Agent Systems (CLIMA’14), Lecture Notes in Computer Science. Springer, Berlin, 183--198.Google Scholar
- S. Vester. 2013. Alternating-time temporal logic with finite-memory strategies. In Proceedings of GandALF (EPTCS’13). 194--207.Google ScholarCross Ref
- D. Walther, W. van der Hoek, and M. Wooldridge. 2007. Alternating-time temporal logic with explicit strategies. In Proceedings of TARK XI. Presses Universitaires de Louvain, 269--278. Google ScholarDigital Library
Index Terms
- Reasoning about Strategic Abilities: Agents with Truly Perfect Recall
Recommendations
Completeness of Flat Coalgebraic Fixpoint Logics
Modal fixpoint logics traditionally play a central role in computer science, in particular in artificial intelligence and concurrency. The μ-calculus and its relatives are among the most expressive logics of this type. However, popular fixpoint logics ...
Refining strategic ability in alternating-time temporal logic
We propose extending Alternating-time Temporal Logic (ATL) by a unary operator i about distributing the powers of some given agent i to a given set of sub-agents . i means that i's powers can be distributed in a way which satisfies the ATL condition on ...
Comparing variants of strategic ability: how uncertainty and memory influence general properties of games
Alternating-time temporal logic (ATL) is a modal logic that allows to reason about agents' abilities in game-like scenarios. Semantic variants of ATL are usually built upon different assumptions about the kind of game that is played, including ...
Comments