[fg-arc] Postdoc position in formal verification of multi-agent systems

[Vadim Malvone]

*Study the impact of natural strategies in decision problems*

Keywords: Formal Verification, Model Checking for Multi-Agent Systems, 
Game Theory

Description

Game theory plays a crucial role in AI by providing a mathematical 
framework for reasoning about reactive systems, which are defined by 
interactions between multiple entities, or players. It has found 
significant applications across various fields, including economics, 
biology, and computer science. An important application of game theory 
in computer science and, more recently, in AI, concerns formal-system 
verification. Model checking, introduced in the late 1970s, uses game 
theory to verify the behavior of systems against formal specifications. 
While initial applications focused on closed systems, which are entirely 
determined by their internal states, most systems in practice are open, 
involving ongoing interactions. This led to the extension of model 
checking to Multi-Agent Systems, using logics like Alternating-time 
Temporal Logic and Strategy Logic to account for strategic reasoning.

Another decision problem in verification is synthesis, the process of 
creating a system that meets its specifications across various 
environments, particularly those involving rational agents. Rational 
synthesis, introduced in the 1990s, addresses this by ensuring that a 
system's behavior aligns with specified objectives across different 
agent interactions. However, decision problems in MAS verification can 
range from polynomial to undecidable, with complexity heavily influenced 
by the type of strategy used (memoryless vs. memoryful). Memoryless 
strategies are computationally efficient but less expressive, while 
memoryful strategies are more powerful but more complex. To address 
these issues, bounded approaches like natural strategies, which consider 
simpler strategies in line with bounded rationality, have been introduced.

Goals

The aim of this project is divided into two main steps:
     - Study decision problems for natural strategies and analyze their 
computational complexity.
     - Develop a tool capable of providing answers to decision problems 
on natural strategies.

Profile and skills required

- PhD in computer science, mathematics, or related fields.
- Strong computer science and/or mathematical background (with 
particular attention on formal methods and logic).
- Good programming skills.
- Good level in written and spoken English.

How to apply
If you are interested you can apply via: 
https://institutminestelecom.recruitee.com/l/en/o/post-doctorante-ou-post-doctorant-en-verification-de-systemes-multi-agents

Other information
Application deadline: 31/03/2025
Job type: 18 months fixed-term contract in the ANR NOGGINS project
Job description: https://partage.imt.fr/index.php/s/69zC4zs8PAt5ZNk
Scientific contact person: Vadim Malvone (vadim.malvone at telecom-paris.fr)

-- 

*Vadim MALVONE*
Associate Professor, HDR

Télécom Paris <https://www.telecom-paris.fr>
*Une école de l'IMT <https://www.imt.fr>*

*19 place Marguerite Perey CS 20031 91123 Palaiseau Cedex
**www.telecom-paris.fr* <https://www.telecom-paris.fr>
LinkedIn Télécom Paris 
<https://www.linkedin.com/school/telecom-paris/>Instagram Télécom Paris 
<https://www.instagram.com/telecom_paris/>Facebook Télécom Paris 
<https://www.facebook.com/TelecomParis>
*Toute l'actualité scientifique de l'IMT : **I'MTech* 
<https://imtech.imt.fr>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.uni-paderborn.de/pipermail/fg-arc/attachments/20250217/60b28ee1/attachment.htm>