Post-doctoral fellow in formal verification of multi-agent systems - 18 months contract

Who we are ?

Télécom Paris, part of the IMT (Institut Mines-Télécom) and a founding member of the Institut Polytechnique de Paris, is one of France's top 5 general engineering schools.

The mainspring of Télécom Paris is to train, imagine and undertake to design digital models, technologies and solutions for a society and economy that respect people and their environment.

We are looking for our future post-doctoral fellow to join the ACES team attached to the LTCI laboratory in the Computer Science and Networks Department. 

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, especially in 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 (MAS), using logics like Alternating-time Temporal Logic (ATL) and Strategy Logic (SL) to account for strategic reasoning.
Another key challenge 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. This project aims to study the decision problems related to natural strategies, analyze their computational complexity, and develop a tool for solving these problems.

Your main missions will be to :
- Carry out research in the field of multi-agent systems verification
- Provide mentoring and tutoring services
- Contribute to the reputation of the School, the Institut Mines-Télécom and the Institut Polytechnique de Paris.
- Publish scientific articles in the field of multi-agent systems verification

To succeed in this role, you will hold a PhD or equivalent. You have acquired in-depth theoretical and practical knowledge in the field of computer science, particularly in formal methods and verification of multi-agent systems. You are recognized for your team spirit, excellent interpersonal skills and teaching abilities.
Fluency in English is a prerequisite for this position.

Why join us?

You'll be working in a fast-growing, pleasant, green and accessible environment (especially for people with disabilities) just 20 km from Paris (RER B and C suburban train lines, close to major roads, shared shuttle departing from Porte d'Orléans). You will benefit from :

• 49 days annual leave (CA + RTT)
  
• flexible working hours (depending on department activity)
  
• telecommuting 1 to 3 days/week possible
  
• 75% public transport pass reimbursement
  
• Proximity to numerous sports facilities, concierge service, underground parking, in-house catering, etc.
  
• Staff association at school and ministry level
  
• Good to know: our social security contributions are lower than in the private sector

Other information :
Application deadline: 31/03/2025
Job type : 18 months fixed-term contract
Job description https://partage.imt.fr/index.php/s/69zC4zs8PAt5ZNk

Scientific contact person: Vadim Malvone (vadim.malvone@telecom-paris.fr)

Administrative contact person: Najoua Kharmaze (najoua.kharmaze@telecom-paris.fr)

We recruit on the basis of skills, regardless of origin, age or gender, and all our positions are open to people with disabilities.