Robot supervisor synthesis needs encoding liveness and auditing for deployment
Realizability Is Not Enough: Encoding, Liveness, and Auditing of Synthesized Robot Supervisors
RoboticsLogic in Computer Science
Summary
Robots make decisions based on actions that can sometimes fail, and simply proving a plan is possible is not enough to make reliable robots. The authors show that robot supervisors need careful design to handle failures, assumptions about retrying tasks, and checks to verify strategies before turning them into real software. They created an open-source tool that helps generate and analyze these robot control plans, finding better encoding and liveness methods to produce controllers that actually work on drones. Their process bridges the gap between proving plans work on paper and making sure robots really follow the expected behaviors.
What this means in practice
- •For robot developers: Generate, check, and deploy robot control supervisors with formal guarantees and verified behavior for multi-capability robots.
- •For drone engineers: Produce reliable drone controllers that handle capability failures and liveness to maintain mission progress and safety.
Authors
David C. Conner, Joshua Luzier, William J. Doyle, Emma R. Faith, Aubrie B. Kooiker, Andrew J. Farney, Sebastian Fox, Evangelina Grimes, Ian G. Conner, Kyle Bloom
Abstract
High-level robotic supervisors coordinate capabilities whose reported outcomes determine the robot's next action. Reactive synthesis can generate such supervisors with formal guarantees, but deployment requires more than proving a Generalized Reactivity (1) (GR(1)) specification realizable. Designers must encode failure-prone capabilities, choose liveness assumptions that match retry intent, audit strategies, and translate them into robot software. We present an open-source pipeline for Robot Operating System (ROS) 2 Flexible Behavior Engine (FlexBE) supervisors that generates capability-based GR(1) specifications, analyzes assumptions before synthesis, audits strategies, reduces states with a behavior-preservation proof, and emits executable state machines. Across four case studies (six comparisons), including hardware on two quadcopter platforms, we compare enumerated and one-hot encodings and two liveness formulations. Under the tested backend, enumerated encoding usually synthesizes faster, although fewer propositions do not reliably predict smaller controllers or lower symbolic cost. System-Goal without pending memory is the only liveness treatment confirmed to yield executable controllers under both encodings across the reported grid; Fair-Outcome can permit realizable cycles without designer-intended completion. For this backend and model, we recommend enumerated encoding with System-Goal and auditing every realized strategy, since proposition count and realizability do not measure deployability. The auditor is sound and complete for four structural defect classes (protocol violations, deadlocks, bounded-failure violations, goal-unreachable traps) but is not a general liveness verifier, and the reduction preserves capability-level behavior. Together, these stages narrow the gap between formal realizability and controllers that pass protocol and structural-progress checks.