<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>An Integrated Tool for the Verification of
Multi-Agent Systems<br>
</b></font></p>
<p>The problem of assuring systems correctness is particularly
felt in hardware and software design, especially in
safety-critical scenarios. When we talk about a safety-critical
system, we mean the one in which failure is not an option. To
face this problem, several methodologies have been proposed.
Amongst these, model checking [1] results to be very useful.
This approach provides a formal-based methodology to model
systems, to specify properties via temporal logics, and to
verify that a system satisfies a given specification.<br>
<br>
Notably, first applications of model checking just concerned
closed systems, which are characterised by the fact that their
behaviour is completely determined by their internal states.
Unfortunately, model checking techniques developed to handle
closed systems turn out to be quite useless in practice, as most
of the systems are open and are characterised by an ongoing
interaction with other systems. To overcome this problem, model
checking has been extended to multi-agent systems. In the latter
context, temporal logics have been extended to temporal logics
for the strategic reasoning [2,3]. Here, the introduction of a
set of agents, each one with its visibility, makes the
verification very hard and often undecidable. Given the
relevance of this setting, even partial solutions to the problem
can be useful. Some approaches have focused on an approximation
either on the visibility [4, 5] or on the strategies [6] or on
the formulas [7].<br>
<br>
For the above reasons, there are few model checkers on
multi-agent systems and, to the best of our knowledge, only
MCMAS [8] handles logics for the strategic reasoning. Unluckily,
the latter does not provide a graphical interface, nor external
documentation to help developers. Furthermore, MCMAS does not
cover the most recent extensions that have been introduced in
theory in the past years (for example in [9,10]). Finally, MCMAS
contains bugs due to the lack of modularity and the fact that
different people have worked on it in different time and
research groups without producing an adequate documentation. It
is relevant to point out that the limitations currently observed
in MCMAS are mainly due to its being a research tool used
exclusively as a proof-of-concept for more theoretical
contributions. In this project, instead, we aim at studying,
engineering, and developing an easy to use, to maintain, and to
extend model checker whose target audience is both academia and
industry.<br>
<br>
Objectives<br>
<br>
The global objective of this PhD is to introduce an integrated
tool for the verification of multi-agent systems.<br>
<br>
The challenges of this PhD will be to tackle (some of) the
following points:<br>
- to study and develop a general-purpose framework for achieving
formal verification of multi-agent systems;<br>
- to develop a user-friendly GUI (Graphical User Interface) for
such framework;<br>
- to guarantee a tool that is modular and extendable for the
research community;<br>
- to analyse and explore the reality gap between theoretical
foundations of formal verification techniques in the area of
strategic reasoning and their practical counterparts;<br>
- to study and develop techniques to handle various kinds of
inputs as models via the introduction of automatic reductions
from classes of models to others (it requires the study of
equivalence relations amongst different formalisms);<br>
- to produce new extensions of models (e.g. by adding
weights/costs) and logics (e.g. by adding counting and strategic
costs);<br>
- to make the formal verification process accessible to research
areas currently not covered.<br>
</p>
[1] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking.
MIT Press, 1999.<br>
[2] R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-Time
Temporal Logic. JACM, 49(5):672–713, 2002.<br>
[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.<br>
[4] F. Belardinelli, A. Lomuscio, and V. Malvone. An
abstractionbased method for verifying strategic properties in
multi-agent systems with imperfect information. In AAAI, pages
6030–6037, 2019.<br>
[5] F. Belardinelli and V. Malvone. A three-valued approach to
strategic abilities under imperfect information. In KR, pages
89–98, 2020.<br>
[6] F. Belardinelli, A. Lomuscio, and V. Malvone. Approximating
perfect recall when model checking strategic abilities. In KR,
pages 435–444, 2018.<br>
[7] A. Ferrando and V. Malvone. Towards the Verification of
Strategic Properties in Multi-Agent Systems with Imperfect
Information. CoRR abs/2112.13621, 2021.<br>
[8] MCMAS <a class="moz-txt-link-freetext"
href="https://vas.doc.ic.ac.uk/software/mcmas/">https://vas.doc.ic.ac.uk/software/mcmas/</a><br>
[9] B. Aminof, V. Malvone, A. Murano, S. Rubin. Graded modalities
in Strategy Logic. Inf. Comput. 261: 634-649 (2018)<br>
[10] W. Jamroga, V. Malvone, A. Murano. Natural strategic ability.
Artif. Intell. 277 (2019)<br>
<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></p>
<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>:</p>
<p>- Curriculum vitae<br>
- Motivation letter<br>
- List of publications (if available)<br>
- List of courses taken during the studies (with assessments) </p>
<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>