Symbolic control and formal methods have been a promising direction in Systems and Control for several decades. Indeed, they allow in principle to provide formal guarantees on the behaviour of dynamical systems, even very complicated ones, by analysing models of such systems. However, such complicated systems are often naturally studied in a ‘model-free’, ‘data-driven’ fashion. Think for instance of a self-driving car, with many heterogeneous and complex components: this system is hard to model rigorously, but at the same time generates a huge amount of data via its many embedded sensors. Other examples include complex robots, smart grids, and many other modern systems.
If data are certainly an opportunity for symbolic control of complex systems, they provide technical challenges that are not well understood nowadays: how can one reconcile the intrinsically random nature of data-driven approaches with certified guarantees? How can we certify asymptotic properties from finite-time observations? In recent years, these questions have found partial answers and deep relations with topics such as Interval Markov Chains, the Scenario Approach, Ergodic Dynamics or Monotone Systems.
The event will consist of seven 40-minutes presentations from various leading researchers active in the topic. The goal of this full-day workshop is to introduce this recently emerged challenge to the community. As such, the talks will be aimed at a general public in control, with an emphasis on pedagogy to provide an entrance point to this exciting field in our community. The day will end with a panel discussion on the future directions of the topic.
Date and time: Tuesday, June 13th, 9:00-17:00
Location: University Politehnica of Bucharest, Library. Room: L.2.2, View Map
Registration: https://ecc23.euca-ecc.org/conference-registration/#workshopRegistration
Organizers:
Antoine Girard (CNRS)
https://sites.google.com/site/antoinesgirard/
Raphael Jungers (UCLouvain and Oxford Univ.)
https://perso.uclouvain.be/raphael.jungers/content/home
Manuel Mazo (Delft University of Technology)
https://mmazojr.3me.tudelft.nl/
Technical program:
9:00-9:10 - Welcome (Girard, Jungers & Mazo)
9:10-9:50 - Talk 1: Alessandro Abate (Univ Oxford) - Certified learning, or learning for verification? (slides)
9:50-10:30 - Talk 2: Pierre-Jean Meyer (Univ. Gustave Eiffel) - Mixed-monotonicity reachability analysis of uncertain neural networks (slides)
10:30-11:00 - Coffee break
11:00-11:40 - Talk 3: Adnane Saoud (CentraleSupélec) - Learning Guaranteed Representations of Dynamical Systems from Data (slides)
11:40-12:00 - Tool presentation and/or discussions
12:00-13:00 - Lunch
13:00-13:40 - Talk 4: Sofie Haesaert (TU Eindhoven) -Optimal experiment design for data-driven control and verification (slides)
13:40-14:20 - Talk 5: Raphael Jungers (UCLouvain) -Data-driven memory-dependent abstractions of dynamical systems (slides)
14:20-15:00 - Talk 6: Maryam Kamgarpour (EPFL) - From uncertainty data to robust satisfaction of formal specifications for an autonomous system (slides)
15:00-15:30 - Coffee break
15:30-16:10 Talk 7: Calin Belta (Boston Univ.) - Safety in Online Learning-based Control (slides)
16:10-17:00 Panel discussion (Panelists: Abate, Meyer, Saoud, Haesaert, Kamgarpour, Belta – Moderators: Girard, Jungers & Mazo)
Abstracts and bios of the speakers:
1/ Alessandro Abate (Univ Oxford)
https://www.cs.ox.ac.uk/people/alessandro.abate/home.html
Title: Certified learning, or learning for verification?
Abstract: We are witnessing an inter-disciplinary convergence between areas underpinned by model-based reasoning and by data-driven learning and AI. Original work across these areas is strongly justified by scientific endeavours and industrial applications, where access to information-rich data has to be traded off with a demand for safety criticality: cyber-physical systems are exemplar applications.
In this talk, I will report on ongoing initiatives in this cross-disciplinary domain. According to the dual perspective in the title of this talk, I will sketch, on the one hand, results where formal methods can provide certificates to learning algorithms, and on the other hand, results where learning can bolster formal verification and strategy synthesis objectives.
Bio: Alessandro Abate is a Professor of Verification and Control in the Department of Computer Science at the University of Oxford. Earlier, he did research at Stanford University and at SRI International, and was an Assistant Professor at the Delft Center for Systems and Control, TU Delft. He received a Laurea degree from the University of Padova and MS/PhD at UC Berkeley.
2/ Pierre-Jean Meyer (Univ. Gustave Eiffel)
http://chapal.eu/pierre-jean_meyer/
Title: Mixed-monotonicity reachability analysis of uncertain neural networks
Abstract: In this talk, we present a new reachability analysis approach to compute interval over-approximations of the output set of uncertain feedforward neural networks. This approach relies on an adaptation to neural networks of the existing mixed-monotonicity method initially introduced for the reachability analysis of dynamical systems. Unlike other tools in the literature focusing on small classes of piecewise-affine or sigmoid-shaped activation functions, the main strength of our mixed-monotonicity approach is its generality, since it can handle neural networks with any Lipschitz-continuous activation function.
Two related algorithms are proposed: one for the reachability analysis with respect to uncertainties on the network's inputs; another when we have additional uncertainties on the internal parameters of the network (weight matrices and bias vectors). In these algorithms, we efficiently apply mixed-monotonicity reachability analysis to all possible partial networks that can be extracted from the given neural network. This ensures the tightest possible interval over-approximation of the output set that could be obtained using mixed-monotonicity reachability.
In the case of input uncertainties only, our algorithm is compared to five other interval-based tools (Interval Bound Propagation, ReluVal, Neurify, VeriNet, CROWN) on both existing benchmarks and sets of randomly generated networks for four activation functions (ReLU, TanH, ELU, SiLU). For uncertainties on the network's parameters, the comparison is done with respect to our own generalization of the Error-based Symbolic Interval Propagation algorithm from VeriNet.
Bio: Pierre-Jean Meyer is a research fellow at the ESTAS lab of Université Gustave Eiffel in Lille, France. He received a PhD in Automatic Control from Université Grenoble Alpes, France, in 2015. He was a postdoctoral researcher at KTH Royal Institute of Technology in Stockholm between 2015 and 2017, and at University of California, Berkeley between 2017 and 2020. His main research topics are on formal methods of dynamical systems, including reachability analysis and abstraction-based control synthesis. His most recent interest is on the safety evaluation of neural networks.
3/ Adnane Saoud (CentraleSupélec)
https://sites.google.com/view/adnanesaoud/
Title: Learning Guaranteed Representations of Dynamical Systems from Data
Abstract: In the last few years, learning-based techniques have shown a great success to control complex cyber-physical systems (CPS), where learning-based tools are used to provide mathematical models of a system, based on which one can synthesize a controller. However, the use of learning-based techniques in the context of safety critical CPS is particularly problematic, since learning-based components are typically viewed as black box-type systems, lacking formal guarantees. In this talk, we first recall how symbolic control techniques can be used in the context of the control of CPS. Then, we focus on how to provide guarantees when learning is used at the model’s level, namely we show how to learn a symbolic model from data, while providing formal guarantees. This symbolic model will be then used to construct the controller for complex specifications, such as linear temporal logics, based on existing tools in the formal methods community.
Bio: Adnane SAOUD is an Associate Professor (Maître de conférences) at CentraleSupelec, University Paris-Saclay, France, and an Affiliate Professor at Mohammed VI Polytechnic University, Morocco. Between January and August 2021, he was a Postdoctoral Research Fellow in the Electrical and Computer Engineering Department at the University of California, Berkeley. Between January and December 2020, he was a Postdoctoral Research Fellow in the Electrical and Computer Engineering Department at the University of California, Santa Cruz. He received the Ph.D. degree in Control from CentraleSupelec, France, in 2019. In 2018, he was selected as one of the top three finalists for the Best student paper award at the European Control Conference, ECC. In 2020, he was selected as a finalist of the French national Best PhD award Discerned by the GdR MACS. In 2021, he was selected as one of the top three finalists of the EECI PhD award, recompensing the best PhD work in Europe in the field of Control. He obtained the M.Sc. degree in control from CentraleSupelec, France, in 2016, and Electrical Engineering degree from Ecole Mohammadia d’ingénieurs, (EMI), Morocco, in 2014. His current research interests include formal methods for Cyber-Physical systems, learning-based control, adaptive control and compositional analysis and synthesis of interconnected systems.
4/ Sofie Haesaert (TU Eindhoven)
https://www.sofiehaesaert.com/
Title: Optimal experiment design for data-driven control and verification
Abstract: Data-driven formal verification approaches for control systems are becoming more and more important. Using data-driven approaches, control systems can be still formally verified when there is missing information in the internal dynamics or the environment of the system. These methods require qualitative data that can represent the missing information. Therefore, it is of interest to design experiments that optimise the data collection and that enable the data-driven verification of formal system properties. This talk will detail the introduction of a Bayesian framework that can be used to reformulate the design of optimal experiments as a stochastic optimal control problem. For the data-driven verification of dynamic systems with internal uncertainty, this experiment design problem results in a policy for the dynamic selection of inputs during the experiment. Within formal methods-based motion planning applications in uncertain environments, a similar formulation can be used to design explorative routes that optimally scout the environment.
Bio: Sofie Haesaert is an Assistant Professor in the Control Systems group of the Department of Electrical Engineering at Eindhoven University of Technology. Her research interests lie in the development of verification and control synthesis methods for cyber-physical systems. She leads the formal methods for control of cyber-physical systems research group and the lab on autonomous motion control. Sofie Haesaert holds a bachelor's degree in Mechanical Engineering and a master's degree in Systems and Control from Delft University of Technology, both cum laude. Haesaert obtained her PhD from Eindhoven University of Technology (TU/e) in 2017 and then went to Caltech (USA) to do a postdoc. Since 2018 Haesaert is Assistant Professor in the Control Systems group.
5/ Raphael Jungers (UCLouvain)
https://perso.uclouvain.be/raphael.jungers/content/home
Title: Data-driven memory-dependent abstractions of dynamical systems
Abstract: We propose a sample-based, sequential method to abstract a (potentially black-box) dynamical system with a sequence of memory-dependent Markov chains of increasing size. We show that this approximation allows alleviating a correlation bias that has been observed in sample-based abstractions. We further propose a methodology to detect on the fly the memory length resulting in an abstraction with sufficient accuracy. We prove that under reasonable assumptions, the method converges to a sound abstraction in some precise sense, and we showcase it in two case studies.
This is joint work with Adrien Banse, Licio Romao, Alessandro Abate
Bio: Raphael Jungers is a Professor at UCLouvain, Belgium, currently on sabbatical leave at Oxford University. His main interests lie in the fields of Computer Science, Graph Theory, Optimization and Control. He received a Ph.D. in Mathematical Engineering from UCLouvain (2008), and a M.Sc. in Applied Mathematics, both from the Ecole Centrale Paris, (2004), and from UCLouvain (2005). He has held various invited positions, at the Université Libre de Bruxelles (2008-2009), at the Laboratory for Information and Decision Systems of the Massachusetts Institute of Technology (2009-2010), at the University of L´Aquila (2011, 2013, 2016), and at the University of California Los Angeles (2016-2017). He is a FNRS, BAEF, and Fulbright fellow. He has been an Editor at large for the IEEE CDC, Associate Editor for the IEEE CSS Conference Editorial Board, and the journals NAHS (2015-2016), Systems and Control Letters (2016-2017), IEEE Transactions on Automatic Control (2015-2020), Automatica (2020-). He was the recipient of the IBM Belgium 2009 award and a finalist of the ERCIM Cor Baayen award 2011. He was the co-recipient of the SICON best paper award 2013-2014, the HSCC2020 best paper award, and an ERC 2019 laureate.
6/ Maryam Kamgarpour (EPFL)
https://people.epfl.ch/maryam.kamgarpour?lang=en
Title: From uncertainty data to robust satisfaction of formal specifications for an autonomous system
Abstract: Formal specifications can be used to formulate complex tasks that autonomous systems need to satisfy. Often such systems operate in uncertain environments, consider for instance, autonomous driving where the future trajectory of other cars or pedestrians is uncertain. Our goal is to design controllers that are robust to these uncertainties. I discuss different frameworks that we have been developing to incorporate the data about the environment uncertainty in the control task. These formulations include data-driven chance constraints or conditional value at risk constraints, under unimodal and multi-modal distribution of the uncertainty. I illustrate our proposed approaches with autonomous driving examples, based on the state-of-the-art neural network trajectory prediction algorithms.
Bio:
Maryam Kamgarpour holds a Doctor of Philosophy in Engineering from the University of California, Berkeley and a Bachelor of Applied Science from University of Waterloo, Canada. Her research is on safe decision-making and control under uncertainty, game theory and mechanism design, mixed integer and stochastic optimization and control. Her theoretical research is motivated by control challenges arising in intelligent transportation networks, robotics, power grid systems and healthcare. She is the recipient of NASA High Potential Individual Award, NASA Excellence in Publication Award, and the European Union (ERC) Starting Grant.
7/ Calin Belta (Boston Univ.)
https://sites.bu.edu/hyness/calin/
Title: Safety in Online Learning-based Control
Abstract: Learning-based control methods, such as reinforcement learning (RL), are mostly used in simulated environments, where mistakes made by learning agents during training are largely inconsequential. For example, in a robotic application, collisions can be safely made during learning in simulation until adequate performance is achieved. Transferring such policies to real-world autonomous and robotic systems raises concerns related to the generalizability and adaptivity of such policies to novel environments encountered at run-time. In particular, for safety critical systems, violation of certain (safety) specifications during run-time are unacceptable. In this talk, I will present an online learning setting, where tools from control theory, formal methods, and machine learning are merged to enable autonomous systems to safely explore their environment in an effort to learn their underlying dynamics, while at the same time developing optimal control policies.
Bio: Calin A. Belta iis a Professor in the Department of Mechanical Engineering at Boston University, where he holds the Tegan Family Distinguished Faculty Fellowship. He is the Director of the BU Robotics Lab, and is also affiliated with the Department of Electrical and Computer Engineering and the Division of Systems Engineering at Boston University. His research focuses on dynamics and control theory, with particular emphasis on hybrid and cyber–physical systems, formal synthesis and verification, robotics, and systems biology, Notable awards include the 2005 NSF CAREER Award, the 2008 AFOSR Young Investigator Award, and the 2017 IEEE TCNS Outstanding Paper Award. He is an IEEE Fellow and a distinguished lecturer of the IEEE Control System Society.