MEXICO: Modelling and Exploitation
of Interaction and Concurrency
Research Topics
In the increasingly networked world, reliablity of applications becomes
ever more critical as the number of users of, e.g., communication systems,
web services, transportation etc grows steadily. MExICo works towards
a better understanding and an increased reliability of distributed
and asynchronous systems, and thus join the existing effort of many
other teams that use formal methods; what is particular in the present
proposal is that our team focusses its research on the two features of
concurrency and
interaction.
Members
Permanent Members 
Thomas Chatain
Assistant professor, ENS ParisSaclay 
Serge Haddad
Professor, ENS ParisSaclay 
Matthias Függer
Researcher, CNRS 
Stefan Haar
Senior researcher, Inria SaclayÎle de France 
Stefan Schwoon
Assistant professor, ENS ParisSaclay 
Associated and Temporary Members 
Philippe Dague
Visiting professor, UPSud 
Lina Ye
Visiting professor, Centrale Supélec 
Benoît Barbot
Associated professor, Université ParisEst Créteil 

Ph.D. Students 
Mathilde Boltenhagen
PhD student 
Igor Khmelnitsky
PhD student 
Hugues Mandon
PhD student, Inria 
Juraj Kolcak
PhD student, ANRFNR AlgoReCell 
Detailed Presentation
The increasing size and the networked nature of communication systems, controls,
distributed services etc. confront us with an ever higher degree of
parallelism between local processes. For any form of analysis and control, a
global view of the system state leads to overwhelming numbers of states and
transitions, and blurs the mechanics that are at work rather than exhibiting
them. Conversely, respecting concurrency relations avoids exhaustive
enumeration of interleavings, and allows to focus on 'essential' properties of
nonsequential processes characterized by causal precedence relations. We see
concurrency in distributed systems as an opportunity rather than a nuisance
that leads to state space explosion in the formal models and slows down
algorithms.
The MExICo team works on complex and concurrent systems from both
a theoretical and practical point of view. Our work is driven by applications
in two fields, namely
1.) Cyberphysical systems and 2.) Biological systems,
and by the methodological challenges posed on the abstract level in the
context of
 A: hybrid/timed/asynchronous systems,
 B: distribution and concurrency, and
 C: partially observable systems.
Application 1: Cyberphysical systems (CPS)
CPS are organized as networks of digital components which, on the one
hand, analyze information flows coming via sensors from the environment,
and on the other hand, react by controlling actuators. The efficient
management of these flows raises in particular the problems of choosing
an architecture and setting clock frequencies. We have attacked
this problem by weakening the classical untimed Boolean abstraction of
circuits, and treat them as timed hybrid systems with analog effects. Our
goals include
 to more accurately predict timing and power consumption,
and thus reduce conservative frequency and power margins; and
 to enable formal verification of circuits, meeting solvability boundaries
of classical problems such as short pulse filtration.
Concretely, this application has arisen in autonomous transportation
systems, in particular collision avoidance for autonomous vehicles.
Application 2: Biological systems
I: (Re)programming in discrete concurrent models
Cellular Regulatory networks  on the level of individual cells 
exhibit highly complex concurrent behaviours that are influenced by a
high number of perturbations such as mutations. We are in particular
investigating discrete models, both in the form of boolean networks and
of Petri nets, to harness this complexity, and to obtain viable methods
for two interconnected and central challenges:
 find attractors, i.e. longrun stable states or sets of states,
that indicate possible phenotypes of the organism under study, and
 determine reprogramming strategies that apply perturbations in
such a way as to steer the cell's longrun behaviour into some desired
phenotype, or away from an undesired one.
II : Distributed Algorithms in wild or synthetic biological systems
On the multicell level, we work with a distributed algorithms view
on microbiological systems, both with the goal to model and analyze
existing microbiological systems as distributed systems, and to design and
implement distributed algorithms in synthesized microbiological systems.
Major longterm goals are drug production and medical treatment via
synthesized bacterial colonies.
Research topic A: Systems continuous in state and time
We study modeling,
controller synthesis, and verification for systems that are continuous in state, time, or both. In particular, this includes
 use of hybrid system models as abstraction for differential
equations, e.g. describing signal traces of digital gates, to enable
verification of highspeed digital circuits;
 Continuous state Continuous Petri nets (CPN)
Research topic B: Distributed and concurrent systems
The analysis of discrete event systems is one of the central activities
of the team. We investigated several topics concerning concurrent systems
and distributed algorithms.
Unfoldings
The study of the partial order semantics of Petri nets and related
models has brought results on diverse applications, and on the theory
in its own right, such as for reset nets, summaries, reveals relations,
and goaldriven unfoldings; this is one of our key approaches.
Distributed Algorithms
We consider distributed algorithms for dynamic communication networks
to solve agreement problems. These algorithms occur as building
blocks in distributed control applications, such as distributed clock
synchronization. One major topic of research is metastabilitytolerant
circuits; it has applications in highspeed control circuits and
faulttolerant implementation of distributed algorithms.
Research topic C: Partially observable systems
In many systems, one or several observers can see only parts of the
execution, and strive to gain knowledge about the system state.
Diagnosis and Opacity
These observers may be
 friendly (performing diagnosis or testing) or hostile (trying to infer
secrets, in which case the designer wants to make the system opaque),
and
 be passive or active, i.e. help the system to either avoid or
diagnose faults;
furthermore, the systems under observation may be of different nature, e.g.
sequential/concurrent, nondeterministic, or probabilistic, etc.
Process Mining
When no complete model of the underlying dynamic system is available,
the analysis of logs may allow to reconstruct such a model, or at least
to infer some properties of interest; this activity, which has emerged
over the past 10 years on the international level, is referred to as
process mining. We have studied unfoldingbased unfoldingbased process
discovery , and the study of process alignments, and continue to work
on these fields under the particular angle of concurrent systems.
Tools
COSMOS
COSMOS is a statistical model checker
for Hybrid Automata Stochastic Logic. It evaluates such formulas on a
Discrete Event Stochastic Process (DESP), a class of stochastic models
which includes, but is not limited to, Markov chains. As a result, HASL
verification turns out to be a unifying framework where sophisticated
temporal reasoning is naturally blended with elaborate rewardbased
analysis. Cosmos is written in C++ and is freely available to the
research community.
MOLE
MOLE  A Petri Net
Unfolder implements the Esparza/Römer/Vogler unfolding algorithm
for lowlevel Petri nets.
National and International Collaborations
Ongoing projects
Past projects