Formal Methods and Decision Making in the Age of AI

The rapid advancement of machine learning and AI is leading to a paradigm shift in the way we make high-level decisions and low-level control for autonomous and robotic systems. While these advancements present exciting opportunities towards building intelligent systems, it also introduces new challenges, such as dealing with the fragility of neural networks, that require novel solutions. Our workshop on ``Formal Methods and Decision Making in the Age of AI'' aims to unravel these challenges and open problems for a general audience and discuss what new principles and techniques we need for perception-enabled system design, scalable design of distributed systems, verifiable learning-enabled systems, systems with humans in the loop, and safety in autonomy.

One of the primary objectives of the workshop is to identify key research challenges and opportunities in the areas of formal methods and decision making in the age of AI. The workshop has a focus on:

• Control of perception-enabled systems: Perception-enabled systems are those that use  high-dimensional sensors to make sense of the environment so that appropriate control actions can be taken. The workshop will popularize recent approaches for analyzing these systems, including statistical techniques for handling uncertainty under formal specifications.

• Scalable design of distributed systems: As AI becomes increasingly integrated into distributed systems, new methods are needed for designing and testing large-scale multi-agent systems. These design approaches need to be scalable and formally correct even in the face of agent failures and changing environmental conditions.

• Verifiable learning-enabled systems: As AI systems become more complex and autonomous, it becomes increasingly important to ensure and verifying that they are behaving as intended. Formal methods can be used to precisely formulate an intended system behavior, and new scalable formal verification tools need to be designed for verifying that high-dimensional learning-enabled systems are achieving their intended goals.

• Systems with humans in the loop: As humans become more integrated into AI systems, new approaches are needed for designing and evaluating feedback control loops that now incorporate robot and human feedback. The workshop will explore methods for ensuring that AI systems can effectively interact with humans. Formal specifications are close to structured language and present a convenient interface between humans.

• Safety in autonomy: One of the most critical challenges in the development of AI systems is ensuring their safety and reliability. There is a strong need for new methods for ensuring the safety of autonomous systems, including approaches for identifying and mitigating potential failures and developing backup systems in case of a failure.

The workshop will provide a platform for theoreticians as well as practitioners from the fields of  systems & control theory, formal methods, machine learning & AI, and applied mathematics to come together and discuss their latest research and emerging trends. Participants will be able to share their insights with each other on the current state-of-the-art in formal methods, decision making and AI, and explore opportunities for interdisciplinary collaborations. To further exchange between our speakers and participants, we will have panel discussions.

With this workshop, we would also like to address a common misconception that formal methods in robotics and control do not scale and are hence not practical. Our expert speakers will showcase that we can now solve real-life problems and have reached a certain stage of maturity. Therefore, the workshop will also promote the use of formal methods and decision making techniques in real-world applications, including autonomous driving and  robotic systems. 

Overall, the workshop aims to advance our understanding of the challenges and opportunities that arise from the use of AI in decision making. By bringing together experts from different fields, the workshop will facilitate interdisciplinary collaborations and foster the development of new approaches that can help ensure the safe and effective use of AI technologies.

• Workshop Date: December 12, 2023, 8:45am - 5:10pm

• Location: Orchid Junior 4211 (details)

Data-driven Verification and Control Synthesis for Dynamical Systems via Bayesian Reasoning

"Autonomous systems are poised to become an integral part of our economy, infrastructure, and society. They are rapidly gaining more capabilities via AI components and serving in ever more safety-critical roles. However, as their complexities grow, the more impossible it becomes to provide safety guarantees for their decisions and overall performance. In this talk, I argue that formal methods combined with control theory and machine learning techniques can form powerful tools to address this problem. To this end, I present our recent contributions that focus on data-driven approaches to formal analysis and control of highly uncertain systems.  Specifically, I focus on a framework for correct-by-construction control synthesis based on Bayesian reasoning, finite abstraction, and automata learning. I also discuss the importance of explanations in autonomous decision making and present our recently developed explanation scheme that provides easily-interpretable and verifiable explanations in the context of multi-agent planning."

Speaker: Dr. Morteza Lahijanian, University of Colorado Boulder

