(formerly known as "TEMPO")

Our research focuses on the automated verification and synthesis of safety-critical systems with quantitative constraints and complex interactions between components. We develop formal models and efficient algorithms to verify, optimize, and synthesize such systems.

## Permanent Members | ||

Dietmar Berwanger
Researcher, CNRS |
Patricia Bouyer-Decitre
Senior researcher, CNRS |
Paul Gastin
Professor, ENS Paris-Saclay |

Benedikt Bollig
Researcher, CNRS |
Laurent Doyen
Researcher, CNRS |
Stéphane Le Roux
Assistant professor, ENS Paris-Saclay |

## Associated and Temporary Members | ||

Fabian Reiter
Post-doctoral researcher, ERC project EQualIS |
||

## Ph.D. Students | ||

Marie Fortin
PhD student, ENS Paris-Saclay |
Mathieu Hilaire
PhD student |
Anirban Majumdar
PhD student |

Mauricio Gonzãlez
PhD student, ERC EQualIS |
Samy Jaziri
PhD student, ERC EQualIS |

The correctness of computerized systems is an important matter as those systems are entrusted more and more (sometimes critical) tasks in our everyday life. We develop techniques for verifying properties of (hand-made models of) such systems (a.k.a. model checking), and to automatically synthesize models satisfying a given set of correctness properties. Our techniques especially apply to embedded systems, which are small devices with a specific role, often having strong real-time and resource constraints, interacting with other components of a larger system.

The word 'quantitative' has several facets here: first the models and
properties to be checked may have quantitative aspects (real-time, energy
constraints, ...); it can also be that we want to *measure*
how much a system satisfies a given property (this can involve stochastic
aspects, but other approaches can be defined). We briefly develop three
directions where VASCO is contributing.

Timed automata extend finite-state automata with clocks, which are (real-valued) variables that can be used to model real-time-dependant behaviours of a system.

Timed automata were defined 25 years ago, and are now well-understood, with numerous theoretical results, efficient algorithms, and cutting-edge tools (e.g. Uppaal) that are able to handle real-life industrial cases.

Building on the success of timed automata, we keep on working on extensions of this model, in particular weighted timed automata, where extra variables (beyond clocks) can be used to keep track of resources (e.g. energy).

Timed automata are governed by a mathematical semantics, where the measure of time has infinite precision and transitions are instantaneous. This has many advantages for our algorithms, but makes a difference with the digital and imprecise nature of physical devices where those automata are implemented: it could be the case that a property of the model is lost when the model is implemented.

We proposed several approaches to bridge the gap between the mathematical and physical worlds, using a parameterized approach for introducing uncertainty in the delays.

Up to now, most of the developments in model checking have considered a boolean approach, where a property is either true or false. Recently, quantitative approaches have been proposed, with relaxed semantics of the satisfaction of properties: there can be several ways for a formula not to hold, and such quantitative approaches can give some insights about how wrong a formula is.

Compared to verification, automated synthesis goes one step further: instead
of checking properties of a hand-made model, it generates a model
(if any) satisfying the given requirements. In this setting, we usually
target *controller synthesis*, that is, the synthesis of one components
interacting with other components of the system. To this aim, we use a
parallel with *game theory*: the players are the components, the arena
is defined by a (graph) model of the system, the strategies correspond to
their behaviors, and the objective of the controller is to enforce the
correctness property.

Quantitative objectives are of particular importance in synthesis, since they can be used for generating optimal controllers. Various objectives can be considered, such as optimal cost or optimal average cost (and of course several qualitative and quantitative objectives can be mixed). In this setting, we focus on deciding the existence and synthesis of winning strategies, and on the complexity (e.g. in terms of memory) of those strategies.

Of particular interest for our target applications are games with limited resources. These resources can be measured in terms of memory or other quantitative aspects. Another important class are games with imperfect information, where the players do not have a complete view of the state of the game. We develop techniques for transforming incomplete-information games into perfect-information ones, trying to obtain practicable algorithms for this complex problem.

Games for synthesis have mostly been studied in the setting of two-player
zero-sum games: the controller that we want to synthesize has to enforce
correct evolution of the whole system whatever the other components do (while
obeying the rules of the game).
We recently turned to multi-player non-zero-sum games, which correspond to a
setting where we would synthesize several components. In this setting, the
objectives of the players are not opposite, and the notion of a winning
strategy is not relevant anymore. Instead, we focus on *equilibria*,
which correspond to rational behaviors (for
instance Nash
equilibria), and develop algorithms for computing the correponding
strategies.

Temporal logics are a powerful formalism for expressing correctness properties of a system. They have been extensively used in model checking. We focus on extensions of temporal logics for expressing objectives in games (especially the existence of winning strategies), and recently defined a very expressive logic that can handle non-zero-sum objectives in multi-player games. In a setting of a client-server interaction for instance, we would query the existence of a policy for the server that would limit the number of clients accessing a resource at the same time (mutual exclusion), while allowing all clients to eventually access the resource if they need it. In this framework, we develop algorithms for deciding and possibly synthesizing such strategies.