Seminars

This talk presents research contributions on Boolean Satisfiability (SAT) solving and its application to the analysis of discrete systems. The first part focuses on parallel SAT solving, addressing key issues such as modular solver design, the articulation between divide-and-conquer and portfolio approaches, and effective learned-clause sharing. In this context, the PaInleSS framework is introduced as a generic platform for building efficient parallel SAT solvers. The second part considers domain-aware SAT solving through programmatic extensions of CDCL, showing how problem-specific knowledge can improve solving strategies, especially in bounded model checking. The presentation concludes with an application to the verification of blockchain smart contracts, where SAT-based reasoning provides a promising basis for analyzing security- and safety-critical properties at scale.

Ce séminaire présente des travaux portant sur le développement d’approches formelles centralisées, modulaires et distribuées pour la modélisation, le contrôle, l’analyse des performances, la reconfiguration et la cybersécurité des systèmes à événements discrets. Ces travaux s’appuient sur différents formalismes tels que les réseaux de Petri (temporisés et colorés), les automates temporisés avec gardes, les automates hybrides, ainsi que les algèbres Max-Plus et Min-Plus et les séries formelles colorées. L’objectif est de proposer des méthodes d’analyse et d’aide à la décision permettant de garantir certaines propriétés des systèmes, notamment en termes de performance, de sûreté et de résilience. Une attention particulière est portée aux problématiques de modélisation et de vérification analytique dans des architectures d’automatisation distribuées (collaboration avec EDF). Les techniques formelles établies sont illustrées à travers plusieurs domaines d’application, notamment la résilience des chaînes logistiques, l’analyse du temps de réponse des systèmes de commande en réseau, les systèmes manufacturiers soumis à contraintes et la sécurité des systèmes cyber-physiques.

Les applications IoT déployées dans le continuum IoT–Fog–Cloud doivent concilier des contraintes de ressources, qualité de service (QoS), hétérogénéité et dynamique d’exécution, tout en restant robustes face aux pannes. Dans ce contexte, la fiabilité ne peut pas reposer uniquement sur des tests ad hoc : elle doit être construite et argumentée de manière systématique, depuis les exigences jusqu’au comportement observé en exécution. Nous présentons d’abord une approche centrée sur la vérification de mécanismes de tolérance aux pannes dans l’IoT multi-couches. La modélisation en Event-B, via raffinement et invariants, permet de formaliser des stratégies telles que la dégradation contrôlée, le basculement vers des composants de secours et la reprise/retour à un état sûr, tout en générant des obligations de preuve garantissant que ces mécanismes préservent les propriétés de sûreté attendues. Cette étape pose un socle : la résilience doit être spécifiée et justifiée rigoureusement, couche par couche, dans des architectures distribuées. Nous passons ensuite au Fog, où l’enjeu devient la composition de services sous contraintes, depuis les exigences jusqu’au déploiement (et, le cas échéant, l’interaction avec des services cloud). La démarche se décline en étapes : (i) capturer et structurer les exigences (fonctionnelles, coordination, ressources, QoS), (ii) décider un placement correct des composants, (iii) établir une configuration/reconfiguration d’un service composite en arbitrant entre efficacité QoS et fiabilité (notamment transactionnelle), puis (iv) vérifier formellement la cohérence de la composition et des interactions par Event-B. Dans cette dynamique, une perspective consiste à mobiliser des agents conversationnels (systèmes multi-agents conversationnels) pour soutenir l’orchestration et la reconfiguration (négociation de contraintes, adaptation, selection, assistance à la décision), tout en conservant un noyau formel vérifiable. Enfin, nous motivons une évolution méthodologique : Event-B est très puissant pour prouver des invariants et structurer la correction, mais il n’est pas toujours le plus adapté pour explorer exhaustivement certains comportements dynamiques typiques des systèmes distribués (interleavings concurrents, scénarios d’exécution, blocages, vivacité, effets de reconfiguration). Pour couvrir ces aspects, nous proposons de compléter la preuve par du model checking, en introduisant une transformation Event-B ? Réseaux de Petri Colorés (CPN). Cette transformation vise à obtenir un modèle exécutable et analysable, permettant ensuite d’appliquer des techniques de vérification automatique (exploration d’espace d’états, détection de deadlocks, propriétés de vivacité/atteignabilité) et de refermer la boucle : les contre-exemples et scénarios trouvés alimentent l’amélioration du modèle Event-B, des exigences et des politiques de configuration. Mots-clés Continuum IoT–Fog–Cloud, Fiabilité / Résilience, Qualité de service (QoS), Tolérance aux pannes multi-couches, Composition et (re)configuration de services, Placement sous contraintes, Vérification formelle, Event-B, Réseaux de Petri colorés (CPN), Model checking, systèmes multi-agents conversationnels

