The formal methods community has produced many successful results and tools in computer science, and over the past two decades has initiated a steady effort in moving towards applications in robotics. However, most researchers and practitioners in robotics are unaware of or find it difficult to adopt these methods due to: 1) the high initial effort to use, and 2) a disconnect between the method and tool developers and the larger community. While initially methods were shown in simple proof-of-concept scenarios, today, tools have matured to conform to the requirements of robotics applications. These tools offer the logical reasoning necessary to automate the planning and control programs, provide a-priori guarantees (certificates) for bug-free achievement of tasks, provide unambiguous specification languages for users, lay the foundation for formal verification of planning components (e.g. machine learning approaches), provide a framework for explainable deep learning, and enable embedding of logical structure in learned models. This workshop seeks to bring together the robotics and formal methods communities in a hands-on event that will demystify the current state-of-the-art, bridge the knowledge-transfer gap, and foster continued collaboration between the communities. We aim to encourage roboticists to adopt and include in their research automated synthesis and formal verification tools, and direct the formal methods community to the needs of robotics practitioners.

• To create a survey of tools within the formal methods community that will materialize into a repository of curated tools, and a survey paper in a leading robotics journal;

• To increase the visibility of existing tools and lower the barriers of entry for non-expert and starting researchers and students; curated tools presented during the workshop and collected afterwards will be assessed with respect to multiple measures of maturity (e.g., stability, repeatability, documentation, tutorials, demonstrations, maintenance, etc.);

• To define research and development tracks that foster wider adoption of formal methods in robotics.

• Tool Demonstration Submission Deadline: April 14th, 2024 (AoE)

• Acceptance Notifications: April 30th, 2024

• Presentation Submission Deadline: TBA

• Workshop Date: May 17th, 2024 

Ensuring Correct Behavior for (Learned) Robot Controllers with Topological Tools in a Latent Space

"Estimating the region of attraction (RoA) for a robot controller is essential for safe application and controller composition. One one hand, many existing methods require a closed-form expression that limit applicability to data-driven controllers. On the other hand, methods that operate only over trajectory rollouts tend to be data-hungry. This talk describes topological tools for RoA estimation based on Morse Graphs, which are directed acyclic graphs that combinatorially represent the underlying nonlinear dynamics. We show that Morse Graphs offer data-efficient RoA estimation without needing an analytical model for low dimensional benchmarks compared to a variety of alternatives. They struggle, however, with high-dimensional systems as they operate over a state-space discretization. We will proceed to show the Morse Graph-aided discovery of Regions of Attraction in a learned Latent Space (MORALS). The approach combines auto-encoding neural networks with Morse Graphs. MORALS shows promising predictive capabilities in estimating attractors and their RoAs for data-driven controllers operating over high-dimensional systems, including a 67-dim humanoid robot and a 96-dim 3-fingered manipulator. It first projects the dynamics of the controlled system into a learned latent space. Then, it constructs a reduced form of Morse Graphs representing the bistability of the underlying dynamics, i.e., detecting when the controller results in a desired versus an undesired behavior. The evaluation on high-dimensional robotic datasets indicates data efficiency in RoA estimation. "

Speaker: Kostas Bekris is a Professor of Computer Science at Rutgers University in New Jersey and an Amazon Scholar with Amazon Robotics. He is working in algorithmic robotics, where his group is developing algorithms for robot planning, learning and perception especially in the context of robot manipulation problems, robots with significant dynamics and a focus on taking advantage of novel soft, adaptive mechanisms. Applications include logistics and manufacturing as well as field robotics. He is serving as Editor of the Intern. Journal of Robotics Research (IJRR) and has served as Program Chair for the Robotics: Science and Systems (RSS) and the Workshop on the Algorithmic Foundations of Robotics (WAFR) conferences. His research has been supported by NSF, DHS, DOD and NASA, including a NASA Early Career Faculty award.

Formal Methods for Dynamical Systems: Completeness and Complexity

"I will provide a short and incomplete overview of existing approaches to formal synthesis for dynamical systems, with specific focus on completeness and complexity. I will first discuss automata-based approaches. I will then focus on two types of optimization-based approaches. First, I will show how optimal control problems for linear systems subject to signal temporal logic constraints can be mapped to mixed integer linear programs. Second, I will discuss approaches based on control barrier functions."

