主讲教师：Thomas Ågotnes (国家级讲座教授)
ZOOM 课程平台链接：
https://uib.zoom.us/j/65737290589?pwd=MFRBZHpXNU12RkdRbGdnZ3UyTnd3Zz09
ABSTRACT 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 coalition 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: [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 basic temporal logic including CTL, and CL and ATL, I will discuss extensions with a particular focus on adding epistemic and/or other additional modalities, as well as alternative interpretations of the coalition modalities.
Lecture 1 and 2(10.22 19:20-21:20, 10.25 14:00-16:00)
Linear-time Temporal Logic (LTL) and Computational Tree Logic (CTL). This lecture will be about temporal logic - logic for reasoning about time. I will introduce and compare Linear-time Temporal Logic (LTL) and 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. We will use CTL in many of the following lectures.
Reference
- Huth and Ryan, Logic in Computer Science. 2nd edition. Cambridge University Press, 2004. Chapter 3.
Lecture 3(11.03 19:20-21:20)
Normative systems and Reasoning about Norm Compliance. We get our first taste of coalition modalities by combining them with CTL in order to reason about so-called normative systems. Here, [C]phi is interpreted as "if we can trust coalition C", then phi will be true.
References
- Thomas Ågotnes, Wiebe van der Hoek, Juan A. Rodriguez-Aguilar, Carles Sierra, and Michael Wooldridge. Multi-modal CTL: Completeness, complexity and an application. Studia Logica, 92(1):1–26, 2009.
- Thomas Ågotnes, Wiebe van der Hoek, and Michael Wooldridge. Robust normative systems and a logic of norm compliance. Logic Journal of the Interest Group in Pure and Applied Logics (IGPL), 18(1):4–30, 2010.
Lecture 4(11.11 19:20-21:20)
Coalition Logic. Game semantics, neighbourhood semantics, representation theorem, axiomatisation.
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.
Lecture 5(11.18 19:20-21:20)
Alternating-time Temporal Logic (ATL). We introduce the ATL framework, which is obtained by combining CTL and 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.
- 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 6 and 7(11.22 19:20-21:20, 11.25 19:20-21:20)
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.
- 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.
- Thomas Ågotnes and Natasha Alechina. Coalition logic with individual, distributed and common knowledge. Journal of Logic and Computation, 2016.
Lecture 8(12.02 19:20-21:20)
Announcements as ability. We take a look at special cases of ability under imperfect information: ability to make some (typically epistemic) formula true by making an informative announcement. Here coalition modalities correspond to quantifying over the possible announcements the coalition can make.
References
- Thomas Ågotnes, Philippe Balbiani, Hans van Ditmarsch, and Pablo Seban. Group announcement logic. Journal of Applied Logic, 8(1):62–81, 2010.
- T. Ågotnes, H. Ditmarsch, and T. French. The undecidability of quantified announcements. Studia Logica, 104(4):597–640, 2016.
- French, T., Galimullin, R., van Ditmarsch, H., and Alechina, N. (2019). Groups versus coalitions: on the relative expressivity of GAL and CAL. In Agmon, N., Taylor, M. E., Elkind, E., and Veloso M., editors, Proceedings of AAMAS 2019, pages 953–961.
- Thomas Ågotnes, Natasha Alechina, and Rustam Galimullin. Logics with group announcements and distributed knowledge: Completeness and expressive power. Journal of Logic, Language and Information, 2021.
- Rustam Galimullin and Thomas Ågotnes. Quantified announcements and common knowledge. In Proceedings of the 20th International Conference on Autonomous Agents and MultiA- gent Systems, AAMAS ’21, page 528–536, Richland, SC, 2021. International Foundation for Autonomous Agents and Multiagent Systems.