Rational synthesis studies the automatic construction of controllers that interact with rational agents pursuing their own objectives. Rather than assuming a hostile environment, this framework accounts for strategic behavior and equilibrium reasoning in multi-agent systems. In this talk, we consider rational synthesis in the presence of shared resources. Agents interact in turn-based games where actions may consume or replenish common resources, and must satisfy qualitative temporal objectives while avoiding resource depletion. We discuss how resource constraints fundamentally impact the synthesis problem, how the model evolves from single to multiple resources, and what this reveals about the limits of automated controller design.

This talk is organized into three main parts. The first part introduces research on Petri net structure theory and robust/adaptive supervisory control of discrete event systems, including controllability of siphons, supervisory control based on time constraints, and robust/adaptive supervisory control for systems with uncertainties caused by unreliable resources or operations. The second part concerns security analysis and resilient control of cyber-physical systems (CPSs) under information impairment. It discusses opacity analysis and resilient supervisory control strategies in the presence of cyberattacks and malicious intrusions. Furthermore, the talk addresses fault diagnosis in CPSs with communication delays. Finally, the talk highlights several future research directions, including prognosability analysis in CPSs with communication delays and the integration of data-driven approaches with supervisory control theory, aiming to enhance the security and resilience of next-generation CPSs.

The recently proposed logics PTATL and PSTCTL extend ATL and SCTL, respectively, to include both continuous time and stochastic aspects (probabilistic transition relations in models and agents' choices in strategies). As such, they have significant expressive power, but also high model checking complexity. I will present the essential theoretical background, as well as our approach to practical verification of these logics in asynchronous multi-agent systems, which combines two state-of-the-art tools IMITATOR and PRISM.

Interest is growing in social learning models where users share opinions and adjust their beliefs in response to others. Our work introduces generalized-bias opinion models, an extension of the DeGroot model, that capture a broader range of cognitive biases. These models can encompass, among others, dynamic (changing) influences, as well as in-group favoritism and out-group hostility, a bias where agents may react differently to opinions from members of their own group compared to those from outside. The reactions are formalized as arbitrary functions that depend, not only on opinion difference, but also on the particular opinions of the individuals interacting. Under certain reasonable conditions, all agents –despite their biases– will converge to a consensus if the influence graph is strongly connected, as in the original DeGroot model.

Client-server systems are a computing paradigm where work loads are distributed by the service providers called servers to the service requesters called clients. In case of a server handling an unbounded number of clients, how does one formally verify such systems? A first approach is to perform bounded model checking on it. Typically, in Bounded Model Checking (BMC), we find errors by examining all possible behaviours of the system for a specific temporal property up to some bounded number of steps. In case of unbounded client-server systems, the standard BMC approach does not suffice. What does one do when both the number of steps and the number of agents are unbounded? How do we choose a suitable model that captures true concurrency in the system? How do we specify the system properties in a suitable logic? In the first half of the talk, we focus on an extension to BMC to verify such unbounded client-server systems and also discuss the verification tool that employs SMT solvers. In the second half of the talk, we extend the idea of verification of systems with unbounded agents modeled using higher order Petri Nets called Elementary Object Systems (EOSs). We will present some decidability results for EOSs and a prototype to verify Petri Nets and EOSs using Answer Set Programming.