[agents] PhD thesis proposal: "Improve Model Checking in Multi-Agent Systems via Runtime Verification" - LTCI - Télécom Paris

[Vadim Malvone]

PhD thesis proposal on Computer Science / Artificial Intelligence

*Improve Model Checking in Multi-Agent Systems via Runtime Verification
*

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).

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].

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.

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.

The challenges of this PhD will be to tackle (some of) the following points:

- to study model checking in the context of monolithic systems and 
multi-agent systems;
- to study runtime verification;
- to develop integrations of model checking and runtime verification 
techniques in the context of multi-agent systems;
- to develop techniques for combining model checking and runtime 
verification to find the decidability of model checking in undecidable 
contexts;
- 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).
- 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?
- 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.

[1] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT 
Press, 1999.
[2] G. Memmi. Integrated Circuits Analysis, System and Method using 
Model Checking. US Patent 7493247, Issued February 17, 2009.
[3] M. Leucker, C. Schallhart. A brief account of runtime verification. 
J. Log. Algebraic Methods Program., 2009.
[4] R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-Time Temporal 
Logic. JACM, 49(5):672--713, 2002.
[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.
[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.
[7] F. Belardinelli and V. Malvone. A three-valued approach to strategic 
abilities under imperfect information. In KR, pages 89–98, 2020.
[8] F. Belardinelli, A. Lomuscio, and V. Malvone. Approximating perfect 
recall when model checking strategic abilities. In KR, pages 435–444, 2018.
[9] A. Ferrando, V. Malvone. Towards the Verification of Strategic 
Properties in Multi-Agent Systems with Imperfect Information. CoRR 
abs/2112.13621, 2021.
[10] D. Ancona, A. Ferrando, V. Mascardi. Parametric runtime 
verification of multi-agent systems. In AAMAS. vol. 17, pp. 1457–1459, 2017.
[11] A. Ferrando, D. Ancona, V. Mascardi. Decentralizing MAS monitoring 
with decamon. In AAMAS vol. 17, pp. 239–248, 2017.
[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.

*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/c8ada482/attachment-0001.html>