A co-located workshop of the 63rd IEEE Conference on Decision and Control (CDC 2024), Milan, Italy, December 16-19, 2024. Registration information is available here, with an early bird registration deadline for this workshop set for October 1st, 2024.

Organizers

• Abolfazl Lavaei (Newcastle University)

• Chuchu Fan (MIT)

• Lars Lindemann (University of Southern California)

• Saber Jafarpour (CU Boulder)

Scope

Formal verification and controller synthesis for dynamical systems have garnered remarkable attention over the past two decades, driven by their extensive applications in safety-critical systems. These systems, whose failure can potentially result in severe consequences such as loss of life, injuries, or substantial financial losses, span wide-ranging domains, including aerospace, automotive, transportation systems, robotics, chemical processes, critical infrastructure, energy, and healthcare.

Given a property of interest for a dynamical model, formal verification is concerned to soundly check whether the desired specification is satisfied. If the underlying model is stochastic, the goal translates in formally quantifying the probability of satisfying the property of interest. A synthesis problem instead concerns dynamical models with the presence of control inputs: the goal is to formally design a controller (also known in different areas as policy, strategy, or scheduler), which is by and large a state-feedback architecture, to enforce the property of interest. This procedure is also called ‘‘correct-by-construction control design", since every step in the controller synthesis procedure comes with a formal guarantee. In a stochastic setting, the key objective is to synthesize a controller that optimizes (e.g., maximizes) the probability of satisfying the given specification. As a result of their intrinsic soundness, formal methods approaches do not require any costly, exhaustive, and possibly unsuccessful post-facto validation, which is needed in many safety-critical, real-world applications.

While formal verification and controller synthesis have become indispensable across numerous applications, they often necessitate closed-form mathematical models of dynamical systems. However, these models might either be unavailable or too complex to be constructed in real-world scenarios. Consequently, one can often not employ model-based techniques to analyze and design complex dynamical systems. Hence, the use of data-driven techniques becomes essential in enabling formal analysis for systems with unknown dynamics.

Over the past decade, several data-driven techniques have been proposed for the formal verification and controller synthesis of unknown dynamical systems. One may classify them in two types: the indirect and direct approaches. 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 classes of nonlinear systems, and accordingly, acquiring an accurate model for complex systems via those indirect techniques could be complicated, time-consuming and 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 systems.

Objectives of the workshop

In this workshop, we bring together a number of researchers active in the area of data-driven verification and control with provable guarantees. 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, by gathering a number of key talks 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 including indirect and direct data-driven 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: Marco Campi
  Affiliation: Professor at University of Brescia, Italy
  Title: Data-Driven Goal-Oriented Design and Verification of Reliability through Scenario Optimization
  Abstract: The use of data is becoming paramount in addressing modern design problems characterized by increasing complexity. Data are used to adjust otherwise general-purpose techniques to the specific problem at hand, thereby pursuing enhanced specification quality. But, can data-driven design be elevated to the status of a real science? One that is endowed with certified guarantees in relation to new, as-yet-unencountered, situations? This presentation will introduce Scenario Optimization, a technique for making certified designs based on data. Our ultimate message is that data can indeed serve a dual role: (i) providing information for making a design, while (ii) simultaneously evaluating the quality of the resulting outcome.
  Biography: Marco C. Campi is Professor of Automatic Control at the University of Brescia, Italy. He has held visiting and teaching appointments with Australian, USA, Japanese, Indian, Turkish and various European universities, besides the NASA Langley Research Center in Hampton, Virginia, USA. He has been IFAC TC-Chair of two committees for multiple terms and has served in diverse capacities on the Editorial Board of top-tier control and optimization journals like Automatica. In 2008, he received the IEEE CSS George S. Axelby outstanding paper award for the article “The Scenario Approach to Robust Control Design”. He has delivered plenary and semi-plenary addresses at major conferences including SYSID, MTNS, and CDC, and has been for four terms a distinguished lecturer of the IEEE Control Systems Society. Marco C. Campi is a Fellow of IEEE and a Fellow of IFAC. His interests include: inductive methods, data-driven decision-making, system identification, stochastic systems and control, randomized methods, and learning theory.

