From Safety to Guilty & from Liveness to Niceness

Robots are solving challenging tasks that we want them to be able to perform (liveness), but we also do not want them to endanger their surroundings (safety). Formal methods provide ways of proving such correctness properties, but have the habit of only saying “yes” when the answer is “yes” (soundness). More often than not, formal methods say “no”: They find out that the system is neither safe nor live, because there are “unexpected” circumstances in which the robot just cannot do what we expect it to. Inspecting those unexpected circumstances is informative, and identifies constraints on reasonable behavior of the environment. This ultimately leads from safety to the question of who is guilty depending on whose action caused the safety violation. It also leads from liveness to the question of what behavior of the environment is nice enough so that the robot can finish its task.