Logic List Mailing Archive

CfA: Postdoc Position in Verification of Multi-Agent Systems, Télécom Paris (France), deadline: 31 March 2025

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 framewor
k for reasoning about reactive systems, which are defined by interactions b
etween 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 rece
ntly, in AI, concerns formal-system verification. Model checking, introduce
d in the late 1970s, uses game theory to verify the behavior of systems aga
inst formal specifications. While initial applications focused on closed sy
stems, which are entirely determined by their internal states, most systems
 in practice are open, involving ongoing interactions. This led to the exte
nsion of model checking to Multi-Agent Systems, using logics like Alternati
ng-time Temporal Logic and Strategy Logic to account for strategic reasonin
g.

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

Goals

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

Profile and skills required

- PhD in computer science, mathematics, or related fields.
- Strong computer science and/or mathematical background (with particular a
ttention 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.recru
itee.com/l/en/o/post-doctorante-ou-post-doctorant-en-verification-de-system
es-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@telecom-paris.fr<ma
ilto:vadim.malvone@telecom-paris.fr>)
--
Vadim MALVONE
Associate Professor, HDR
[Tlcom 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 Tlcom Paris]<https://www.linkedin.com/school/telecom-paris/
>[Instagram Tlcom Paris]<https://www.instagram.com/telecom_paris/>[Fa
cebook Tlcom Paris]<https://www.facebook.com/TelecomParis>
Toute l'actualit scientifique de l'IMT : I'MTech<https://imtech.imt.fr>

--
[LOGIC] mailing list, provided by DLMPST
More information (including information about subscription management) can
be found here: http://dlmpst.org/pages/logic-list.php