• Speaker: Samuel Coogan
  Affiliation: Associate Professor at Georgia Institute of Technology, USA
  Title: Interval-based Methods for Efficient Verification and Synthesis of Learning-enabled Control Systems
  Abstract: We present a computationally efficient framework for studying learning-enabled control systems using interval analysis. First, we develop a method for computing reachable sets of neural network-controlled systems. Our approach builds upon inclusion functions for the neural network controller and the open-loop system, and we particularly leverage the fact that many state-of-the-art neural network verifiers can produce inclusion functions for neural networks. We use these inclusion functions to construct an embedding system with twice the number of states as the original system and show that a single trajectory of this embedding system provides hyper-rectangular over-approximations of reachable sets. Next, we use this framework for training certified robust forward invariant user-prescribed polytopes in neural network-controlled systems. Our approach uses the concept of a lifted embedding system to turn a complex robust invariance condition into a single evaluation of a vector field in a higher dimensional space. By backpropogating against this simple condition, our algorithm finds neural network controllers for desired forward invariant polytopes. Time permitting, we also show how these techniques are leveraged to verify and synthesize controllers against signal temporal logic (STL) specifications using a novel interval extension of STL. Finally, complementary to our theoretical developments, we present efficient and automated implementations of our algorithms in our toolbox IMMRAX, an open-source toolbox based in the JAX framework for parallelizable and differentiable interval analysis.
  Biography: Samuel Coogan is an associate professor and the Demetrius T. Paris Junior Professor at the Georgia Institute of Technology in the School of Electrical and Computer Engineering. Prior to joining Georgia Tech in 2017, he was an assistant professor at the University of California, Los Angeles from 2015 to 2017. He received the B.S. degree in Electrical Engineering from Georgia Tech and the M.S. and Ph.D. degrees in Electrical Engineering from the University of California, Berkeley. His research is in the area of dynamical systems, nonlinear control, and autonomy and focuses on developing scalable tools for verification and control of networked, cyber-physical systems. He received a CAREER Award from the National Science Foundation in 2018, a Young Investigator Award from the Air Force Office of Scientific Research in 2019, and the Donald P Eckman Award from the American Automatic Control Council in 2020.

• Speaker: Na Li
  Affiliation: Professor at Harvard University, USA
  Title: Representation-based Control and Learning for Dynamical Systems
  Abstract: The explosive growth of machine learning and data-driven methodologies have revolutionized numerous fields. Yet, the translation of these successes to the domain of dynamical physical systems remains a significant challenge. Closing the loop from data to actions in these systems faces many difficulties, stemming from the need for sample efficiency and computational feasibility, along with many other requirements such as verifiability, robustness, and safety. In this talk, we bridge this gap by introducing innovative representations to develop nonlinear stochastic control and reinforcement learning methods. The key in the representation is to represent the stochastic, nonlinear dynamics linearly onto a nonlinear feature space. We present a comprehensive framework to develop control and learning strategies that achieve efficiency, safety, and robustness with provable performance. We also show how the representation could be used to close the sim-to-real gap.
  Biography: Na Li is a Winokur Family Professor of Electrical Engineering and Applied Mathematics at Harvard University. She received her Bachelor's degree in Mathematics from Zhejiang University in 2007 and Ph.D. degree in Control and Dynamical systems from California Institute of Technology in 2013. She was a postdoctoral associate at the Massachusetts Institute of Technology 2013-2014. She has held a variety of short-term visiting appointments including the Simons Institute for the Theory of Computing, MIT, and Google Brain. Her research lies in the control, learning, and optimization of networked systems, including theory development, algorithm design, and applications to real-world cyber-physical societal system. She has been an associate editor for IEEE Transactions on Automatic Control, Systems & Control Letters, IEEE Control Systems Letters, and served on the organizing committee for a few conferences. She received the NSF career award (2016), AFSOR Young Investigator Award (2017), ONR Young Investigator Award(2019), Donald P. Eckman Award (2019), McDonald Mentoring Award (2020), the IFAC Manfred Thoma Medal (2023), along with some other awards.

