<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
<div class="moz-text-html" lang="x-unicode"> <span
style="font-size: 14.000000pt; font-family: 'Calibri';
font-style: italic" class="">PhD thesis proposal on Computer
Science / Artificial Intelligence </span>
<p><font size="+1"><b>Find the gap between the existing strategic
logics for the verification process</b></font></p>
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. <br>
<p> 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. <br>
<br>
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".<br>
<br>
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.<br>
<br>
The aim of this thesis project is divided in two macro steps:</p>
<blockquote>
<p>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.</p>
<p>2. Develop a model checking tool that can solve the
verification problem for the new logic proposed.</p>
</blockquote>
<p>[1] Model Checking, Edmund M. Clarke, Jr., Orna Grumberg and
Doron A. Peled, MIT Press, 1999.<br>
</p>
<p>[2] R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-Time
Temporal Logic. JACM, 49(5):672–713, 2002.<br>
</p>
<p>[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.</p>
<p><b>Profile and skills required</b></p>
<p>- Master degree in computer science, mathematics, or related
fields<br>
- Strong computer science and/or mathematical background (with
particular attention on Formal Methods and Logics)<br>
- Good programming skills<br>
- Good level in written and spoken English</p>
<p><b>How to apply</b><br>
</p>
If you are interested you can apply by sending the following
documents to <a class="moz-txt-link-abbreviated
moz-txt-link-freetext"
href="mailto:vadim.malvone@telecom-paris.fr">vadim.malvone@telecom-paris.fr</a>:</div>
<div class="moz-text-html" lang="x-unicode"><br>
</div>
<div class="moz-text-html" lang="x-unicode">- Curriculum vitae<br>
- Motivation letter<br>
- List of publications (if available)<br>
- List of courses taken during the studies (with assessments) </div>
<div class="moz-text-html" lang="x-unicode"><span style="font-size:
12.000000pt; font-family: 'TimesNewRomanPSMT'; color:
rgb(6.670000%, 33.300000%, 80.000000%)" class=""></span><span
style="font-size: 12.000000pt; font-family: 'TimesNewRomanPSMT';
color: rgb(6.670000%, 33.300000%, 80.000000%)" class=""></span>
<p class=""><span style="font-size: 12.000000pt; font-family:
'TimesNewRomanPSMT'; color: rgb(6.670000%, 33.300000%,
80.000000%)" class=""> </span><span style="font-size:
12.000000pt; font-family: 'TimesNewRomanPS'; font-weight: 700"
class="">Deadline for application submission</span><span
style="font-size: 12.000000pt; font-family:
'TimesNewRomanPSMT'" class="">: March 31, 2022. </span></p>
</div>
</body>
</html>