HSCC Keynote

Compositional Synthesis for Symbolic Control

HSCC Keynote by Antoine Girard


Short bio
Antoine Girard is a Senior Researcher at CNRS and a member of the Laboratory of Signals and Systems (L2S). He received the Ph.D. degree in applied mathematics from Grenoble Institute of Technology, in 2004. From 2004 to 2006, he held postdoctoral positions at University of Pennsylvania and Verimag Laboratory. From 2006 to 2015, he was an Assistant/Associate Professor at the Université Grenoble-Alpes. His research interests mainly deal with analysis and control of hybrid systems with an emphasis on computational approaches, formal methods and applications to cyber-physical systems. He is also interested in multi-agent and distributed parameter systems. He received the George S. Axelby Outstanding Paper Award from the IEEE Control Systems Society in 2009. In 2014, he was awarded the CNRS Bronze Medal. In 2015, he was appointed as a junior member of the Institut Universitaire de France (IUF). In 2016, he was awarded an ERC Consolidator Grant.


Symbolic control aims at designing “correct by construction” controllers for continuous dynamical systems, by using algorithmic discrete synthesis techniques. The key concept in symbolic control is that of symbolic model (also called finite abstraction), which is a finite-state dynamical system, obtained by abstracting continuous trajectories over a finite set of symbols. When the symbolic and the continuous dynamics are formally related by some behavioral relationship (e.g. simulation or bisimulation relations), controllers synthesized for the symbolic model using discrete synthesis techniques can be refined to certified controllers for the original continuous system. Computation of finite abstractions is often based on discretization of the state and input spaces and therefore the symbolic control approach suffers from scalability issues. However, the design of large systems can still be tackled by means of compositional techniques.
In this talk, we will present some recent results on compositional synthesis in the symbolic control approach. Firstly, we will present an approach to compute abstractions of systems made of several, possibly overlapping components. Secondly, we will show how to synthesize decentralized (and possibly asynchronous) controllers for invariance properties, by combining these overlapping abstractions and assume-guarantee contracts. In the last part of the talk, motivated by the use of parametric assume-guarantee contracts for stability properties, we will show recent developments on abstraction-based quantitative synthesis.