• Speaker: Nikolai Matni
  Affiliation: Assistant Professor at University of Pennsylvania, USA
  Title: Representation learning for dynamics and control
  Abstract: Representation learning, in which common features are extracted using data from heterogeneous sources or tasks, has underpinned much of the exciting recent progress in machine learning. Intuitively, using all of one's data to learn a common representation function benefits both computational effort and statistical generalization by leaving a smaller number of parameters to fine-tune on a given target task, and indeed, recent results support this intuition in the context of classification and regression over i.i.d. data. However, in order to reap the benefits of representation learning in the context of dynamics and control applications, algorithmic and analytical tools need to accommodate sequential data that is emphatically not i.i.d.. Towards that goal, we will first overview our recent progress in understanding how and when empirical risk minimization-based representation learning over data generated by a dynamical system is statistically beneficial, with a focus on applications to imitation learning. Then, time permitting, we turn our attention to optimization challenges (and solutions!) related to learning representations over non-isotropic non-i.i.d. data, and show how simple modifications to alternating-descent-methods can significantly improve their convergence properties.
  Biography: Nikolai Matni is an Assistant Professor in the Department of Electrical and Systems Engineering at the University of Pennsylvania, where he is also a member of the Department of Computer and Information Sciences (by courtesy), the GRASP Lab, the PRECISE Center, and the Applied Mathematics and Computational Science graduate group. He has held positions as a Visiting Faculty Researcher at Google Brain Robotics, NYC, as a postdoctoral scholar in EECS at UC Berkeley, and as a postdoctoral scholar in the Computing and Mathematical Sciences at Caltech. He received his Ph.D. in Control and Dynamical Systems from Caltech in June 2016. He also holds a B.A.Sc. and M.A.Sc. in Electrical Engineering from the University of British Columbia, Vancouver, Canada. His research interests broadly encompass the use of learning, optimization, and control in the design and analysis of autonomous systems. Nikolai is a recipient of the AFOSR YIP (2024), NSF CAREER Award (2021), a Google Research Scholar Award (2021), the 2021 IEEE CSS George S. Axelby Award, and the 2013 IEEE CDC Best Student Paper Award. He is also a co-author on papers that have won the 2022 IEEE CDC Best Student Paper Award and the 2017 IEEE ACC Best Student Paper Award.

