Realizability Is Not Enough: Encoding, Liveness, and Auditing of Synthesized Robot Supervisors

David C. Conner, Joshua Luzier, William J. Doyle +7

High-level robotic supervisors coordinate capabilities whose reported outcomes determine the robot's next action. Reactive synthesis can generate such supervisors with formal guara…