[agents] PhD thesis proposal: "Find the gap between the existing strategic logics for the verification process" - LTCI - Télécom Paris

[Vadim Malvone]

PhD thesis proposal on Computer Science / Artificial Intelligence

*Find the gap between the existing strategic logics for the verification 
process*

Game theory in AI is a powerful mathematical framework to reason about 
reactive systems. The latter are characterized by an ongoing interaction 
between two or more entities, called players, and the behaviour of the 
entire system deeply relies on this interaction. Game theory has been 
largely investigated in a number of different fields such as: economics, 
biology, and computer science.

An important application of game theory in computer science and, more 
recently, in AI, concerns formal-system verification. In particular, 
game theory has become a powerful tool for the verification of reactive 
systems and embedded systems. This story of success goes back to the 
late seventies with the introduction of the model checking technique 
[1]. The idea of model checking is powerful and simple at the same time. 
In fact, to check whether a system satisfies a desired behaviour we 
check instead whether a mathematical model of the system meets a formal 
specification. For the latter, temporal logics, such as LTL and CTL, are 
usually used.

Notably, first applications of model checking just concerned closed 
systems, which are characterized by the fact that their behaviour is 
completely determined by their internal states. Unfortunately, all model 
checking techniques developed to handle closed systems turn out to be 
quite useless in practice as most of the systems are open in the sense 
that they are characterized by an ongoing interaction with other 
systems. To overcome this problem, model checking has been extended to 
multi-agent systems. Breakthrough contributions along this direction 
concern the introduction of logics for the strategic reasoning such as 
Alternating-time Temporal Logic (ATL) [2], Strategy Logic (SL) [3], and 
their extensions. ATL is obtained as a generalization of CTL, in which 
the existential E and the universal A path quantifiers are replaced with 
strategic modalities of the form <A> and [A], where A is a set of 
agents. On the other hand, SL is an extension of LTL and treats 
strategies as first-order objects that can be determined by means of the 
existential Ex and universal Ax quantifiers, which can be respectively 
read as "there exists a strategy x" and "for all strategies x".

However, ATL and SL suffer from two main problems in two different 
sides. ATL has a polynomial model checking complexity but it cannot 
express several solution concepts such as the Nash Equilibrium. The 
strong limitation of ATL is that it threats strategies only implicitly 
in the semantics of its modalities. So, it is weak in expressivity. On 
the other hand, SL is the more powerful logic for the strategic 
reasoning but its model checking problem is non-elementary. So, the full 
logic can not have practical applications.

The aim of this thesis project is divided in two macro steps:

    1. Define a new logic for the strategic reasoning that can
    incorporate the positive features of ATL in terms of complexity and
    the good features of SL in terms of expressivity. Therefore, a
    thorough study of the semantics of these logics is required to find
    the right compromise.

    2. Develop a model checking tool that can solve the verification
    problem for the new logic proposed.

[1] Model Checking, Edmund M. Clarke, Jr., Orna Grumberg and Doron A. 
Peled, MIT Press, 1999.

[2] R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-Time Temporal 
Logic. JACM, 49(5):672–713, 2002.

[3] F. Mogavero, A. Murano, G. Perelli, and M. Y. Vardi. Reasoning About 
Strategies: On the Model-Checking Problem. TOCL, 15(4):34:1--34:47, 2014.

*Profile and skills required*

- Master degree in computer science, mathematics, or related fields
- Strong computer science and/or mathematical background (with 
particular attention on Formal Methods and Logics)
- Good programming skills
- Good level in written and spoken English

*How to apply*

If you are interested you can apply by sending the following documents 
to vadim.malvone at telecom-paris.fr:

- Curriculum vitae
- Motivation letter
- List of publications (if available)
- List of courses taken during the studies (with assessments)

Deadline for application submission: March 31, 2022.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cs.umbc.edu/pipermail/agents/attachments/20220217/97f7d34d/attachment.html>