• Speaker: Andreas A. Malikopoulos
  Affiliation: Professor at Cornell University, USA
  Title: Data-Driven Optimal Decentralized Control on Team Decision Problems
  Abstract: In this talk, I consider sequential dynamic team decision problems with delayed-sharing information structures. The team consists of a number of members who cooperate to achieve a common objective. I provide structural results for each team member that yield an information state that does not depend on their control strategy, and thus, it can lead to a dynamic programming decomposition where the optimization problem for each team member is over the space of their decisions. Then, I show that the solution of each team member is the same as the one derived by the “manager” of the team, who is a centralized solution. Therefore, each team member can derive their optimal strategy, which is also optimal for the team, without the manager’s intervention. The solution can be used to explore approaches at the intersection of learning and control for team decision problems with nonclassical information structures.
  Biography: Andreas Malikopoulos is a Professor in the School of Civil & Environmental Engineering and the Director of the Information and Decision Science Lab at Cornell University. Prior to these appointments, he was the Terri Connor Kelly and John Kelly Career Development Professor in the Department of Mechanical Engineering (2017-2023) and the founding Director of the Sociotechnical Systems Center (2019-2023) at the University of Delaware (UD). Before he joined UD, he was the Alvin M. Weinberg Fellow (2010-2017) in the Energy & Transportation Science Division at Oak Ridge National Laboratory (ORNL), the Deputy Director of the Urban Dynamics Institute (2014-2017) at ORNL, and a Senior Researcher in General Motors Global Research & Development (2008-2010). He received a Diploma from the National Technical University of Athens, Greece, and his M.S. and Ph.D. degrees from the University of Michigan, Ann Arbor, in 2004 and 2008, respectively, all in Mechanical Engineering. His research interests span several fields, including analysis, optimization, and control of cyber-physical systems; decentralized stochastic systems; stochastic scheduling and resource allocation; and learning in complex systems. Dr. Malikopoulos is the recipient of several prizes and awards, including the 2007 Dare to Dream Opportunity Grant from the University of Michigan Ross School of Business, the 2007 University of Michigan Teaching Fellow, the 2010 Alvin M. Weinberg Fellowship, the 2019 IEEE Intelligent Transportation Systems Young Researcher Award, and the 2020 UD’s College of Engineering Outstanding Junior Faculty Award. He has been selected by the National Academy of Engineering to participate in the 2010 German-American Frontiers of Engineering (FOE) Symposium and organize a session on transportation at the 2016 European-American FOE Symposium. He has also been selected as a 2012 Kavli Frontiers of Science Scholar by the National Academy of Sciences. Dr. Malikopoulos has been an Associate Editor of the IEEE Transactions on Intelligent Vehicles and IEEE Transactions on Intelligent Transportation Systems from 2017 through 2020. He is an Associate Editor of Automatica and IEEE Transactions on Automatic Control, and a Senior Editor of IEEE Transactions on Intelligent Transportation Systems. He is a Senior Member of the IEEE, a Fellow of the ASME, and a member of the Board of Governors of the IEEE Intelligent Transportation Systems Society.

• Speaker: Majid Zamani
  Affiliation: Associate Professor at University of Colorado Boulder, USA
  Title: Assured Autonomy Transfer
  Abstract: This talk investigates the recent advancements in certifying the safety of autonomous systems via barrier certificates. Traditional methods for formulating these certificates demand substantial expertise and computational resources, becoming unwieldy with even minimal system changes. Addressing this, we present a novel framework that leverages transfer learning, inverse dynamics, and system relationships, represented through neural networks, to facilitate the adaptation of safety controllers and assurances across diverse system environments. The integration of barrier certificates and safety controllers from a source system with the inverse dynamics of the target system offers a method to confirm formal safety proofs while streamlining proofs and controller transferability. We ensure the framework’s correctness with a neural network-based validity condition anchored in Lipschitz continuity, assuring the correctness of our controllers.
  Biography: Majid Zamani is an associate professor in the Computer Science Department at University of Colorado Boulder. Between May 2014 and January 2019, he was an assistant professor in the Department of Electrical Engineering at Technical University of Munich where he led the Hybrid Control Systems Group. He received a Ph.D. degree in Electrical Engineering and an MA degree in Mathematics both from University of California, Los Angeles in 2012, an M.Sc. degree in Electrical Engineering from Sharif University of Technology in 2007, and a B.Sc. degree in Electrical Engineering from Isfahan University of Technology in 2005. He received the George S. Axelby Outstanding Paper Award from the IEEE Control Systems Society in 2023, the NSF Career award in 2022 and ERC starting grant and ERC Proof of Concept grant from the European Research Council in 2018 and 2023, respectively. His research interests include verification and control of cyber-physical systems, secure-by-construction synthesis, and compositional analysis and synthesis of interconnected systems.

