ERAS Conference
1:30-4:30pm, May 30th, 2025
This workshop aims to provide an overview of the current research in formal methods for ensuring the safety, robustness, and trustworthiness of robotic systems, particularly in multi-agent systems. These methods have gained significant traction due to their capacity to formally verify critical properties of autonomous systems and to automatically generate robot control strategies from specifications, providing guarantees for the robot’s behavior. These notions of safety, robustness, and resiliency extend to multi-agent systems, but the curse of dimensionality is exacerbated in this domain. Providing guarantees to these systems is more challenging and relies on efficient computational methods.
Safety is typically encoded as part of the user-defined temporal logic formula as a constraint. This encoding is then verified at runtime when a robot synthesizes its controllers. For the scope of this workshop, we define a closed-loop system as safe if it satisfies this temporal logic formula. However, safety may be violated due to uncertainty in timing and/or space. Robustness ensures that the system can continue to operate under challenging conditions (e.g. disturbances). In contrast, resiliency focuses on the system’s ability to recover when being robust is not possible. In such scenarios, robots should be able to autonomously recover from unforeseen disturbances by changing their objectives in order to stay safe (i.e. maintain resiliency). The goal is to either to design controllers that respect the user-defined formula under these types of uncertainty, or to design specifications that take this uncertainty into consideration. This should happen both at the time of design and at runtime.