Vasco: Verification and Synthesis of Complex Systems

(formerly known as "TEMPO")

Research Topics

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.

Members

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
Mengqi Xie
PhD student, DigiCosme

Detailed presentation

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.

Quantitative verification

quantities 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 and extensions

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.

computer mouse

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).

Robustness of timed automata

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.

Measures of correctness

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.

Game theory for synthesis

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.

Games with quantitative requirements

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.

Multi-player games and the synthesis of complex systems

grid

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 for multi-player games

client-server

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.

National and international collaborations

Ongoing projects

Past projects

About LSV

Presentation VASCO (2013)

Tempo presentation at AERES (2013)

Vasco-Mexico seminar

No entries.

Ongoing projects

Recent Publications

All the Vasco publications

P. Bouyer, S. Jaziri and N. MarkeyEfficient Timed Diagnosis Using Automata with Timed DomainsIn RV'18, LNCS 11237, pages 205-221. Springer, September 2018. PDF | BibTeX )
P. Bouyer, M. González, N. Markey and M. RandourMulti-weighted Markov Decision Processes with Reachability ObjectivesIn GandALF'18, Electronic Proceedings in Theoretical Computer Science 277, pages 250-264. September 2018. Web page | PDF | BibTeX )
B. Bollig, P. Bouyer and F. ReiterIdentifiers in Registers - Describing Network Algorithms with Logic.  Research Report 1808.10240, Computing Research Repository, November 2018. 34 pages. Web page | PDF | BibTeX )
V. Brattka, S. Le Roux, J. S. Miller and A. PaulyConnected Choice and Brouwer's Fixed Point TheoremJournal of Mathematical Logic, 2018. To appear. BibTeX )
S. Le Roux, A. Pauly and M. RandourExtending finite-memory determinacy to Boolean combinations of winning conditionsIn FSTTCS'18, Leibniz International Proceedings in Informatics. Leibniz-Zentrum für Informatik, December 2018. BibTeX )

All the Vasco publications