• Speaker: Stephanie Gil
  Affiliation: Assistant Professor at Harvard University, USA
  Title: The Role of Data and Physicality for Resilient Coordination in Networked Multi-Robot Teams
  Abstract: Multi-robot systems are becoming more pervasive all around us, in the form of fleets of autonomous vehicles, future delivery drones, and robotic teammates for search and rescue. As a result, it becomes increasingly critical to question the robustness of their coordination algorithms to reliable information exchange, security threats and/or corrupted data. This talk will focus on the role of control and information exchange for enhancing situational awareness and security of multirobot systems. We will focus on the problem of combining physicality and data to arrive at stronger notions of resilient multirobot systems.
  Biography: Stephanie is an Assistant Professor in the John A. Paulson School of Engineering and Applied Sciences (SEAS) at Harvard University. Her work centers around trust and coordination in multi-robot systems for which she has received the Office of Naval Research Young Investigator award (2021) and the National Science Foundation CAREER award (2019). She has also been selected as a 2020 Sloan Research Fellow for her contributions at the intersection of robotics and communication. She has held a Visiting Assistant Professor position at Stanford University during the summer of 2019, and an Assistant Professorship at Arizona State University from 2018-2020. She completed her Ph.D. work (2014) on multi-robot coordination and control and her M.S. work (2009) on system identification and model learning. At MIT she collaborated extensively with the wireless communications group NetMIT, the result of which were two U.S. patents recently awarded in adaptive heterogeneous networks for multi-robot systems and accurate indoor positioning using Wi-Fi. She completed her B.S. at Cornell University.

• Speaker: Miroslav Pajic
  Affiliation: Associate Professor at Duke University, USA
  Title: Statistical Verification of Learning-Based Cyber-Physical Systems
  Abstract: The use of Neural Network (NN)-based controllers has attracted significant attention in recent years. Yet, due to the complexity and non-linearity of such NN-based cyber-physical systems (CPS), existing verification techniques that employ exhaustive state-space search, face significant scalability challenges; this effectively limits their use for analysis of real- world CPS. In this talk, I will focus on the use of Statistical Model Checking (SMC) for verifying complex NN-controlled CPS. Using an SMC approach based on Clopper-Pearson confidence levels, we verify from samples specifications that are captured by Signal Temporal Logic (STL) formulas. Moreover, we will show how using such novel statistical tests, we developed the first statistical verification methods for the probabilistic conformance of a wide class of CPS, focusing on a notion of (approximate) probabilistic conformance for sets of complex specifications expressed by the Signal Temporal Logic (STL). Finally, we will show how these methods can be extended for verification of of hyperproperties for CPS, focusing on the joint probabilistic distribution of multiple paths, as well as specifications with nested probabilistic operators quantifying different paths, which cannot be handled by existing SMC algorithms.
  Biography: Miroslav Pajic is the Dickinson Family Associate Professor in the Department of Electrical and Computer Engineering at Duke University. He also holds a secondary appointment in the Computer Science Department, and the Department of Mechanical Engineering and Material Science. His research interests focus on the design and analysis of high-assurance cyber-physical systems with varying levels of autonomy and human interaction, at the intersection of (more traditional) areas of AI, learning and controls, embedded systems, robotics and formal methods. Dr. Pajic received various awards including the NSF CAREER Award, ONR Young Investigator Program Award, ACM SIGBED Early-Career Researcher Award, IEEE TCCPS Early-Career Award, IBM Faculty Award, ACM SIGBED Frank Anger Memorial Award, the Joseph and Rosaline Wolf Dissertation Award from Penn Engineering, as well as eight Best Paper and Runner-up Awards, such as the Best Paper Awards at the 2017 ACM SIGBED International Conference on Embedded Software (EMSOFT) and 2014 ACMIEEE International Conference on Cyber-Physical Systems (ICCPS), and the Best Student Paper award at the 2012 IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS). He is an associate editor in the ACM Transactions on Cyber-Physical Systems and ACM Transactions Computing for Healthcare (ACM HEALTH), and was a Chair of the 2019 ACMIEEE International Conference on Cyber-Physical Systems (ICCPS’19).

Workshop Program on December 15 (Local Time)