The Modelling Cluster (Pôle Modèles) of LMF is dedicated to the construction and analysis of computational models. It brings together three closely related research themes — Model Checking and Synthesis, Distributed and Concurrent Systems, and Critical Systems — which collectively address a wide range of challenges in the formal modelling of discrete and hybrid systems.
Research in the cluster focuses on developing abstract models that balance expressiveness with algorithmic tractability, aiming to capture essential system characteristics such as timing constraints, stochastic behaviour, concurrency, interaction with the physical environment, and human-in-the-loop decision-making. A central goal is to identify the modelling frameworks best suited for the specification, verification, and synthesis of complex systems.
Each of the three themes brings a complementary perspective to this common agenda:
- Model Checking and Synthesis investigates how system correctness can be established through automatic verification, and how implementations can be synthesised from formal specifications. Research areas include timed and weighted automata, specification logics, runtime monitoring and fault prediction in discrete event systems, game-theoretic methods for synthesis, and the algorithmic analysis of infinite-state systems.
- Distributed and Concurrent Systems studies the behaviour and coordination of interacting components operating with only partial knowledge of the system. Key topics include distributed automata and trace theory, agreement protocols in dynamic networks, Petri net unfolding techniques, and the modelling of physical effects such as metastability.
- Critical Systems focuses on systems with high requirements for safety, reliability, and robustness, especially in domains such as transportation, energy, and embedded control. Research addresses cyber-physical systems, design and verification of automated and semi-automated driving functions, human–machine interaction, and domain-specific modelling frameworks for simulation and analysis.
The activity of the Modelling Cluster also contributes to broader interdisciplinary efforts, in particular through interactions with research on artificial intelligence and synthetic biology.