I am particularly interested in exploring the links between AI Planning and Model Checking. My goal is to build compositional techniques for the verification of distributed systems.
Memberships
Member of the expert board of the Model Checking Contest @ Petri Nets since the 2015 edition.
Member of the steering committee of SynCoP since the 2019 edition.
Conducting the GT (previously action à vocation inter-GDR) AFSEC of GDR GPL, together with Mehdi Lhommeau.
Past memberships
Organizer of SynCoP 2018, a joint ETAPS workshop.
Member of the program committees of ACSD 2018 and ACSD 2019.
From January 2016 to December 2017, coordinator of a PHC Procope 2016 project involving the STR team (Nantes, France) and the Chair for Foundations of Software Reliability and Theoretical Computer Science (Munich, Germany). We worked on parallelizing message passing algorithms for model checking.
Involved in the ANR project PACS.
Reviews for journals and conferences
IEEE Transactions on Automatic Control; IEEE Transactions on Automation Science and Engineering; IEEE Transactions on Systems, Man and Cybernetics: Systems; Discrete Event Dynamic Systems; Automatica; Frontiers of Information Technology and Electronic Engineering; CDC 2010; SafeProcess 2012; LATA 2013; ECC 2013; CAV 2013; LICS 2013; ACSD 2013; MED 2015; FORMATS 2015; RTNS 2015; WODES 2016; ASE 2016; FORMATS 2017; WODES 2018; Petri Nets 2018; ACSD 2018; RTSS 2018; ECC 2019; ACSD 2019; WODES 2020; Petri Nets 2020.
Current works
Optimal planning in parametric systems
Student: Bastien Serée.
Collaboration with: Didier Lime.
Tree decomposition of graphs for efficient model-checking
Student: Peidong Zhang.
Collaboration with: Didier Lime.
We develop exact methods allowing the use of message passing algorithms on larger classes of interaction graphs than just trees. This is achieved by studying the structure of the interaction between the components of various real as well as randomly generated model checking problems, in order to see to which extent graph decomposition techniques can be applied (and extended) to deal with such interaction graphs. Currently, such decompositions are able to transform any interaction graph with cycles into a tree by merging some components, but are not designed for the particular case of message-passing algorithms (i.e. the tree they produce is in general not optimal for applying the message-passing).
Past works
Lazy Rechability Analysis in Distributed Systems
Collaboration with: Didier Lime.
We work on the problem of reachability in distributed systems, modelled as networks of finite automata. We have proposed and proved a new algorithm to solve it efficiently in many cases. This easily parallelizable algorithm allows to decompose the reachability objective among the components, and proceeds by constructing partial products by lazily adding new components when required. It thus constructs more and more precise over-approximations of the complete product. This permits early termination in many cases, in particular when the objective is not reachable, which often is an unfavorable case in reachability analysis. An early implementation of this algorithm — in a tool called LaRA — provided very encouraging experimental results: webpage on LaRA. These first results were presented at CONCUR'16.
We have recently extended the approach to network of timed automata. We lazily add components and clocks as well. The previous approach nicely extends to this setting, with two main technical difficulties however: invariants (i.e. urgency at some places of the automata) and resets of shared clocks. The tool LaRA has been extended to this setting as well: webpage on LaRA-T. These results were presented at FORMATS'17.
Finally, together with Bastien Serée, we extended these results to perform reachability analysis in unbounded Petri nets and in bounded Petri nets with inhibitor arcs. These results will be presented at Petri nets 2021.
Parallelization of Message-Passing Algorithms for Model Checking
Collaboration with: Javier Esparza.
Our goal is to build a distributed model checker for distributed systems. It will rely on the message-passing algorithms studied in my Phd. This work is partially funded by a PHC Procope 2016 project.
Postdoctoral works
Computation of summaries by Petri nets unfolding
Collaboration with: Javier Esparza and Stefan Schwoon.
Our goal was to describe precisely all the possible behaviours of an automaton (that we call interface) in a network of automata. For this purpose we compute the product of the automata in the network as a Petri net, unfold this net, project it on the interface, and refold the result to get an automaton (called a summary) having the desired property. The difficulty was to find stopping conditions for the unfolding process, ensuring to unfold sufficiently for having a summary while guarantying to have a finite unfolding in all cases. In particular, we exhibited an example showing that the standard criteria for stopping the unfolding process were too strict and led to incomplete summaries. Finally, we proposed an approach in which the stopping conditions are dynamic: a stopped part of the unfolding process can be reactivated depending on the evolution of the unfolding on the interface. This work has been presented at FSTTCS'13.
Verification of distributed systems with message-passing algorithms
Collaboration with: Javier Esparza.
We have shown that the message passing algorithms of my PhD can be used in a model checking setting, for verifying local properties of distributed systems. In particular, we looked at safety and vivacity properties. From these theoretical results we built a tool that we successfully compared to SPIN on two models of distributed systems: a mutual exclusion protocol due to Kerry Raymond and the Pragmatic General Multicast protocol. This work has been presented at VMCAI'14.
Computation of attractors by Petri nets unfolding
Collaboration with: Thomas Chatain, Stefan Haar, Loïc Paulevé, and Stefan Schwoon.
Opacity and concurrency
Collaboration with: Béatrice Bérard, Stefan Haar, John Mullins, and Stefan Schwoon.
Phd works
Planning with message-passing algorithms
Collaboration with: Éric Fabre, Patrik Haslum and Sylvie Thiébaux.
We have shown that the message passing algorithms, used in particular in constraint solving, can be used to find minimum cost paths in networks of automata. These algorithms allow to compute a summary of each of the automata of the network (that is, a complete representation of the behaviour of this automaton inside the network) by local computations (taking into account one automaton — and the automata it directly interacts with — at a time). From these summaries it is possible to directly (that is without computing the product of the automata) extract minimum cost paths without backtracking. These results have been applied to planning and implemented in a tool called Distoplan. They have been presented at several conferences (CDC'09 and ICAPS'10 in particular) and are regrouped in my PhD Thesis.
Distributed A*
Collaboration with: Éric Fabre.
Using message passing algorithms for factored planning can be seen as a top-down approach: from a representation of all the local plans of each component, successive refinements allow to keep only those plans that are part of global plans. At the end of my thesis we also worked on a bottom-up approach to factored planning: a unique plan is built by a set of cooperating agents (one agent per component). Each agent uses an algorithm close to A* to perform a local search, constrained by the searches of the other agents. An early version of this work has been presented at CDC'12 and a more general version of it is available in my PhD Thesis.
Probabilistic diagnosis
Collaboration with: Éric Fabre.
In parallel with my PhD work, we looked at probabilistic diagnosis. Given a probabilistic automaton in which only some actions can be observed, we aimed at building a finite deterministic machine (an observer) allowing to compute the probability to have reached each of the states of the automaton for any possible sequence of observations. A way to build such an observer already existed, but this observer was an object stronger than probabilistic automata: an automaton with probability matrices on transitions. This work has been presented at WODES'10.