Bio: Dr. Morteza Lahijanian is an Assistant Professor in the Aerospace Engineering Sciences Department and Computer Science Department at the University of Colorado Boulder. Dr. Morteza Lahijanian received the B.S. in Bioengineering at the University of California, Berkeley, the M.S. in Mechanical Engineering at Boston University, and the Ph.D. in the field of systems and control theory with applications in robotics under the supervisions of Dr. Sean B. Andersson and Dr. Calin Belta at Boston University. Dr. Morteza Lahijanian was a postdoctoral fellow in the field of robotics under the guidance of Dr. Lydia Kavraki and Dr. Moshe Vardi in the Dept. of Computer Science at Rice University. Then, Dr. Morteza Lahijanian joined the Dept. of Computer Science at University of Oxford as a research scientist and worked with Marta Kwiatkowska on the "Mobile Autonomy: Safety, Trust, and Integrity" project. His research interests include dynamics, control theory, game theory, systems, and formal methods with applications in robotics, particularly, motion planning, strategy synthesis, model checking, hybrid systems, and human-robot interaction.

Formal methods for Cyber Physical Systems: State of the Art and Future Challenges

Slides

"Modern cyber-physical systems, like high-end passenger vehicles, aircraft, or robots, are equipped with advanced sensing, learning, and decision making modules. On one hand these modules render the overall system more informed, possibly providing predictions into the future. On the other hand, they can be unreliable due to problems in information processing pipelines or decision making software. Formal methods, from verification and falsification to correct-by-construction synthesis hold the promise to detect and possibly eliminate such problems at design-time and to provide formal guarantees on systems' correct operation. In this talk, I will discuss several recent advances in control synthesis and corner case generation for cyber-physical systems with a focus on scalability, and what role data and learning can play in this process. I will conclude the talk with some thoughts on challenges and interesting future directions."

Speaker: Dr. Necmiye Ozay, University of Michigan

Bio: Necmiye Ozay received her B.S. degree from Bogazici University, Istanbul in 2004, her M.S. degree from the Pennsylvania State University, University Park in 2006 and her Ph.D. degree from Northeastern University, Boston in 2010, all in electrical engineering. She was a postdoctoral scholar at the California Institute of Technology, Pasadena between 2010 and 2013. She joined the University of Michigan, Ann Arbor in 2013, where she is currently an associate professor of Electrical Engineering and Computer Science, and Robotics. Dr. Ozay’s research interests include hybrid dynamical systems, control, optimization and formal methods with applications in cyber-physical systems, system identification, verification \& validation, autonomy and dynamic data analysis. Her papers received several awards. She has received the 1938E Award and a Henry Russel Award from the University of Michigan for her contributions to teaching and research, and five young investigator awards, including NSF CAREER, DARPA Young Faculty Award, ONR Young Investigator Award, and NASA Early Career Faculty Award. She is also the recipient of the 2021 Antonio Ruberti Young Researcher Prize from the IEEE Control Systems Society for her fundamental contributions to the control and identification of hybrid and cyber-physical systems.

Spatiotemporal logic control for leader-follower multi-agent systems

Slides

"Formal methods based planning and control is an established methodology for autonomous systems that are subject to high level tasks. When it comes to multi-agent systems, recent trends involve objectives which are quantified in space and time in the form Signal Temporal Logic (STL) formulas and its variations. However, in most cases the agents are considered homogeneous with respect to their dynamics, sensing and communication constraints and actuation limitations. In this talk, we tackle a particular case of heterogeneous multi-agent systems under STL tasks, namely the case of leader-follower networks where an agent subgroup of leaders are responsible for the control objective fulfilment of the whole group. We start by presenting transient controllers for leader-follower networks in the framework of Prescribed Performance Control (PPC) and under simple control objectives such as consensus and formation control, and we then use these controllers as bases for more general multi-agent tasks given by STL. We provide necessary and sufficient conditions for STL task fulfilment that relate to the topology of the leader-follower network. This work is related to the recently defended PhD thesis of Fei Chen at KTH."

Speaker: Farhad Mehdifar, KTH Royal Institute of Technology

