CPS Events
Synthesis and Verification of Neural Feedback Controllers for Temporal Logic Tasks
Abstract
Signal Temporal Logic (STL) has become a popular logic for expressing spatio-temporal requirements for Cyber-Physical Systems (CPS). In this presentation, we address the problems of synthesizing and verifying Neural Network (NN) controllers for general STL specifications. Namely, given an STL specification in discrete time, we show how to synthesize feed-forward neural network (NN) controllers with ReLU activations for bounded sets of initial conditions. A key component of our synthesis tools is the use of quantitative semantics for STL. We present different smooth semantics for STL that can improve the performance of training algorithms for complex STL specifications. Since synthesis methods based on backpropagation are limited to probabilistic guarantees of correctness, we also present complete bounded-time reachability methods for NN controllers for STL requirements. In the case where both the plant model and the controller are ReLU-activated neural networks, we reduce the STL verification problem to a reachability problem in ReLU neural networks. In this scenario, we can prove system safety and, in addition, analyze system robustness against the STL requirement. Finally, we show how such reachability analysis can be performed when the set of initial conditions is a truncated probability distribution. This line of work establishes a new research direction for the quantitative verification of NN-based control systems. We demonstrate the practical efficacy of our techniques on a number of examples of learning-enabled control systems.
Speaker Bio
Georgios Fainekos (aka Dr. Φ) is a Senior Principal Scientist at Toyota Motor North America, Research & Development. He received his Ph.D. in Computer and Information Science from the University of Pennsylvania in 2008 where he was affiliated with the GRASP laboratory. He holds a Diploma degree (B.Sc. & M.Sc.) in Mechanical Engineering from the National Technical University of Athens. Among other professional roles, he was a tenured faculty of Computer Science and Computer Engineering at Arizona State University, and a Postdoctoral Researcher at NEC Laboratories America in the System Analysis & Verification Group. He is currently working on Cyber-Physical Systems (CPS) with a focus on autonomous mobile systems. His technical expertise is on formal verification and requirements, search-based testing, control theory, artificial intelligence, and optimization. In 2013, Dr. Fainekos received the NSF CAREER award and the ASU SCIDSE Best Researcher Junior Faculty Award. He has also been recognized with the top 5% teacher award in 2019 and 2021. His research has received several paper awards and nominations, and the 2008 Frank Anger Memorial ACM SIGBED/SIGSOFT Student Award. In 2016, Dr. Fainekos was the program co-Chair for the ACM International Conference on Hybrid Systems: Computation and Control (HSCC).
Distributed Control & Optimization Framework for Multi-Agent Systems in Space Applications
Abstract
Cooperative control of multi-agent systems has garnered significant attention across scientific communities for its diverse applications, including aerial vehicle formation for search and rescue, environmental monitoring, autonomous rendezvous and docking in space exploration, mapping and exploration of unknown environments by a swarm of mobile robots, coordinated optimal energy arrangement in smart grids, and precision agriculture. The overarching objective in these scenarios is to develop distributed control algorithms where each agent leverages both its local information and the information from other networked agents. However, sensing and actuation limitations, network malfunctions, communication latency, and other system-specific requirements pose significant challenges and add complexity to achieving collective decision-making. In this presentation, we introduce a novel distributed control and computationally efficient optimization framework tailored for multi-agent systems in space applications.
Bio
Himadri Basu is a postdoctoral research scholar at the Hybrid Systems Laboratory, University of California Santa Cruz, currently working on autonomous rendezvous & docking of spacecraft in in-orbit servicing applications. His research interests are in the broad areas of control theory, cyber-physical systems, hybrid systems, and coordinated control of multi-agent systems in space applications. He received his Ph.D. in Electrical and Computer Engineering from the University of New Hampshire in 2020. Prior to joining UCSC, he worked on the formation reconfiguration control problem of multi-satellite clusters in low-earth orbits at the University of Vermont, and stabilization of networked control systems under measurement intermittency at the University of Grenoble Alpes, France.
Learning Safe Control Laws from Expert Demonstrations
Abstract
Learning-enabled autonomous control systems promise to enable many future technologies such as autonomous driving, intelligent transportation, and robotics. Accelerated by algorithmic and computational advances in machine learning and the availability of data, there has been tremendous success in the design of learning-enabled controllers. However, these exciting developments are accompanied by new fundamental challenges that arise regarding the safety of these increasingly complex control systems. In this talk, I will provide new insights and discuss exciting opportunities to learn verifiably safe control laws. Specifically, I will present an optimization framework to learn safe control laws from expert demonstrations in a setting where the system dynamics are at least partially known. In most safety-critical systems, expert demonstrations in the form of system trajectories that showcase safe system behavior are readily available or can easily be collected. I will propose a constrained optimization problem with constraints on the expert demonstrations and the system model to learn control barrier functions for safe control. Formal correctness guarantees are provided in terms of the density of the data and the smoothness of the system model and the learned control barrier function. In a next step, we will discuss how we can account for model uncertainty and for hybrid system models in this framework. Finally, we will see how we can learn safe control laws from high-dimensional sensor data such as cameras. We provide two empirical case studies on a self-driving car and a bipedal robot to illustrate the method.
Bio
Lars Lindemann is an Assistant Professor in the Thomas Lord Department of Computer Science at the University of Southern California where he leads the Safe Autonomy and Intelligent Distributed Systems (SAIDS) lab. There, he is also a member of the Ming Hsieh Department of Electrical and Computer Engineering (by courtesy), the Robotics and Autonomous Systems Center, and the Center for Autonomy and Artificial Intelligence. Between 2020 and 2022, he was a Postdoctoral Fellow in the Department of Electrical and Systems Engineering at the University of Pennsylvania. He received the Ph.D. degree in Electrical Engineering from KTH Royal Institute of Technology in 2020. Prior to that, he received the M.Sc. degree in Systems, Control and Robotics from KTH in 2016 and two B.Sc. degrees in Electrical and Information Engineering and in Engineering Management from the Christian-Albrecht University of Kiel in 2014. His research interests include systems and control theory, formal methods, and autonomous systems. Professor Lindemann received the Outstanding Student Paper Award at the 58th IEEE Conference on Decision and Control and the Student Best Paper Award (as a co-advisor) at the 60th IEEE Conference on Decision and Control. He was finalist for the Best Paper Award at the 2022 Conference on Hybrid Systems: Computation and Control and for the Best Student Paper Award at the 2018 American Control Conference.
Building Safe Autonomous Systems Using Imperfect Components
Abstract
Modern autonomous systems are an ensemble of multiple components implementing machine learning, control, scheduling, and security. Current design flows aim for each of these components to work perfectly, and system design consists of composing these components together. As a result research in machine learning aims towards near-perfect classification or estimation, scheduling techniques aim to meet all deadlines, and security algorithms aim towards fully secure systems. While such separation of concerns has served us well till now, as systems become more complex, this goal towards achieving perfection is becoming unreasonable. In this talk we will argue that we can design safe autonomous systems, without requiring its components to be perfect -- as long as the imperfections of one component are balanced by suitable actions from other components. Such a design approach is potentially more reasonable and cost effective, and we will provide examples of how it plays out.
Speaker's Bio
Samarjit Chakraborty is a Kenan Distinguished Professor and Chair of the Department of Computer Science at UNC Chapel Hill. Prior to coming here in 2019, he was a professor of Electrical Engineering at the Technical University of Munich in Germany, where he held the Chair of Real-Time Computer Systems for 11 years. Before that he was an assistant professor of Computer Science at the National University of Singapore for 5 years. He obtained his PhD from ETH Zurich in 2003. His research interests can be best described as a random walk through various aspects of designing hardware and software for embedded computers. He is a Fellow of the IEEE and received the 2023 Humboldt Professorship Award from Germany.
Building a Framework for Trustworthy Autonomous Agents: Autonomous Agents and Value Alignment
Abstract
With recent advancements in systems engineering and artificial intelligence, autonomous agents are increasingly being called upon to execute tasks that traditionally required human or social value-judgements or norms. These are tasks that directly—and potentially adversely—affect human well-being and demand of the agent a degree of normative sensitivity and compliance. Such norms and normative principles are typically of a social, legal, ethical, empathetic, or cultural (‘SLEEC’) nature.
These norms that agents must comply with are generally discussed in the abstract as high-level principles such as “respect for human autonomy” or “non-maleficence.” However, realistically addressing these concerns requires taking these abstract principles and formulating them into concrete particular rules that agents can follow. This can be tricky as a norm such as privacy can have different, and potentially contradictory requirements, when considering either its cultural or legal dimension, for example.
In my presentation, I will discuss research done by my colleagues and I to create a process for deriving specific rules from general norms. This proposed framework helps bridge the gap between abstract value-judgements about what is right and wrong and what agents actually do in practice – helping resolve potential conflicts between norms and develop actionable rules.
Speaker Bio
Gabriel Nemirovsky is a Ph.D. candidate within the philosophy department at the University of York. Previously, he served as a researcher at the UKRI Trustworthy Autonomous Systems, Resilience Node, collaborating closely with diverse stakeholders including industry, academia, government, and non-governmental organizations. As a researcher in the Resilience Node, Gabriel helped shape ethical frameworks for autonomous systems, underscoring his commitment to interdisciplinary excellence. Gabriel's academic pursuits are driven by a profound interest in the social impact of technological innovation, the economic dynamics of innovation, and political philosophy centered on justice and democratic engagement.
