<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>Improve Model Checking in Multi-Agent
Systems via Runtime Verification<br>
</b></font></p>
Model Checking [1] is a well-known formal verification technique
which is used to check if a mathematical model of the system
satisfies a property specified via temporal logics. Therefore,
model checking has several applications (e.g., see [2]).
Unfortunately, this kind of technique is computationally expensive
and becomes easily unfeasible when applied to large systems (state
space explosion). Luckily, other more lightweight formal
verification techniques exist, like Runtime Verification [3],
where the verification of the property is performed at runtime on
the actual system (rather than on a model of the latter).<br>
<p> To solve the verification problem in which several systems
interact with each other, the model checking has been extended
to multi-agent systems. In this context, temporal logics have
been extended to temporal logics for the strategic reasoning
[4,5]. Here, the state space explosion remains an open problem
and in addition, 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 [6, 7] or
on the strategies [8] or on the formulas [9].<br>
<br>
Runtime Verification might help to overcome the difficulties of
the model checking, but it has never been applied to strategic
scenario. Instead, it has been mainly used to verify agent
interaction protocols [10,11], where the formal properties are
used to specify communication protocols, and runtime monitors
are used to verify whether the agents' communication is
conformant with such protocols. Moreover, since model checking
and runtime verification are two similar formal verification
techniques but different in principle, it is extremely relevant
to not only tackle the computational difficulties independently,
but also to consider possible integrations. Works on how to
integrate model checking and runtime verification exist (e.g.,
see [12]), but no work in the area of multi-agent systems, above
all when considering strategic reasoning, has ever been
proposed.</p>
<p>The aim of this research theme is to introduce, in theory and
practice, runtime verification in the model checking for
multi-agent systems. Moreover, by enhancing runtime verification
with strategic behaviour, very interesting new features can be
exploited. For instance, the dynamic synthesis of strategies for
the agents by monitoring the system execution.<br>
<br>
The challenges of this PhD will be to tackle (some of) the
following points:<br>
<br>
- to study model checking in the context of monolithic systems
and multi-agent systems;<br>
- to study runtime verification;<br>
- to develop integrations of model checking and runtime
verification techniques in the context of multi-agent systems;<br>
- to develop techniques for combining model checking and runtime
verification to find the decidability of model checking in
undecidable contexts;<br>
- to enhance runtime verification with a predictive behaviour by
first verifying properties via model checking on the strategic
context (at design time) and then applying runtime verification
for the remaining temporal part (at runtime).<br>
- to use runtime monitors to synthesize strategies. The existing
logics for the strategic reasoning try to answer the question:
Is there a strategy? But, another important question is: which
strategy?<br>
- to extend the theoretical foundations of runtime verification
to tackle strategic properties natively. Such extension will be
built on top of existing research regarding the use of runtime
verification on branching-time logics.<br>
</p>
[1] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking.
MIT Press, 1999.<br>
[2] G. Memmi. Integrated Circuits Analysis, System and Method
using Model Checking. US Patent 7493247, Issued February 17, 2009.
<br>
[3] M. Leucker, C. Schallhart. A brief account of runtime
verification. J. Log. Algebraic Methods Program., 2009.<br>
[4] R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-Time
Temporal Logic. JACM, 49(5):672--713, 2002.<br>
[5] 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>
[6] 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>
[7] F. Belardinelli and V. Malvone. A three-valued approach to
strategic abilities under imperfect information. In KR, pages
89–98, 2020.<br>
[8] F. Belardinelli, A. Lomuscio, and V. Malvone. Approximating
perfect recall when model checking strategic abilities. In KR,
pages 435–444, 2018.<br>
[9] A. Ferrando, V. Malvone. Towards the Verification of Strategic
Properties in Multi-Agent Systems with Imperfect Information. CoRR
abs/2112.13621, 2021.<br>
[10] D. Ancona, A. Ferrando, V. Mascardi. Parametric runtime
verification of multi-agent systems. In AAMAS. vol. 17, pp.
1457–1459, 2017.<br>
[11] A. Ferrando, D. Ancona, V. Mascardi. Decentralizing MAS
monitoring with decamon. In AAMAS vol. 17, pp. 239–248, 2017.<br>
[12] A. Ferrando, L. A. Dennis, R. C. Cardoso, M. Fisher, D.
Ancona, V. Mascardi. Toward a Holistic Approach to Verification
and Validation of Autonomous Cognitive Systems. ACM Trans. Softw.
Eng. Methodol. 30(4): 43:1-43:43, 2021.<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><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>