Top

ESSAI 2024 Course

Logic-based specification and

verification of multi-agent systems


Athens, July 15 - 19, 2024

Last update: July 15, 2024, 16.50 CEST
Mail to V.Goranko

ESSAI 2024

Lecturer: Valentin Goranko

Detailed course plan and schedule:

(Current version. Updates will be made frequently.)

Lecture 1

Date 15/07/2024

Main Topics

Introduction to the course.

Multi-agent transition systems and concurrent game models.

Formal specification of agents' strategic abilities using the alternating-time temporal logic ATL.

Using model checking of ATL formulae for strategy synthesis.

Recommended readings

M. Pauly, A Modal Logic for Coalitional Power in Games, Journal of Logic and Computation, Volume 12, Issue 1, 2002, pp. 149–166

R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-time temporal logic. Journal of the ACM 49:672-713, 2002.

Nils Bulling, Valentin Goranko, Wojciech Jamroga: Logics for reasoning about strategic abilities in multi-player games. In: Models of Strategic Reasoning: Logics, Games and Communities, Springer, LNCS/FoLLI series, vol. 8972, 2015, pp. 93--136.

Supplementary readings

V. Goranko and G. van Drimmelen: Decidability and Complete Axiomatization of the Alternating-time Temporal Logic, Theoretical Computer Science, Vol. 353, 1-3, (2006), pp. 93-117.

V. Goranko and D. Shkatov. Tableau-based decision procedures for logics of strategic ability in multi-agent systems. ACM Transactions of Computational Logic, vol. 11, No.1, 2010

S. Cerrito, A. David and V. Goranko. Optimal Tableaux Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-time Temoral Logic ATL+, ACM Transactions of Computational Logic, Vol. 17 Issue 1, October 2015, Article No. 4.

Slides on Lecture 1:

Slides on Lecture 1

Lecture 2

Date 16/07/2024

Main Topics

Strategic reasoning with incomplete and imperfect information: some variations of ATL.

Modeling and synthesis of memoryless and memory-based strategies.

Recommended readings

T. Ågotnes, V. Goranko, W. Jamroga, and M. Wooldridge: Knowledge and Ability, chapter in: Handbook of Epistemic Logic, College Publications, 2015, pp. 543–589.

W. van der Hoek and M.J.W. Wooldridge, Cooperation, Knowledge, and Time: Alternating- time Temporal Epistemic Logic and its Applications, Studia Logica,75:1, pp. 125 – 157, 2003.

Supplementary readings

T. Ågotnes and W. Jamroga, Constructive Knowledge: What Agents Can Achieve under Imperfect Information, Journal of Applied Non-Classical Logics, 17(4), pp. 423-475.

N. Bulling and W. Jamroga, Comparing variants of strategic ability: how uncertainty and memory influence general properties of games, Autonomous Agents and Multi-Agent Systems, 2014, Volume 28, pages 474-518.

Dilian Gurov, Valentin Goranko, Edvin Lundberg: Knowledge-Based Strategies for Multi-Agent Teams Playing Against Nature, Artificial Intelligence, Volume 309, August 2022, 103728

Slides on Lecture 2:

Slides on Lecture 2

Lecture 3

Date 17/07/2024

Main Topics

Some extensions of ATL. ATL with strategy contexts.

Temporal logic for coalitional goal assignments. Strategy logic.

Recommended readings

François Laroussinie and Nicolas Markey. Augmenting ATL with strategy contexts , Information and Computation, Volume 245, December 2015, Pages 98--123

Sebastian Enqvist and Valentin Goranko. The temporal logic of coalitional goal assignments in concurrent multi-player games , ACM Transactions of Computational Logic, Vol. 23, No. 4, Article 21, 2022.

Fabio Mogavero, Aniello Murano, Giuseppe Perelli, Moshe Y. Vardi. Reasoning about Strategies: on the Satisfiability Problem , Logical Methods in Computer Science Vol. 13(1:9), 2017, pp. 1–37

Supplementary readings

TBA

Slides on Lecture 3:

Slides on Lecture 3

Lecture 4

Date 18/07/2024

Main Topics

Formal framework and logics for combining quantitative and qualitative objectives in MAS.

Generalized dining philosophers games and formal verification and rational synthesis problems in them.

Applications to dynamic resource allocation.

Recommended readings

Nils Bulling and Valentin Goranko. Combining quantitative and qualitative reasoning in concurrent multi-player games , Journal of Autonomous Agents and Multiagent Systems, 2022, 36:2, 1--33.

Riccardo De Masellis, Valentin Goranko, Stefan Gruner, and Nils Timm. Generalising the Dining Philosophers Problem: Competitive Dynamic Resource Allocation in Multi-agent Systems in: Proceedings of the 16th European Conference in Multi-agent Systems (EUMAS2018), Springer LNCS vol.11450, 2019, pp. 30-47.

Supplementary readings

TBA

Slides on Lecture 4:

Slides on Lecture 4

Lecture 5

Date 19/07/2024

Main Topics

Modelling, formal specification, and algorithmic verification of homogeneous dynamic MAS.

Competitive dynamic resource management, modelled as multi-stage Colonel Blotto games.

Conclusion of the course.

Recommended readings

Riccardo De Masellis and Valentin Goranko. Logic-based Specification and Verification of Homogeneous Dynamic Multi-agent Systems, Journal of Autonomous Agents and Multiagent Systems , vol. 34 (2), 2020, article 34.

TBA

Supplementary readings

TBA

Slides on Lecture 5:

Slides on Lecture 5

Additional readings

TBA

Queries

Mail to V.Goranko