Bio: Farhad Mehdifar is a Ph.D. student at the Division of Decision and Control Systems (DCS) of KTH Royal Institute of Technology, advised by Prof. Dimos V. Dimarogonas. Previously, I was a research assistant at INMA, ICTEAM, UCLouvain in Belgium under an FRIA / FNRS fellowship. I got my B.Sc. and M.Sc. degrees in Electrical Engineering (Control Systems) from the University of Tabriz, Iran. 

Logic-based Specifications meet Learning-enabled Control

Slides

"Autonomous cyber-physical systems (CPS) are increasingly relying on learning-based techniques for perception, decision-making, and low-level control. An important aspect of such systems is that they are safety-critical: any undesirable behavior by such systems can cause serious harm to human lives or property. Formal methods research in the CPS area has long advocated the use of logic and automata as specifications for safety-critical CPSs, and the past few decades have seen significant strides in algorithms for their verification, testing, and automated synthesis. The challenge is to adapt such specification logics and verification algorithms to learning-enabled components (LECs) in CPSs. In this talk, we will review some recent work on using logic and learning-based techniques to provide guarantees for CPS applications using LECs. Specifically, we will discuss how we can combine approaches such as reinforcement learning and learning-from-demonstrations with temporal logic specifications, and how we can leverage statistical verification algorithms to provided probabilistic guarantees for learning-enabled CPS applications."

Speaker: Dr. Jyotirmoy Deshmukh, University of Southern California

Bio: Jyotirmoy V. Deshmukh (Jyo) is an Associate Professor in the Department of Computer Science at the University of Southern California, and the co-Director of the Center for Autonomy and AI. Before joining USC, Jyo worked as a Principal Research Engineer at Toyota R\&D. He got his Ph.D. from the University of Texas at Austin in 2010 and was a postdoctoral research fellow at the University of Pennsylvania. He is the recipient of the 2021 NSF Career Award and the 2021 Amazon Research Award. 

Certified learning, or learning for verification?

Slides

"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."

Speaker: Dr. Alessandro Abate, University of Oxford

Bio: Alessandro Abate is a Professor of Verification and Control in the Department of Computer Science at the University of Oxford. Earlier, Alessandro 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.

Formal Verification and Synthesis of Security for Cyber-Physical Systems: Notions, Algorithms and Recent Trends

"Engineering systems that involve physical elements controlled by computational infrastructures are called Cyber-Physical Systems. Ever-increasing demands for safety, security, performance, and certification of these critical systems put stringent constraints on their design and necessitate the use of formal model-based approaches to analyze and design of secure systems. In this talk, we focus on an important information-flow security property, called opacity, in the analysis of cyber physical systems. It captures the plausible deniability of the system's secret behavior in the presence of an intruder that may access the information flow. Particularly, we introduce the new concept of approximate opacity for dynamic systems whose output sets are equipped with metrics. Such systems are widely used in the modeling of many real-world systems whose measurements are physical signals. Approximate opacity quantitatively evaluates the security guarantee level with respect to the measurement precision of the intruder. We discuss how to verify and enforce approximate opacity for large-scale, or even infinite systems, using their finite abstractions. We also discuss some recent research progresses  and future directions on this topic."

Speaker: Dr. Xiang Yin, Shanghai Jiao Tong University

Bio: Xiang Yin was born in Anhui, China, in 1991. He received the B.Eng degree from Zhejiang University in 2012, the M.S. degree from the University of Michigan, Ann Arbor, in 2013, and the Ph.D degree from the University of Michigan, Ann Arbor, in 2017, all in electrical engineering. Since 2017, he has been with the Department of Automation, Shanghai Jiao Tong University, where he is an Associate Professor. His research interests include formal methods, discrete-event systems and cyber-physical systems. He is serving as the chair of the IEEE CSS Technical Committee on Discrete Event Systems, Associate Editors for the Journal of Discrete Event Dynamic Systems: Theory \& Applications, the IEEE Control Systems Letters, IEEE Transactions on Intelligent Vehicles, and a member of the IEEE CSS Conference Editorial Board. Dr. Yin received the IEEE Conference on Decision and Control (CDC) Best Student Paper Award Finalist in 2016.

