Supervisor

Suitable for

Abstract

Strategy Logic (SL) is a temporal logic to reason about strategies in multi-player games. Such games have multiple applications in Logic and Semantics, Artificial Intelligence and Multi-Agent Systems, and Verification and Computer Science. SL is a very powerful logic for strategic reasoning -- for instance, Nash equilibria and many other solution concepts in game theory can be easily expressed -- which has an undecidable satisfiability problem and a non-elementary model checking problem. In this project, the aim is to study fragments of SL which can potentially have better results (decidability and complexitity) with respect to the satisfiability and model checking problems. The fragments to be studied can be either syntactic fragments of the full language or semantic fragments where only particular classes of models are considered.

Prerequisites: Discrete Mathematics, Introduction to Formal Proof, Logic and Proof; Computer-Aided Formal Verification, Computational Complexity

Desirable: Automata, Logic and Games, Computational Game Theory.

Project type: theory