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 Paris-Saclay
Laurent Fribourg
Senior researcher, CNRS
Serge Haddad
Professor, ENS Paris-Saclay
Matthias Függer
Researcher, CNRS
Stefan Haar
Senior researcher, Inria Saclay-Île de France
Stefan Schwoon
Assistant professor, ENS Paris-Saclay

Associated and Temporary Members

Da-Jung Cho
Post-doctoral researcher, Digicosme
Philippe Dague
Visiting professor, UPSud
Daniele Zonetti
Post-doctoral researcher, Digicosme

Ph.D. Students

Mathilde Boltenhagen
PhD student
Igor Khmelnitsky
PhD student
Hugues Mandon
PhD student, Inria
Jawher Jerray
PhD student
Juraj Kolcak
PhD student, ANR-FNR AlgoReCell
Adnane Saoud
PhD student, Digicosme project Emergence Codecsys (joint with L2S)

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.) Cyber-physical systems and 2.) Biological systems, and by the methodological challenges posed on the abstract level in the context of

Application 1: Cyber-physical 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 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:

II : Distributed Algorithms in wild or synthetic biological systems

On the multi-cell 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 long-term 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

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 goal-driven 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 metastability-tolerant circuits; it has applications in high-speed control circuits and fault-tolerant 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 furthermore, the systems under observation may be of different nature, e.g. sequential/concurrent, non-deterministic, 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 unfolding-based unfolding-based 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 reward-based analysis. Cosmos is written in C++ and is freely available to the research community.

MINIMATOR

MINIMATOR allows to synthesize automatically a control for cyberphysical systems that satisfies desired properties of safety and stability. MINIMATOR has been successfully applied to real case studies such as power electronics devices and smart heating of an 11-room building in Denmark.

IMITATOR

IMITATOR is a software tool for parametric verification and robustness analysis of real-time systems with parameters. It relies on the formalism of networks of parametric timed automata, augmented with integer variables and stopwatches.

MOLE

MOLE - A Petri Net Unfolder implements the Esparza/Römer/Vogler unfolding algorithm for low-level Petri nets.

National and International Collaborations

Ongoing projects

Past projects

About LSV

About MExICo

A joint team with

Logo INRIA Saclay

Presentation of MExICo (2013)

Mexico presentation at AERES (2013)