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

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 · N/A · 2026

Summary

Abstract Summary

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.

Key Points

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.

Synthesis Pipeline Overview

Before presenting the demonstration domains, we summarize how our synthesis pipeline turns a description of a robot’s software capability interfaces into an executable FlexBE supervisor, and introduce the vocabulary the demonstrations rely on. Section 5 formalizes this pipeline in full.

This overview focuses on the concepts needed to read a capability configuration file and follow what the synthesized controller is doing.

Synthesis Pipeline Overview — Realizability Is Not Enough: Encoding, Liveness, and Auditing of Synthesized Robot Supervisors — Figure 2: The FlexBE Synthesis Pipeline builds a reusable capability catalog once at startup (Preprocessing) by discovering FlexBE’s existing state implementations, each of which interfaces with an underlying robot system capability such as planning, perception, or control. Request-time processing runs once per synthesis request and performs specification analysis, synthesis, auditing, and reduction before ending either in Failure or in a realized FlexBE state machine, loaded into FlexBE’s Behavior Engine for execution. The running HFSM activates the state implementations and receives their outcomes in return, driving the next transition.

Demonstrations

This paper presents four examples of synthesis using the modular pipeline. This section introduces the demonstration domains used throughout the paper so that the synthesis pipeline and specification choices can be described concretely. We describe the experimental setup and show the synthesized state machines executing here. Section 6 compares specification-generation variations.

All of the code required for these demonstrations is available open source CNURobotics (2026b) ; CNURobotics (2026a) .

Demonstrations — Realizability Is Not Enough: Encoding, Liveness, and Auditing of Synthesized Robot Supervisors — Figure 3: The Mealy strategy of Listing 2 , rendered by our mealy2dot tool in the visual convention used throughout this paper. Each raw slugs node is drawn as a linked pair: a large circle showing the node’s ID and which input propositions are true (an environment-observation state), followed by a green env$\to$sys edge to a small filled dot showing the same node’s ID suffixed _sys and which output propositions it newly asserts (a system-activation state). A red sys$\to$env edge then leaves that dot for each of the node’s trans successors, representing the environment’s next choice. Node 0 is idle ( bu false, no output asserted) and self-loops until the environment sets bu . Node 1 observes bu , and the system responds by asserting gr . Node 2 is entered with bu false again, and the system asserts br before returning to node 0.

Synthesis Pipeline

Section 3 introduced this pipeline’s stages and the capability vocabulary needed to read the demonstrations (Section 4 ). This section follows the stages shown in Fig. 2 : preprocessing, capability-based specification generation, specification analysis, the slugs synthesis wrapper that produces the raw strategy audited in Section 5.5 , and controller realization after auditing and reduction.

Proofs for the Strategy Auditor (Section 5.5 )

The auditor works directly on an explicit Mealy strategy of the kind emitted by slugs . As the main-body JSON example in Listing 2 illustrates, each JSON node is a strategy state. The variables item fixes the proposition order for the per-node state array, and trans lists the node’s successors. Each state therefore records both the environment input observed on arrival and the system output asserted there.

Proofs for State-Merging Reduction (Section 5.6 )

Throughout this appendix, let $A=(S,\delta,s_{0})$ denote the raw strategy automaton produced by slugs , where $S$ is the finite set of Mealy strategy states, $\delta\subseteq S\times S$ is the transition relation, and $s_{0}\in S$ is the initial state.

Each Mealy strategy state $s\in S$ carries labels $\mathit{in}(s)\subseteq AP_{I}$ and $\mathit{out}(s)\subseteq AP_{O}$, the environment-input valuation observed on arrival at $s$ and the system-output valuation asserted at $s$.

Proofs for State-Merging Reduction (Section 5.6 ) — Realizability Is Not Enough: Encoding, Liveness, and Auditing of Synthesized Robot Supervisors — Figure 6: Excerpt of the Two-Rivers symbolic state machine synthesized by the slugs tool, using the mealy2dot visual convention introduced in Fig. 3 (Section 3.3 ). Large circles are environment-observation states, small dots are system-activation states, green edges are env$\to$sys transitions, and red edges are sys$\to$env transitions. Only True and enumerated values are shown. The excerpt comes from the one-hot, System-Goal, no-pending configuration ( 2S ) under the alphabetic declaration ordering. In this case, states 4_sys and 7_sys can be identified to reduce the state machine size. The entire file is available with our open source release.

Coffee Demonstration

Section 6.1 summarizes the Coffee results by realizability, well-separation, strategy size, and the three headline timing rows. This appendix gives the full specification-size and BDD-node breakdown behind those summary tables, the per-configuration well-separation timing, the specification-level mechanism behind the strategy non-uniqueness noted there, and the full variable-ordering sweep.

Two-Rivers Demonstration

Section 6.2 summarizes the Two-Rivers results by realizability, well-separation, strategy size, and the three headline timing rows. This appendix gives the full specification-size and BDD-node breakdown behind that summary, the exact hand-written baseline comparison, the representative minimized well-separation cores, and the per-configuration well-separation timing.

As in Section 6.2 , Table 18 excludes both hand-written baselines to save space.

Two-Rivers Demonstration — Realizability Is Not Enough: Encoding, Liveness, and Auditing of Synthesized Robot Supervisors — Figure 8: Excerpt of the PyRoboSim P1 symbolic state machine synthesized by the slugs tool under the enumerated capability encoding, prior to reduction, using the mealy2dot visual convention introduced in Fig. 3 (Section 3.3 ). Capability activation is a single capability value under this encoding rather than a per-capability boolean, so each system state is annotated with the activated index and its name. States 22–26 show the open capability ( capability=8 ) activated at state 22. On failure (23), log_open_failed ( capability=5 ) retries by re-activating open . On success (24), the controller proceeds to move_robot ( capability=7 ), which itself retries through log_move_failed ( capability=4 ) on failure before reaching state 26.

PyRoboSim Demonstration

Section 6.3 summarizes the PyRoboSim results by realizability, well-separation, strategy size, and the headline timing rows (Section 6.3.1 for P0, Section 6.3.2 for P1).

This appendix gives the full specification-size and BDD-node breakdown behind the P0 summary tables, the exact hand-written baseline and encoding comparisons, the per-configuration well-separation timing, and the full well-separation minimized-core breakdown.

PyRoboSim Demonstration — Realizability Is Not Enough: Encoding, Liveness, and Auditing of Synthesized Robot Supervisors — Figure 9: “PiHawk” drone platform used in this case study.

Quadcopter Demonstration Results

Section 6.4 summarizes the results for the quadcopter flight supervisor by realizability, well-separation, strategy size, and the headline timing rows. This appendix gives the full specification-size and BDD-node breakdown behind that summary, the exact budget-sensitivity and well-separation timing figures, and the current status of the Fair-Outcome-with-pending ( 1FP / 2FP ) configurations.

As in the other domains, enumerated variants (2*) reduce input AP count ($84\rightarrow 2$). The counts follow from the generated specification.

Quadcopter Demonstration Results — Realizability Is Not Enough: Encoding, Liveness, and Auditing of Synthesized Robot Supervisors — Figure 10: RViz screenshot showing the layout of labeled gates in our flight space.

Declarations

Funding This work was primarily supported by United States Navy contract No. N00174-23-1-0018. Additional support was provided by the Christopher Newport University School of Engineering and Computing and the CNU Office of Research and Creative Activities. The views expressed are those of the authors. Competing interests The authors declare no competing interests.

Sources and Demonstrations

Figures are reproduced from Conner et al. See the full paper for experimental details and the project page, when the paper links one, for demonstrations and videos.