课程名称：

Reasoning about time and coalitional ability

主讲教师：

Prof. Thomas Ågotnes

内容摘要：

In recent years there has been a great interest in modal logics capturing the strategic abilities of coalitions, with Pauly's Coalition Logic (CL) and Alur et al.'s Alternating-time Temporal Logic (ALT) being the most popular frameworks. Typically, these logics have a modality [C] for each group of agents C, with [C]phi meaning that C have the ability to make phi true. There is a close connection to game theory: alternatively [C]phi can be interpreted as C having a winning strategy for phi. ATL is an extension of the popular temporal logic Computational Tree Logic (CTL) with coalition modalities. In addition to introducing the basic frameworks of CTL, CL and ATL, I will discuss extensions with a particular focus on adding epistemic and/or other additional modalities.

预计课程安排及参考文献：
The following is a tentative schedule and some pointers to some papers. It is not necessary to read the references to attend the seminar. Since I don't know the backgrounds of the students so well, I would like to set the pace as we go along, and I also encourage as much discussion as possible, so we might not stick very closely to the schedule.

2020.11.11 09:40-12:10（星期三）
* Lecture 1: Computational Tree Logic (CTL). This lecture will be about temporal logic - logic for reasoning about time. I will introduce and discuss Computational Tree Logic (CTL). CTL is a discrete, branching-time logic. It is one of the most well-known temporal logics, and one of the most used logics in computer science where it is used for formal specification and verification of computer systems.

* Lecture 2: Coalition Logic.: Game semantics, neighbourhood semantics, representation theorem, axiomatisation. We also discuss an extension allowing quantification over coalitions.

 References:
  - Thomas Ågotnes. Coalition Logic. In Encyclopedia of Philosophy and the Social Sciences, 2013.
  - M. Pauly. A modal logic for coalitional power in games. Journal of Logic and Computation, 12(1):149–166, 2002.
  - V. Goranko, W. Jamroga, and P. Turrini. Strategic games and truly playable effectivity functions. In Proceedings of AAMAS 2011, pages 727–734, 2011.
  - Thomas Ågotnes, Wiebe van der Hoek, and Michael Wooldridge. Quantified coalition logic. Synthese, 165(2):269–294, 2008.

2020.11.18 09:40-12:10（星期三）
* Lecture 3: ATL. We introduce the ATL framework, which is obtained by adding temporal CTL-operators to CL. We discuss the role of memory in strategic reasoning,  revocability of strategic decisions, bisimulation, axiomatisation.

 References:
  - R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time Temporal Logic. Journal of the ACM, 49:672–713, 2002. [Only for reference - hard to read!]
  - V. Goranko and G. van Drimmelen. Complete axiomatization and decidability of alternating-time temporal logic. Theoretical Computer Science, 353(1):93–117, 2006. [Only for reference - hard to read!]
- Thomas Ågotnes, Valentin Goranko, and Wojciech Jamroga. Alternating-time temporal logics with irrevocable strategies. In Dov Samet, editor,  Proceedings of the 11th Conference on Theoretical Aspects of Rationality and Knowledge (TARK XI), pages 15--24, Brussels, Belgium, June 2007. Presses Universitaires de  Louvain.

* Lecture 4: CL/ATL and imperfect information. We extend CL and ATL with epistemic modalities. It turns out that a straightforward combination of the semantics of the two types of operators give the notion of ability some counter-intuitive properties. We discuss possible solutions, and possible variants of "ability" under  imperfect information.

 References:
  - Thomas Ågotnes, Valentin Goranko, Wojciech Jamroga, and Michael Wooldridge. Knowledge and ability. In Hans van Ditmarsch, Joseph Y. Halpern, Wiebe van der Hoek, and Barteld Kooi, editors, Handbook of Epistemic Logic, pages 543–589. College Publications, 2015.
   - Thomas Ågotnes and Natasha Alechina. Coalition logic with individual, distributed and common knowledge. Journal of Logic and Computation, 2016.
  - W. van der Hoek and M. Wooldridge. Cooperation, knowledge and time: Alternating-time Temporal Epistemic Logic and its applications. Studia Logica, 75(1):125–157, 2003.
  - Thomas Ågotnes. Action and knowledge in alternating-time temporal logic. Synthese, 149(2):377–409, 2006.
  - P. Y. Schobbens. Alternating-time logic with imperfect recall. Electronic Notes in Theoretical Computer Science, 85(2), 2004.
  - Wojciech Jamroga and Thomas Ågotnes. Constructive knowledge: what agents can achieve under imperfect information. Journal of Applied Non-Classical Logics, 17(4):423--475, 2007.