Safe Perception-based Temporal Logic Planning in Unknown Semantic Environments

Slides

"Recent groundbreaking advances in robot perception, AI, and control theory have revolutionized the capabilities of autonomous robots in accomplishing diverse tasks in unknown environments such as package delivery, mapping of underground environments, surveillance, and environmental monitoring. However, with the rise of AI-enabled autonomous systems, new challenges regarding safety and reliability have surfaced. This talk particularly focuses on the safe integration of AI-enabled perception systems with decision making. Specifically, in this talk, (i) I will present a novel perception-based planning algorithm that allows teams of mobile robots to complete high level temporal logic tasks in unknown semantic environments. The proposed algorithm empowers the robots to actively mitigate environmental uncertainty arising due to imperfect AI-enabled perception in order to design uncertainty-aware paths accomplishing tasks with user-specified probabilistic performance and safety requirements. If time permits, I will briefly discuss (ii) how to enhance resiliency of the aforementioned multi-robot planning algorithm against individual system failures (e.g., sensor or actuation failures) and (iii) how the robots can actively interact with the unknown environment, by reconfiguring its structure, to facilitate task completion. The latter capability becomes vital in scenarios when the structure of the environment prevents task satisfaction (e.g., when all pathways towards goal regions are blocked by movable objects)."

Speaker: Dr. Yiannis Kantaros, Washington University St. Louis

Bio: Dr. Yiannis Kantaros is an Assistant Professor in the ESE Department at Washington University in St. Louis. Before joining WashU, he was a postdoctoral researcher in the Department of Computer and Information Science (GRASP and PRECISE lab) at the University of Pennsylvania.  He received the M.Sc. and the Ph.D. degrees in Mechanical Engineering and Materials Science from Duke University, Durham, NC, in September 2017 and May 2018, respectively. He also received the Diploma in Electrical and Computer Engineering from the University of Patras, Greece in July 2012. His current research interests include machine learning, distributed planning and control, and formal methods with applications in robotics. He received the Best Student Paper Award at the 2nd IEEE Global Conference on Signal and Information Processing in 2014 and the 2017-18 Outstanding Dissertation Research Award from the Department of Mechanical Engineering and Materials Science, Duke University, Durham, NC.

Assuring Safety of Learning-Enabled Systems with Perception Contracts

Slides

"Formal verification of deep learning models remains challenging, and yet they are becoming integral in many safety-critical autonomous systems. Verifying local robustness of neural networks is not useful because the system-level safety specifications are not available. We present framework for certifying end-to-end safety of learning-enabled autonomous systems using perception contracts. The method flows from the observation that learning-based perception is often used for state estimation, and the error characteristics of such estimators can be succinct, testable, and amenable to effective formal analysis. Our framework constructs approximations of perception models, using system-level safety requirements and program analysis. Mathematically proving that a given perception model conforms to a contract will be a challenge, but empirical measures of conformance can provide confidence levels to safety claims. We will discuss recent applications of this framework in creating low-dimensional, intelligible contracts and end-to-end safety certificates for vision-based lane keeping and auto-landing systems, as well as a number for future research directions."

Speaker: Dr. Sayan Mitra, University of Illinois at Urbana-Champaign

Bio: Sayan is the Associate Head of Graduate Affairs, Professor, and a John Bardeen Faculty Scholar of ECE at UIUC. Sayan received his PhD from MIT and his research is on formal verification and safe autonomy. His group is well-known for developing algorithms for data-driven verification and synthesis, some of which are being commercialized. His textbook on verification of cyber-physical systems was published in 2021.  Former PhD students from his group are now professors at Vanderbilt, NC Chapel Hill, MIT, and WashU. His group's work has been recognized with ACM Doctoral Dissertation Award, NSF CAREER Award, AFOSR YIP,  and several best paper awards.

Using data to tackle uncertainty in correct-by-design control synthesis

Slides

"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 talk about direct data-driven control synthesis and about Bayesian data-driven and model-based approaches."

Speaker: Dr. Sofie Haesaert, Eindhoven University of Technology

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.