Guaranteeing safety, predictability and reliability of robots is crucial for the assimilation of such systems into society, be it at home or in the workplace. While every robotics researcher working with or on a robot is aware of safety issues, only recently people have begun looking at ways to either formally prove or guarantee by design different behavioral properties such as safety and correctness.
The robotics domain offers unique challenges for verification and synthesis; Robots are mechanical systems working in the physical world in close proximity to people. Their sensors are noisy which induces significant uncertainty regarding their environment. Their actuation is not perfect, meaning that actions are not deterministic. Their state space is infinite and their desired behavior is often expressed in abstract terms (such as “search the rooms”, “pick up an object”, etc).
The goal of this workshop is to start a dialog between robotics researchers and the formal methods community. We aim to present the specific challenges, the current approaches in robotics (such as the use of temporal logics to specify tasks, correct by construction controllers, etc) and explore how ideas from these two disjoint communities can be used in this specific domain.
This workshop follows the successful workshops held at ICRA (International Conference on Robotics and Automation) 2009 and ICRA 2010. We believe that changing the venue from the Robotics conference to CAV will promote cross fertilization of ideas, facilitate interdisciplinary collaborations and stimulate further progress in the area.
The workshop consists of invited talks by both robotics and formal methods researchers in a format that promotes cross-discipline discussion.
Organizers:
- Hadas Kress-Gazit - Cornell University
- Nir Piterman - University of Leicester