Speaker: Calin Belta is the Brendan Iribe Endowed Professor of Electrical and Computer Engineering and Computer Science at the University of Maryland, College Park. His research focuses on dynamics and control theory, with particular emphasis on cyber-physical systems, formal methods, and applications to robotics and systems biology. Notable awards include the 2008 AFOSR Young Investigator Award, the 2005 National Science Foundation CAREER Award, and the 2017 IEEE TCNS Outstanding Paper Award. He is a Fellow of the IEEE and a Distinguished Lecturer of the IEEE CSS.

A Bayesian approach to breaking things: efficiently predicting and repairing failure modes via sampling

"Before robots can be deployed in safety-critical applications, we must be able to understand and verify the safety of these systems. For cases where the risk or cost of real-world testing is prohibitive, we propose a simulation-based framework for a) predicting ways in which a robotic system is likely to fail and b) automatically adjusting the system’s design to mitigate those failures preemptively. We frame this problem through the lens of approximate Bayesian inference and use differentiable simulation for efficient failure case prediction and repair. I will introduce several applications of this approach on a range of robotics and control problems, including optimizing search patterns for robot swarms and reducing the severity of outages in power transmission networks."

Speaker: Dr. Chuchu Fan is an Assistant Professor in AeroAstro and LIDS at MIT. Before that, she was a postdoc researcher at Caltech and got her Ph.D. from ECE at the University of Illinois at Urbana-Champaign. Her research group, Realm at MIT, works on using rigorous mathematics, including formal methods, machine learning, and control theory, for the design, analysis, and verification of safe autonomous systems. Chuchu is the recipient of the 2020 ACM Doctoral Dissertation Award, an NSF CAREER Award, and an AFOSR Young Investigator Program (YIP) Award.

Preference-Based Planning in Stochastic Environments: From  Partially-Ordered  Temporal Goals to Most Preferred Policies

"Human preferences are not always represented via complete linear orders: It is natural to employ partially ordered preferences for expressing incomparable outcomes.   In this talk, I will present our recent work on decision making and probabilistic planning in stochastic systems, given a partially ordered preference over a set of temporally extended goals. Specifically, each temporally extended goal is expressed using a formula in Linear Temporal Logic on Finite Traces (LTLf).  The talk is centered upon three questions: How to express human's preference over temporal goals compactly and correctly as a computational model for planning and decision making? How to translate the preference relation over trajectories to a partial order over distributions over trajectories, induced by different policies in the stochastic systems? How to compute most preferred but incomparable policies? This presentation introduces theory and algorithmic solutions to address preference-based temporal logic planning and  discuss several potential future directions."

Speaker: Jie Fu received her Ph.D. in Mechanical Engineering from the University of Delaware in 2013, and subsequently worked as a Postdoctoral Scholar with the University of Pennsylvania from 2013 to 2015. From 2016 to 2021, she served as an Assistant Professor in the Department of Robotics Engineering at Worcester Polytechnic Institute. In 2021, she joined the Department of Electrical and Computer Engineering at the University of Florida as an assistant professor. Fu's research focuses on developing control theory and planning algorithms for constructing secured (semi-)autonomous systems with high-level logic reasoning and adaptive decision-making capabilities.  Dr. Fu has also received several early career awards, including the AFOSR Young Investigator Award and the DARPA Young Faculty Award in 2021, and the NSF CAREER Award in 2022. She has received funding for her research projects from ARO, NSF, DARPA, and AFOSR.

Formal Methods for Scalable Autonomy in Unknown Environments

"Recent advances in formal methods have enabled the design of new planning approaches capable of addressing a broader spectrum of class of tasks than the classical point-to-point navigation, capturing temporal and logical requirements. However, a key challenge in temporal logic planners is their high computational cost that increases exponentially fast as the number of robots or the task complexity increase. This limitation restricts their utility, particularly in dynamic and unknown environments where real-time replanning is imperative.

In the first part of this talk, I will introduce STyLuS*, a highly scalable optimal temporal logic planner for multi-robot systems operating in known environments. STyLuS* is a sampling-based planner that builds incrementally trees that explore the multi-robot motion space and an automaton state space in order to design optimal plans. A key novelty of STyLuS* is a biased sampling strategy allowing it to efficiently address temporal logic planning problems that involve hundreds of robots. In the second part of the talk, I will show how we have extended STyLuS* to address planning problems for perception-enabled robots residing in unknown semantic environments. The resulting planning algorithm enables robots to complete temporal logic tasks with user-specified probability, by actively mitigating environmental uncertainty stemming from imperfect perception. Several case studies that include aerial and ground robots will be presented to demonstrate the proposed algorithms."

Speaker: 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.

Talk 6

""

Speaker: 

Talk 7

""

Speaker: