Workshop on Data-Driven Verification and Control of Cyber-Physical Systems
 

A co-located workshop of the IFAC World Congress 2023, Yokohama, Japan, July 9, 2023

Organizers

Scope

The framework of cyber-physical systems (CPS) that captures the tight interaction of computational systems with the physical world is believed to carry great promises for analysis and design of systems in many safety-critical industrial applications. Examples of such applications include aerospace, automotive, transportation systems, robotics, chemical process, energy, and healthcare. Within CPS, embedded control software plays a significant role by monitoring and adjusting several physical variables through feedback loops where physical processes affect computation and vice versa. Although CPS have become ubiquitous in modern technology due to significant advances in computational devices, closed-form mathematical models for those complex systems are either not available or equally complex to be constructed. Consequently, one cannot employ model-based techniques to analyze and design this type of complex unknown systems. Hence, data-driven techniques are essential to provide formal analysis for CPS with unknown dynamics.

Over the past decade, two types of direct and indirect data-driven techniques have been proposed in the relevant literature for the formal analysis and design of unknown CPS. More specifically, indirect data-driven techniques are those which leverage system identification to learn approximate models of unknown systems, followed by model-based controller analysis approaches. Their advantage is that once the identification phase is achieved, one may rely on the powerful armada of techniques available in model-based control. On the downside, most identification techniques are mainly limited to linear or some specific class of nonlinear systems, and accordingly, acquiring an accurate model for complex systems via those indirect techniques could be expensive. In comparison, direct data-driven techniques are those that bypass the system identification phase and directly employ system measurements for the verification and controller design of unknown CPS.

Objectives of the workshop

In this workshop, we bring together a number of researchers active in the area of data-driven verification and control of CPS. The contributions will describe recently developed efforts towards new frontiers on the subject. Along with cherishing the exchange of ideas between researchers in the field, we aim to achieve the following goals for the audience attending the workshop:

  • Provide to the researchers new to these topics an updated view of the state of the art on data-driven verification and control of CPS including indirect and direct techniques;

  • Discuss scalable directions and areas to mitigate the, so-called, sample complexity;

  • Suggest novel applications of these data-driven techniques.

Additionally, we hope the active discussions of the participants will lead to fruitful collaborations.

Speakers

  • Speaker: Pietro Tesi
    Affiliation: Associate Professor at University of Florence, Italy
    Title: Event-triggered Control from Data
    Abstract: We present a data-based approach to design event-triggered state-feedback controllers for unknown continuous-time linear systems affected by disturbances. By an event, we mean state measurements transmission from the sensors to the controller over a digital network. By exploiting a sufficiently rich finite set of noisy state measurements and inputs collected off-line, we first design a data-driven state-feedback controller to ensure an input-to-state stability property for the closed-loop system ignoring the network. We then take into account sampling induced by the network and we present robust data-driven triggering strategies to (approximately) preserve this stability property. The approach is general in the sense that it allows deriving data-based versions of various popular triggering rules of the literature. In all cases, the designed transmission policies ensure the existence of a (global) strictly positive minimum inter-event times thereby excluding Zeno phenomenon despite disturbances. These results can be viewed as a step towards plug-and-play control for networked control systems, i.e., mechanisms that automatically learn to control and to communicate over a network.

  • Speaker: Necmiye Ozay
    Affiliation: Associate Professor at University of Michigan, USA
    Title: Learning-in-the-Loop Correct-by-Construction Control
    Abstract: In this talk, I will present some approaches for designing controllers for constrained control tasks when some of the components in the feedback loop are unknown and learned using data. In the first problem, we will assume the system model is unknown but a model estimate is learned from data. In the second problem, we will assume a perception module that generates output estimates from high-dimensional measurements is learned. In each case, we will show how the errors in the learned components can be propagated through the feedback loop when using a contraction-based tracking controller so that the overall tracking error can be bounded. This enables us to develop motion-planning algorithms that can operate provably safely in constrained environments. The approach will be demonstrated on interesting robotics tasks. Joint work with Glen Chou and Dmitry Berenson.

  • Speaker: Raphael Jungers
    Affiliation: Professor at UCLouvain, Belgium
    Title: Data-Driven Control of Hybrid Systems, Chance-Constrained Optimization, and Smart Abstractions
    Abstract: Control systems are increasingly complex, often at the point that obtaining a model for them is out of reach. In some situations, (parts of) the systems are proprietary, so that the very equations that rule their behaviour cannot be known. On the other hand, the ever-growing progress in hardware technologies often enables one to retrieve massive data, e.g. from embedded sensors. Because of these evolutions, control theory is moving from a model-based towards a model-free paradigm. For Linear Time-invariant systems, classical results from Identification theory provide a rather straightforward approach. However, these approaches become useless (or at least inefficient) if one relaxes the strong assumptions they rely upon (linearity, Gaussian noise, etc.). This is especially the case in safety-critical applications, where one needs guarantees on the performance of the obtained solution. Despite these difficulties, one may sometimes recover firm guarantees on the behaviour of the system. This may require to change one’s point of view on the nature of the guarantees we require.  I will provide examples of such results for different control tasks and different complex systems, and will raise the question of theoretical fundamental barriers for these problems.

  • Speaker: Chuchu Fan
    Affiliation: Assistant Professor at MIT, USA
    Title: Neural Certificates in Large-Scale Autonomy Design
    Abstract: Learning-enabled control systems have demonstrated impressive empirical performance on challenging control problems in robotics, but this performance comes at the cost of reduced transparency and lack of guarantees on the safety or stability of the learned controllers. In recent years, new techniques have emerged to provide these guarantees by learning certificates alongside control policies. These certificates provide concise, data-driven proofs that guarantee the safety and stability of the learned control system. These methods not only allow the user to verify the safety of a learned controller but also provide supervision during training, allowing safety and stability requirements to influence the training process itself. In this talk, we present an overview of this rapidly developing field of certificate learning. We hope that this talk will serve as an accessible introduction to the theory and practice of certificate learning, both to those who wish to apply these tools to practical robotics problems and to those who wish to dive more deeply into the theory of learning for control.

  • Speaker: Mahyar Fazlyab
    Affiliation: Assistant Professor at Johns Hopkins University, USA
    Title: Reachability Analysis of Neural Network Dynamical Systems
    Abstract: Neural Networks (NNs) have become increasingly effective at many difficult machine-learning and control tasks. However, the nonlinear and large-scale nature of neural networks makes them hard to analyze and, therefore, they are mostly used as black-box models without formal guarantees. This issue becomes even more complicated when NNs are used in learning-enabled closed-loop systems, where a small perturbation can substantially impact the system being controlled. In this talk, we present a plethora of tools based on optimization and robust control that can provide useful certificates of stability, safety, and robustness for NN-driven systems.

  • Speaker: Sofie Haesaert
    Affiliation: Assistant Professor at Eindhoven University of Technology, The Netherlands
    Title: Data-Driven Verification and Control Moving from Linear Dynamical Systems to Nonlinear Stochastic Systems
    Abstract: We often lack exact model knowledge of the dynamics of systems that we want to control in a verifiable manner. This can be due to lack of information on the physical composition of dynamic systems and its environment or due to wear and tear of the physical system during operation. Using data-driven approaches, controllers for these systems can be still formally verified. In this talk I will cover some of our results on data-driven verification and control synthesis for linear and nonlinear (stochastic) dynamics. I will explain how we can deal with missing information on the internal system dynamics or in the environment of the system and I will also highlight the design of experiments for data collection that supports an efficient data-driven toolchain.

  • Speaker: Abolfazl Lavaei
    Affiliation: Assistant Professor at Newcastle University, United Kingdom
    Title: Data-Driven Safety Verification of Unknown Systems with Formal Guarantees
    Abstract: In this talk, I will present a formal data-driven verification scheme for both discrete- and continuous-time systems with unknown mathematical models. The main target is to verify the safety of unknown systems based on the construction of barrier certificates via a set of data collected from trajectories of systems while providing an a-priori guaranteed confidence on the safety. In our proposed framework, we first cast the original safety problem as a robust convex program (RCP). Solving the proposed RCP is not tractable in general since the unknown model appears in one of the constraints. Instead, we collect finite numbers of data from trajectories of the system and provide a scenario convex program (SCP) corresponding to the original RCP. We then establish a probabilistic closeness between the optimal value of SCP and that of RCP, and as a result, we formally quantify the safety guarantee of unknown systems based on the number of data points and a required level of confidence. We propose our framework in both discrete- and continuous-time settings, considering both deterministic and stochastic scenarios.

  • Speaker: Sadegh Soudjani
    Affiliation: Associate Professor at Newcastle University, United Kingdom
    Title: Reinforcement Learning for Formal Synthesis of Cyber-Physical Systems
    Abstract: In this talk, I will go over recent results on learning methods to design controllers for cyber-physical systems. The goal of the controller is to maximise the probability of satisfaction of temporal specifications when the system is affected by uncertain factors. The goal of the learning is to obtain such controllers without the knowledge of state evolution of the system. In the first part of the talk, I will discuss how reinforcement learning (RL) can be used to get such controllers with theoretical epsilon-optimality guarantees for a fragment of linear temporal logic (LTL) specifications. The sub-optimality guarantee is established by projecting the sampled trajectories onto a finite abstract space. In the second part of the talk, I will discuss additional assumptions needed to get guarantees for full LTL specifications and show how to translate these specifications to average reward objectives for RL. If time permits, I will also briefly present a Bayesian approach to temporal logic control of uncertain systems based on coupled partial simulations relations. The results are obtained with collaborators from Max Planck Institute, Newcastle University, TU Eindhoven, and CU Boulder.

Workshop Program on July 9 (Local Time)

8:15–8:30 Welcome
8:30–9:15 Chuchu Fan, MIT, USA
Neural Certificates in Large-Scale Autonomy Design (slides)
9:15–10:00 Mahyar Fazlyab, Johns Hopkins University, USA
Reachability Analysis of Neural Network Dynamical Systems (slides)
10:00–10:30 Coffee break
10:30–11:15 Pietro Tesi, University of Florence, Italy
Event-triggered Control from Data (slides)
11:15–12:00 Abolfazl Lavaei, Newcastle University, United Kingdom
Data-Driven Safety Verification of Unknown Systems with Formal Guarantees (slides)
12:00–13:30 Lunch
13:30–14:15 Necmiye Ozay, University of Michigan, USA
Learning-in-the-Loop Correct-by-Construction Control (slides)
14:15–15:00 Sadegh Soudjani, Newcastle University, United Kingdom
Reinforcement Learning for Formal Synthesis of Cyber-Physical Systems (slides)
15:00–15:30 Coffee break
15:30–16:15 Raphael Jungers, UCLouvain, Belgium
Data-Driven Control of Hybrid Systems, Chance-Constrained Optimization, and Smart Abstractions (slides)
16:15–17:00 Sofie Haesaert, Eindhoven University of Technology, The Netherlands
Data-Driven Verification and Control Moving from Linear Dynamical Systems to Nonlinear Stochastic Systems (slides)
17:00–17:30 Discussions and Closing Remarks