DigiCosme Spring School 2016 on Hybrid SystemsMay 9 to 13 at ENSTA ParisTech, Palaiseau
Complexity and computability in dynamical systems
Olivier Bournez was a student of Ecole Normale Supérieure of Lyon from 1992 to 1996. He finished his PhD in the "Laboratoire de l’Informatique du Parallélisme (LIP)” in Lyon in 1999, after one year in “Verimag” laboratory in Grenoble where he did his national service as a researcher (Scientifique du Contingent) from 1997 to 1998. His PhD was about |
"Algorithmic complexity of continuous and hybrid dynamical systems”. He spent 9 years at INRIA in Loria laboratory in Nancy, and defended his habilitation (Habilitation à Diriger les Recherches) in 2006. In 2008, he got a Professor position at Ecole Polytechnique in Palaiseau. From 2010 to 2015, he was also the director of the Computer Science Laboratory of Ecole Polytechnique (Laboratoire d’Informatique de l’X, LIX). The research interests of Olivier Bournez include computability and complexity for continuous and hybrid systems, analog continuous time models of computations, and more generally computability and complexity theory and their relations with dynamical systems in various fields. More details can be found on his web page http://www.lix.polytechnique.fr/~bournez.
The talk will present a survey about the algorithmic complexity of properties for continuous dynamical systems. We will mainly focus on properties motivated by verification or control theory, such as reachability properties. We will focus on continuous time dynamical systems, discrete time dynamical systems working over a continuous space, as well as hybrid systems mixing both behaviors. We will discuss the hardness of the problems by exploring the boundary between what is decidable and what is not, which is a classical question, but also by exploring the boundary between what is polynomial time verifiable and what is not, which is a less studied question. We will relate these questions to other problems outside of these domains, in particular in the context of computation theory for continuous time models of computation.
Date and Time :Monday 9, 2.30 to 6 pm
Presentation Olivier Bournez
Observability and diagnosability of hybrid systems
Maria Domenica Di Benedetto has been Professor of Control Theory at University of l'Aquila since 1994. From 1995 to 2002, she has been Adjunct Professor at the Department of EECS, University of California at Berkeley. In 1987, she was Visiting Scientist al MIT, in 1988, 1989 e 1992 Visiting Professor at the University of Michigan, Ann Arbor, in 1992 Chercheur Associé, C.N.R.S., Poste Rouge, Ecole Nationale Supérieure de Mécanique, Nantes, France, from 1990 to 1995 McKay Professor at the University of California Berkeley. She is the Director of the Center of Excellence for Research DEWS "Architectures and Design methodologies for Embedded controllers, Wireless interconnect and System-on-Chip". She has been President of the European Embedded Control Institute since 2009. Since 2010, she has been a Member of the International Advisory Board of the Lund Center for the Control of Complex engineering systems (LCCC). Since 2013, she has been President of the Italian Society of researchers in Automatic Control (SIDRA).|
In 2002, she was elected IEEE Fellow. From 2007 to 2010, she has been member of the IEEE Control Systems Technical Fields Award Committee, IEEE Control Systems Society. From 2003 to 2007 she has been Chair of the Standing Committee on Fellow Nominations, IEEE Control Systems Society. From 1995 to 1999, she has been Associate Editor of the IEEE Transactions of Automatic Control. From 2006 to 2009, she has been Associate Editor at Large of the IEEE Transactions on Automatic Control. Since 1995 she is Subject Editor of the International Journal of Robust and Nonlinear Control. From 2016 she is Associate Editor of the IFAC Journal Nonlinear Analysis: Hybrid Systems.
Her research interests are centered about analysis and control of hybrid systems and networked control.
Hybrid systems, i.e., heterogeneous systems that include discrete and continuous-time subsystems, have been used to model applications in automotive such as engine, brake, and stability control, as well as air traffic control and manufacturing plant control. Because of their generality, deriving rigorous controller synthesis procedures is difficult. The most effective hybrid control algorithms are based on full state feedback. However, in the majority of cases, only partial information about the internal state of the hybrid plant can be measured. Observability is a concept of fundamental importance that establishes the conditions for reconstruction of the state of a system, while the related property of diagnosability corresponds to the possibility of determining the past occurrence of some particular states, for example faulty states. Observability and diagnosability play an essential role in general in safety-critical applications, so much so that requirements mandated by Governments, for example On-Board Diagnostic I and II and ISO26262, demand that the critical components of a car be observable and diagnosable.
Hybrid systems’ observability involves both the discrete structure and the continuous dynamics of the system. A hybrid system is said to be observable when it is possible to reconstruct the discrete as well as the continuous state of the system from the observed output information. In this talk, we will review and place in context how the continuous and the discrete dynamics, as well as their interactions, intervene in the observability property of a general class of hybrid systems. Moreover, we will present a general framework where diagnosability of the discrete structure of the hybrid system can be analyzed and characterized.
Date and Time :Thursday 12, 2.30 to 6 pm
Presentation Maria Di Benedetto
Formal verification of stochastic hybrid systems via formal abstractions
Alessandro Abate is an Associate Professor in the Department of Computer Science at the University of Oxford (UK), and is additionally affiliated with the Delft Center for Systems and Control at TU Delft (NL). He received a Laurea in Electrical Engineering in October 2002 from the University of Padova (IT), an MS in May 2004 and a PhD in December 2007, both in Electrical Engineering and Computer Sciences, at UC Berkeley (USA). He has been an International Fellow in the CS Lab at SRI International in Menlo Park (USA), and a PostDoctoral Researcher at Stanford University (USA), in the Department of Aeronautics and Astronautics. From June 2009 to mid 2013 he has been an Assistant Professor at the Delft Centre for Systems and Control, TU Delft - Delft University of Technology (NL).|
His research interests are in the analysis, verification, and control of probabilistic and hybrid systems, and in their general application over a number of domains, particularly in systems biology and in energy.
This seminar looks at the development of abstraction techniques based on quantitative approximations, in order to investigate the dynamics of complex systems and to provide computable approaches for the synthesis of control architectures. The approach employs techniques and concepts from the formal verification area, such as that of (approximate probabilistic) bisimulation, over models and problems known in the field of systems and control. While emphasising the generality of the approach over a number of diverse model classes, this seminar zooms in on stochastic hybrid systems, which are probabilistic models with heterogeneous dynamics (continuous/discrete, i.e. hybrid, as well as nonlinear). A case study in energy networks, dealing with the problem of demand response, is employed to clarify concepts and techniques. Theory is complemented by the development and use of SW tools, to be elucidated and demonstrated in the seminar.
Date and Time :Tuesday 10, 2.30 am to 6 pm
Presentation Alessandro Abate
Engineering Constraint Solvers for the Automatic Analysis of Hybrid Systems
Martin Fränzle is professor for hybrid discrete-continuous systems at the Carl von Ossietzky Universität in Oldenburg, Germany, where he also has been dean of the Faculty of Computing Science, Business Administration, Economics, and Law, and is affiliated with the research institute OFFIS as member of the board of the research division “Transportation”. Further affiliations include the DFG-funded Transregional Research Center SFB-TR 14 AVACS (Automatic Verification and Analysis of Complex Systems), there being coordinator for the research area hybrid systems and multiple projects, the DFG-funded graduate school DFG-GRK 1765 “SCARE — System Correctness under Adverse Conditions”, and the Interdisciplinary Research Center for Safety Critical Systems at Oldenburg University.|
Previous positions include an associate professorship and a visiting professorship at the Technical University of Denmark, post-doctoral positions at Oldenburg University, and a doctoral researcher position at Kiel University, where he obtained his doctoral degree. His research interests are in the modeling, verification, and synthesis of reactive, real-time, and hybrid discrete-continuous systems, with applications in highly automated driving and power networks. He has worked on the semantics of high-level modeling and specification languages and on logical and arithmetic decision problems and their application to verifying and synthesizing real-time and hybrid discrete-continuous systems including settings subject to stochastic disturbances. In particular, SAT-modulo-theory techniques for arithmetic constraint solving have been extended to the undecidable domain of arithmetic constraints involving transcendental functions and ordinary differential equations as well as to stochastic variants facilitating the fully symbolic analysis of probabilistic hybrid systems.
Within this lecture, we develop a constraint solving approach to the symbolic analysis of hybrid discrete-continuous systems. We start from a discrete-time, qualitative setting, proceed to continuous models involving non-linear ordinary differential equations, and finally address hybrid systems exhibiting both non-deterministic and probabilistic behavior akin to infinite-state Markov decision processes. To enable mechanized analysis of such systems, we extend the reasoning power of arithmetic satisfiability-modulo-theories (SMT) solving by, first, adding reasoning over transcendental functions and ordinary differential equations (ODEs) and, second, a comprehensive treatment of randomized (also known as stochastic) quantification as well as existential quantification.
Date and Time :Wednesday 11, 9.30 am to 1 pm
Presentation Martin Fränzle
Formal verification of linear hybrid systems
Goran Frehse is an assistant professor of computer science at Verimag Labs, University Grenoble Alpes, France. He holds a Diploma in Electrical Engineering from Karlsruhe Institute of Technology, Germany, and a PhD in Computer Science from Radboud University Nijmegen, The Netherlands. Before joining Verimag in 2005, he spent two years researching at Carnegie Mellon University. His main research interests are reachability analysis and compositionality of hybrid systems, as well as practical applications of these techniques. Goran Frehse developed PHAVer, a model checker for Linear Hybrid Automata, and is leading the development of SpaceEx, a verification platform for hybrid systems.|
This lecture gives an introduction to modeling mixed discrete-continuous systems and algorithms to check their behaviour. Hybrid automata combine finite state models with continuous variables that are governed by differential equations. Hybrid automata are used to model systems in a wide range of domains such as automotive control, robotics, electronic circuits, systems biology, and health care. Hybrid systems are difficult to analyze since neighboring states, no matter how close, may exhibit qualitatively different behaviors. Conventional techniques from model-based design, such as numerical simulation, may fail to detect critical behavior. Numerical simulation approximates the evolution of the variables with a sequence of points in discretized time. This highly scalable technique is widely used in engineering and design, but it is difficult to simulate all representative behaviors of a system. Set-based reachability constructs a cover of of all behaviors by exhaustively computing one-step successor states until a fixed-point is found. If precise enough, it can show safety of the system as well as provide quantitative measurements of key variables. On the downside, it can only be computed approximately and is difficult to scale to complex systems. Techniques like verification by simulation and approximate bisimulations help to overcome such limitations.
Date and Time : Thursday 12, 9.30 am to 1 pm
Presentation Goran Frehse
Simulation Based Design of Hybrid Systems with Formal Specifications
Alexandre Donzé is currently a research scientist at the department of Electrical Engineering and Computer Science of UC Berkeley, working in the group of Sanjit Seshia. In 2007, he graduated from Grenoble University with a Ph.D in Computer Science and Mathematics on simulation-based verification of hybrid systems, under the supervision of Oded Maler and Thao Dang at Verimag. In 2007-2008, He was a post-doctoral faculty at Carnegie Mellon University, working with Edmund M. Clarke and Bruce H. Krogh on the verification of control systems. Most notably, he worked on statistical Model Checking and systematic testing/simulation of Simulink models using sensitivity or uncertainty analysis. Back in Verimag in 2009, he contributed to the development of Spaceex, one of the leading reachability analysis tool for hybrid systems. started a collaboration with Eric Fanchon and others at TIMC laboratory on the topic of formal methods applied to systems biology, and later on joined UC Berkeley in 2012. A major focus of his research is the development and use of Signal Temporal Logic (STL), a formal specification language adapted to hybrid systems which include Cyber-physical (embedded) systems, circuits, biological systems, etc. He is the author of Breach, a Matlab toolbox supporting various simulation-based techniques using STL specifications, which is getting a wide adoption in both academia and industry. |
Hybrid systems used in practice for modeling complex systems and their physical environment are notoriously difficult to analyze, verify or control formally. One reason is that practical modeling tools, such as Simulink, favor expressiveness and ease of use over rigor and simplicity. Their resulting semantics are far richer than the semantics supported by formal methods tools, and most models cannot be directly translated into equivalent models amenable to formal analysis. Another reason is scalability: models of practical interest are generally too large or complex to analyze formally. Last but not least, the cultural and educational gap between the engineer designing a system and the computer scientist building formal tools is such that the latter do not understand the needs and issues of the former, and the former do not see the benefits of explaining these issues and learning to use the tools of the latter.
Fortunately, over the years, middle grounds have appeared that help reduce these gaps. Simulation-based methods using formal specifications, for instance, are getting some traction from both industry and academia. The idea, simple, is that a simulation trace is an object that everybody can work with. Engineers get to develop their models and obtain simulation results with the tools of their choice, and computer scientists get to verify formal properties on the resulting traces. From there, a lot can be done to further close the loop. A simulation trace satisfying a property is usually not enough to prove a system correct, but a falsifying trace is often indicative of a design flaw. Hence the falsification problem, i.e., the problem of finding such falsifying traces is of great interest. A useful concept to solve it is that of quantitative satisfaction, which estimates "how far" a trace is from falsifying a specification. This quantity can be instrumented by an optimizer to get closer and eventually reach falsification. Another problem of interest is that of specification mining: given a set of traces, find a set of properties that are satisfied by these traces.
This talk will present a tool implementing these concepts called Breach. It interfaces with practical modeling and simulation tools, such as (but not limited to) Simulink, and supports formal specifications expressed in Signal Temporal Logic (STL). In Breach, parameters are first class citizens. Models behaviors are explored by defining and varying sets of parameters, and STL formulas are most often Parametric STL (PSTL) formulas. Falsification and specification mining can be casted as parameter synthesis problems, solved mostly by optimization involving quantitative satisfactions, which Breach can compute efficiently. The talk will present the concepts of simulation-based design using formal specifications and walk through a tutorial, demos and exercices based on Breach.
Date and Time : Tuesday 10, 9.30 am to 1 pm.
Presentation Alexandre Donze
Timed automata and beyond: On the quantitative analysis of timed systems
Patricia Bouyer, born in 1976, has contributed fundamental results to the theory and applications of timed automata as a fundamental model of real-time systems. Patricia Bouyer has received her PhD in 2002 from the Laboratoire de Specification et Verification, CNRS & ENS de Cachan, for the thesis "Models of Algorithms for the Verification of Timed Systems", and her habilitation in 2009 from the Universite Paris 7, for the thesis "From Qualitative to Quantitative Analysis of Timed Systems". In 2007 she received CNRS Bronze medal, awarded for outstanding achievements by a junior researcher, and she received in 2011 the Presburger Award, given by the EATCS (European Association of Theoretical Computer Science). She is the Principal Investigator of the ERC project EQualIS, on the quantitative verification of interacting systems, which started in 2013.|
Complex real-time systems require the development of quantitative models able to represent the various quantitative constraints of such systems. In the early 1990s, Alur and Dill proposed the prominent model of timed automata, which allows to express quantitative constraints on delays. This model has been extensively studied since then, and is now very well-adopted as a canonical model for real-time systems. Timed automata are not expressive enough for modelling other quantitative constraints on energy, bandwidth, etc… and for modelling interactions between several processes. To that aim, extensions have been proposed.
In this lecture, I will present the models of weighted timed automata and games, which extend timed automata with quantitative information for resource consumption, and with interaction. I will discuss decidability and algorithmics issues for these models. The lecture will give an overview of results of these last 15 years, and present a tool that we are developing.
Date and Time : Friday 13, 9.30 am to 1 pm
Presentation Patricia Bouyer Decitre
POSTERSPOSTER ALEXANDRE ROCCA
POSTER ENGEL LEFAUCHEUX
POSTER GHITA ION
POSTER HADI ZAATITI
POSTER HELA GUESMI
POSTER HICHAM ZATLA
POSTER JIEYING CHEN
POSTER KENZA MENOUER
POSTER SLIM MEDIEMGH
POSTER JULIETTE POCHET
POSTER YANN DUPLOUY
POSTER ALEXANDRE DAMBREVILLE
Address and directions
Address828, Boulevard des Maréchaux, 91762 Palaiseau Cedex
GPS : 48.711042, 2.219278
From Paris and Paris airports to Massy-Palaiseau
- From Orly Airport (about 30 min):
- take the ORLYVAL to Antony,
- then the RER line B, direction Saint-Rémy-les-Chevreuse.
- From Roissy Charles de Gaulle Airport (about 1 h):
- take the RER line B direction Saint-Rémy-les-Chevreuse.
From Massy-Palaiseau to ENSTA
- Take the bus 14 direction « École Polytechnique ». Stop at" La Hunière Concorde".
- Walk 5 minutes to ENSTA ParisTech
Organisation and contactAlexandre Chapoutot : scientific coordinator
Isabelle Glas : organisation
contact at digicosme.fr
CHAIRE INGENIERIE DES SYSTEMES COMPLEXES