[agents] PhD thesis proposal: "An Integrated Tool for the Verification of Multi-Agent Systems" - LTCI - Télécom Paris

[Vadim Malvone]

PhD thesis proposal on Computer Science / Artificial Intelligence

*An Integrated Tool for the Verification of Multi-Agent Systems
*

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.

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

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.

Objectives

The global objective of this PhD is to introduce an integrated tool for 
the verification of multi-agent systems.

The challenges of this PhD will be to tackle (some of) the following points:
- to study and develop a general-purpose framework for achieving formal 
verification of multi-agent systems;
- to develop a user-friendly GUI (Graphical User Interface) for such 
framework;
- to guarantee a tool that is modular and extendable for the research 
community;
- to analyse and explore the reality gap between theoretical foundations 
of formal verification techniques in the area of strategic reasoning and 
their practical counterparts;
- 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);
- to produce new extensions of models (e.g. by adding weights/costs) and 
logics (e.g. by adding counting and strategic costs);
- to make the formal verification process accessible to research areas 
currently not covered.

[1] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. 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.
[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.
[5] F. Belardinelli and V. Malvone. A three-valued approach to strategic 
abilities under imperfect information. In KR, pages 89–98, 2020.
[6] F. Belardinelli, A. Lomuscio, and V. Malvone. Approximating perfect 
recall when model checking strategic abilities. In KR, pages 435–444, 2018.
[7] A. Ferrando and V. Malvone. Towards the Verification of Strategic 
Properties in Multi-Agent Systems with Imperfect Information. CoRR 
abs/2112.13621, 2021.
[8] MCMAS https://vas.doc.ic.ac.uk/software/mcmas/
[9] B. Aminof, V. Malvone, A. Murano, S. Rubin. Graded modalities in 
Strategy Logic. Inf. Comput. 261: 634-649 (2018)
[10] W. Jamroga, V. Malvone, A. Murano. Natural strategic ability. 
Artif. Intell. 277 (2019)

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