PaperlayerView exact revision on arXiv

Source-linked AI summary

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

arXiv:2609.30460v1cs.ROcs.LO

TL;DR

Robot supervisors must react to failure-prone capability outcomes, but realizability alone does not ensure designer-intended progress. This paper presents an open-source pipeline that generates, analyzes, audits, reduces, and realizes capability-based GR(1) supervisors. Across its evaluations, encoding size did not reliably predict symbolic cost, and Fair-Outcome could yield strategies that fail to ensure intended completion.

  • Problem

    Robot supervisors must handle capability failures and recovery paths, while a formally realizable strategy may still fail to ensure designer-intended task progress.

    Source: §1 · pp. 1–2

  • Method

    The open-source pipeline generates capability-based GR(1) specifications, checks well-separation, synthesizes and audits strategies, reduces states, and translates valid results into executable FlexBE HFSMs.

    Source: §7 · p. 53

  • Results

    Across the evaluated domains, enumerated encoding’s lower proposition count did not reliably predict strategy size or symbolic synthesis cost, and Fair-Outcome strategies could contain goal-unreachable traps.

    Source: §6.5 · pp. 51–52

  • Takeaways & Limitations

    Realizability and proposition count alone do not establish deployability, so the pipeline checks realized strategies for structural progress failures before controller realization.

    Source: §6.5 · p. 52, §7 · p. 53

    State merging can mask an existing goal trap because unioned arrival metadata may make a state appear more able to reach the goal, so auditing precedes reduction.

    Source: §5.6.3 · p. 33

Abstract

from arXiv · show

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.

1 Introduction

Robot supervisors must handle capability failures and recovery paths, yet formal realizability alone does not ensure designer-intended progress. This paper extends an open-source pipeline to generate, analyze, synthesize, audit, reduce, and realize executable FlexBE supervisors, then evaluates encoding and liveness choices across four case studies.

Motivation

  • Reactive supervisors must respond to reported capability failures with retries, alternatives, or safe termination, making manual design harder as recovery paths multiply.Failures can arise from conditions outside a capability’s influence, such as a closed door, camera failure, or low battery.Source: §1 · pp. 1–2

Contributions

  • The pipeline adds configurable enumerated versus one-hot encodings and Fair-Outcome versus System-Goal liveness, plus pre-synthesis analysis, strategy auditing, and state reduction.The auditor checks protocol conformance, deadlock, bounded-failure policies, and goal-unreachable traps; reduction preserves output-trace behavior and capability-level guarantees.Source: §1 · p. 3

Evaluation scope

  • The four case studies cover coffee-making, river crossing, simulated mobile-manipulation logistics, and two quadcopter platforms, comparing encodings and liveness formulations.Six domain or subdomain comparisons examine proposition count, symbolic size, synthesis time, strategy size, and task-level behavior.Source: §1 · p. 3

Study findings

  • Enumerated encoding usually improves synthesis time, but proposition-count reduction does not reliably predict strategy size or symbolic cost; Fair-Outcome can realize strategies that miss intended progress.System-Goal without pending memory is the only treatment confirmed to yield realized FlexBE HFSMs under both encodings across the reported grid.Source: §1 · p. 3

Deployment scope

  • The pipeline’s realized controllers are executable ROS 2 FlexBE HFSMs; quadcopter controllers are additionally validated in simulation and on physical hardware.Configurations with confirmed protocol or progress failures halt before realization, while well-separation is a separate, non-blocking diagnostic.Source: §1 · p. 4

2 Background

The background situates reactive synthesis among robot behavior approaches and explains the GR(1) framework used in this work. It also distinguishes specification realizability from well-separated behavior and intended progress.

2 Background

  • Robot behavior can also be generated by offline PDDL planning, but this work targets a reusable supervisor that reacts at runtime to reported capability outcomes, including failures.The demonstrated simulator includes PDDLStream task-and-motion planning for sampled action sequences.Source: §2 · p. 4

2.1 Robot System Behaviors

  • FlexBE implements behaviors as HFSMs whose Python states interface with system capabilities through ROS topics, services, and actions.Prior work has synthesized deployable controllers for FlexBE-based systems.Source: §2.1 · pp. 4–5

2.2 LTL-based State Machine Synthesis

  • GR(1) restricts specification structure for tractable synthesis; its implication-based realizability can nevertheless permit assumption-falsifying strategies or cyclic behavior that never reaches a terminal state.Well-separation diagnoses whether a strategy can force assumption violations, while this paper’s auditor checks whether a synthesized strategy structurally fails to progress.Source: §2.2 · p. 5
  • BDD-based GR(1) cost depends on constraint structure and variable interactions, so proposition count alone is not a reliable predictor of synthesis cost.The slugs implementation uses BDDs through CUDD and restricts Next usage differently for environment and system clauses.Source: §2.2 · p. 6

3 Synthesis Pipeline Overview

The pipeline turns configured robot capabilities and task goals into executable FlexBE supervisors. It models capability outcomes as environment inputs, then analyzes, synthesizes, audits, reduces, and realizes strategies.

3.1 From Capability to Executable State

  • A capability is a parameterized unit of robot functionality whose reported outcomes, including failures and timeouts, become environment inputs in the GR(1) model.The supervisor selects the capability and parameter values, and the resulting FlexBE state can be inspected and executed using ordinary FlexBE tools.Source: §3.1 · p. 7
  • A capability configuration binds each capability to its FlexBE state and specifies parameters, preconditions, outcome-driven postconditions, and required follow-on transitions.A parameter prefixed with @ is selected from an enumerated proposition in the synthesized strategy at runtime.Source: §3.1 · p. 7

3.2 Pipeline Stages

  • Startup preprocessing builds a reusable capability catalog; each synthesis request generates a specification, optionally checks well-separation, synthesizes, audits, reduces, and realizes a FlexBE HFSM or ends in failure.The reduction preserves executable behavior, and realization mechanically connects concrete FlexBE outcomes to corresponding abstract transitions.Source: §3.2 · pp. 7–8, Figure 2 · p. 8

3.3 Slugs Example

  • In the coffee-machine example, the extracted three-state Mealy strategy idles until a button input, asserts the green output, then asserts the brown output before returning to idle.The visualization splits each strategy node into an environment-observation circle and a system-activation dot; each pair maps to one FlexBE state.Source: §3.3 · pp. 9–10, Figure 3 · p. 10

4 Demonstrations

The demonstrations exercise the synthesis pipeline across a cyclic coffee-maker task, a failure-prone river crossing, simulated logistics, and quadcopter hardware. They show synthesized controllers executing in FlexBE, with state reduction and explicit handling of reported capability outcomes.

4 Demonstrations

  • The paper presents four demonstration domains and releases their code, configuration files, scripts, and raw trial data as open-source artifacts.The exact tag and experiment-data commit are listed in the paper’s availability declaration.Source: §4 · p. 10

4.1 Extended Coffee Maker Demonstration

  • The extended coffee-maker controller has no finished or failed outcomes, so it runs indefinitely by returning to button detection after brewing.The example adds a failure-prone button-detection capability to the original coffee-maker example.Source: §4.1 · p. 10

4.2 Two-Rivers Demonstration

  • Two-Rivers uses one parameterized MoveState2R capability with enumerated positions and move-item values, while the user specifies the puzzle’s safety rule rather than every GR(1) formula.The rule requires the farmer to supervise the goat whenever it is with the wolf or corn.Source: §4.2 · p. 12
  • The Two-Rivers controller safely crosses both rivers after reducing its 37-state machine to 23 states, and delivers all items despite repeated, noncontinuous injected failures.The one-hot System-Goal example identifies equivalent states; FlexBE emulates crossing failures such as high wind.Source: §4.2 · p. 12, Figure 6 · p. 14

4.3 Logistics Demonstration

  • The larger PyRoboSim logistics domain tracks six items; its custom environment constraints capture task semantics such as co-location for grasping and door conditions in P1.The controller selects which item to grab through an enumerated output rather than a fixed capability parameter.Source: §4.3 · p. 14
  • The P1 logistics specification yields a 46-state machine, reduced to 27 states before FlexBE execution; the controller opens the fridge and pantry before delivery.P1 models storage-door state, unlike P0, which abstracts doors away.Source: §4.3 · p. 14

4.4 Quadcopter Hardware-Integration Demonstration

  • On two quadcopter platforms, the synthesized supervisor coordinates trajectory planning and execution, while audited failure branches handle reported outcomes during flights.Across more than a dozen flights, most completed via the all-success branch; PiHawk pose-tracking dropouts exercised the failure branch on hardware.Source: §4.4 · p. 16
  • The quadcopter task plans five sequential trajectory segments through four gates, and only terminal ROS 2 action results trigger supervisor transitions.FlexBE polls action status without blocking, keeping the supervisor responsive to operator input.Source: §4.4 · p. 17

5 Synthesis Pipeline

The pipeline turns capability configurations and user requests into GR(1) specifications, analyzes and synthesizes them, then audits and reduces the resulting strategy before realizing it as a FlexBE controller. Its checks distinguish realizability from intended progress, and reduction preserves capability-level behavior within the core-output projection.

5.1 Preprocessing

  • Preprocessing compiles each capability configuration into a FlexBE state declaration and outcome-proposition mapping, reused to instantiate the state and wire its normalized outcome to the reduced-automaton successor.The shared mapping supports domain-specific outcome names without requiring a hand-authored transition table.Source: §5.1 · p. 20

5.2 Capability-Based Specification Generation

  • At request time, modules load selected capabilities and generate propositions and structured slugs input for the request’s initial conditions, goal, and encoding.The synthesis problem can include choices among symbolic parameter values as well as capability selection.Source: §5.2 · p. 21

5.2.1 Specifications

  • Specifications model each activation as followed by exactly one environment-reported capability outcome, permit consecutive-step retries, and require one active capability at each strategy step.Execution time within a state is abstracted away; execution limits belong to the capability or FlexBE state implementation. The generated assumptions also rule out outcomes for inactive capabilities.Source: §5.2.1 · pp. 21–23

5.2.2 Encodings

  • Enumerated encoding replaces per-capability activation and outcome propositions with a log2(|C|+1)-bit capability variable and shared outcomes, eliminating explicit mutual-exclusion constraints.A synthetic startup slot accounts for the extra value; the variable is constrained to be non-null after the initial state.Source: §5.2.2 · pp. 24, 26

5.2.3 Liveness Modeling

  • Failure-prone capabilities make base goal liveness insufficient, so the pipeline provides two alternative liveness-generation modules stated over that capability set.The base system liveness condition is the configured goal; without failure-handling liveness, an adversarial environment can return failure indefinitely and make specifications unrealizable.Source: §5.2.3 · p. 26
  • Fair-Outcome can make its environment promise depend on system-controlled retry bookkeeping, allowing assumption falsification, whereas System-Goal avoids a separate capability fairness assumption but does not guarantee terminal progress against endless failures.System-Goal’s progress reading is conditional on failure-prone capabilities eventually completing or taking an explicitly bounded recovery outcome; the paper motivates it over Fair-Outcome based on reported results.Source: §5.2.3 · pp. 27–28

5.3 Specification Analysis Module

  • Well-separation analysis runs before synthesis and reports whether the specification is well-separated or gives a non-well-separated case class, witness when available, and responsible assumptions.The analyzer emits diagnostics rather than a controller, is complementary to the auditor, and was nonfatal in the evaluated configurations.Source: §5.3 · p. 28

5.4 Synthesis

  • The synthesis wrapper compiles structuredslugs specifications for slugs, captures realizability and timing, and parses realizable strategies into YAML for downstream modules.Unrealizable requests instead terminate with a structured failure record.Source: §5.4 · pp. 28–29

5.5 Post-Synthesis Strategy Auditor

  • The post-synthesis auditor checks reachable strategies for protocol violations, deadlocks, bounded-failure violations, and goal-unreachable traps; it is not a general liveness verifier.Its checks are sound and complete for these four defined defect classes. Well-separation warns about assumption-falsifying behavior, but does not establish whether the particular extracted strategy exhibits a defect.Source: §5.5 · p. 29

5.6 Strategy State-Merging Reducer

  • State merging replaces the raw Mealy strategy before FlexBE realization, so the reduction must preserve executable capability-level behavior rather than merely simplify its representation.The formal preservation result applies to the core-output projection of the strategy passed to realization.Source: §5.6 · p. 31, §5.6.2 · p. 32

5.6.1 Core and Pending Outputs

  • Pending propositions are excluded from the reducer’s output comparison because they are synthesis bookkeeping and downstream HFSM realization does not branch on them.The reducer compares states by their nonpending core outputs, while pending bits may differ.Source: §5.6.1 · p. 31

5.6.2 The Reduction Procedure

  • The reducer preserves exactly the raw strategy’s core-output traces for the same environment input sequences, including capability activations and parameter choices.Pruning removes only states unreachable from the initial state, and each merged pair satisfies a sufficient output-trace-equivalence condition.Source: §5.6.2 · p. 32

5.6.3 What Reduction Does Not Preserve

  • Reduction does not preserve discarded pending-bit assignments, so the reduced automaton is not generally a valid assignment to the original GR(1) propositions.Only its core-output projection is meaningful under the preservation claim.Source: §5.6.3 · p. 33
  • Reduction may make configured goal labels appear more reachable, so the pipeline audits raw strategies before reduction; a post-reduction audit checks the implementation rather than establishing correctness.This limitation applies to the pipeline’s goal-label kinds, not arbitrary API goal propositions; repeating the local merge sweep to a fixed point also need not yield the smallest automaton.Source: §5.6.3 · p. 33

5.7 Controller Realization

  • Realization maps capability-selecting strategy outputs to FlexBE states using shared outcome mappings, while bootstrap, null, and terminal-bookkeeping states may be omitted or merged without changing capability-level behavior.Strategy-state counts are not necessarily realized FlexBE state counts; multiple terminal contexts can map to one FlexBE outcome.Source: §5.7 · pp. 33–34

6 Results and Discussion

This section examines how encoding and liveness choices relate to synthesis cost, strategy size, and progress across the reported comparisons, including quadcopter hardware demonstrations of synthesized supervisors. It shows that realizability and proposition count alone do not establish task-level progress or deployment suitability.

6 Results and Discussion

  • The hypotheses that enumerated encoding lowers symbolic cost and Fair-Outcome preserves intended progress wherever realizable are both rejected as stated; measurements also depend on the strategy slugs selects for a declaration order and CUDD configuration.The results characterize selected strategies, not every winning strategy admitted by a specification.Source: §6 · p. 34

6.1 Coffee Demonstration

  • Coffee configurations were realizable and produced valid FlexBE controllers, but enumerated encoding’s smaller proposition count came with slightly larger strategies, while its realizability-time advantage was clearest for extended capabilities.The extended Fair-Outcome-pending configuration was the sole case failing well-separation, although it remained realizable, auditor-valid, and executable.Source: §6.1 · p. 37

6.2 Two-Rivers Demonstration

  • In Two-Rivers, enumerated encoding reduced raw strategy size but did not uniformly reduce symbolic cost; under random orderings, its System-Goal peak BDD size increased, a reversal traced to ordering sensitivity.Fair-Outcome without pending memory was unrealizable for both encodings; pending memory restored realizability but produced the largest peak BDDs and did not fix the Fair-Outcome well-separation issue.Source: §6.2 · p. 42

6.3 PyRoboSim Demonstration

  • PyRoboSim evaluates P0 without door modeling and P1 with an added open capability and door state; P1 tests scaling rather than repeating the full sweep because per-trial synthesis cost rules that out.P0 is the baseline configuration; the two configurations are reported separately.Source: §6.3 · p. 42

6.3.1 P0: Baseline (No Door Modeling)

  • In PyRoboSim P0, Fair-Outcome without pending memory was unrealizable under both encodings across all 22 orderings, while pending propositions restored realizability but triggered GOAL_UNREACHABLE_TRAP on all 44 trials.The auditor flagged every pending Fair-Outcome trial for both encodings.Source: §6.3.1 · p. 43
  • In P0, Fair-Outcome-with-pending was realizable yet audited as a goal-unreachable trap, so the pipeline produced no executable controller.The trap shown for 2FP is a closed cycle of states 72, 73, and 83; cost metrics did not specifically signal that 2FP/3FP could not guarantee completion. System-Goal enumerated encoding was smaller and faster before reduction, but both encodings reduced to 19 states; five of seven NWS-yet-realizable configurations passed the auditor.Source: §6.3.1 · pp. 44–45, Figure 14 · p. 45

6.3.2 P1: Adding Door Modeling

  • In P1, 4FP reproduced P0’s audited goal-unreachable trap while 4F was unrealizable; the only completed one-hot run, 2S, took 25,842.0 s.This was a single fixed-ordering trial, not directly comparable with P0’s random-seed means; under that tested ordering, 2S had 8.2× the peak BDD nodes and 109.9× the realizability time of enumerated 4S.Source: §6.3.2 · pp. 46–47

6.4 Quadcopter Hardware-Integration Results

  • Across six quadcopter configurations, enumerated encoding reduced input propositions and realizability time but yielded larger extracted strategies; all 20-seed trials completed within 36,000 s.Fair-Outcome liveness was the main complexity driver, and realized FlexBE state counts could be smaller than reduced-strategy counts because terminal contexts and bootstrap states are shared or represented as wiring.Source: Table 13 · p. 48, §6.4 · pp. 48–49

6.4.1 Budget Sensitivity of One-Hot Synthesis

  • Enumerated encoding completed all 20 orderings at 900 s, while one-hot 1F required 3,600 s and 1SP 36,000 s; both Fair-Outcome-with-pending variants were realizable but audited as traps.One-hot 1FP resolved within the 24-hour budget; enumerated 2FP resolved on the faster machine in 16.6 hours, and its raw-strategy audit found the same trap.Source: §6.4.1 · p. 49

6.4.2 Well-Separation

  • Six quadcopter configurations were well-separated across all 22 orderings, whereas 1FP and 2FP were non-well-separated and both exhibited goal-unreachable traps.For these configurations, the specification-level violation signature was confirmed by the extracted strategies.Source: §6.4.2 · pp. 49–50

6.4.3 Hardware Execution and Failure-Handling Validation

  • The synthesized 1S supervisor flew on Crazyflie and PiHawk, and repeated PiHawk pose dropouts triggered the intended failure logging and land-disarm behavior.Simulation forced-outcome tests also checked recovery transitions; flights were exploratory rather than a statistically powered reliability study, and hardware evidence validates integration with robot software, not end-to-end formal correctness.Source: §6.4.3 · pp. 50–51

6.5 Summary

  • Across domains, enumerated encoding's lower proposition count did not predict strategy size or symbolic cost; synthesis-cost effects varied, with savings in PyRoboSim and the quadcopter case study.System-Goal liveness was preferred on synthesis cost and reliability; Fair-Outcome increased difficulty in the main realizable pending comparisons, most dramatically for quadcopters, but not uniformly in every case.Source: §6.5 · p. 51
  • Fair-Outcome-with-pending strategies exhibited cyclic retry structures and goal-unreachable traps in PyRoboSim and at quadcopter hardware scale, in both encodings.These failures show that formal realizability alone does not establish designer-intended terminal progress.Source: §6.5 · pp. 51–52
  • System-Goal without pending memory was the only formulation confirmed to yield a realized FlexBE HFSM across all six comparisons under both encodings; Fair-Outcome without pending failed in Two-Rivers and both PyRoboSim configurations.Where Fair-Outcome did realize, System-Goal produced shorter realizability times except in Coffee’s flat sub-millisecond base cases, where timing differences were statistically indistinguishable.Source: Table 14 · p. 52, §6.5 · pp. 52–53
  • Every goal-unreachable-trap audit failure occurred in a non-well-separated specification, but several non-well-separated specifications still produced auditor-valid strategies realized as FlexBE HFSMs.The pipeline checks well-separation before synthesis and audits extracted strategies afterward; whether all such traps arise from non-well-separated specifications remains open.Source: §6.5 · p. 52
  • Enumerated was no slower than one-hot on realizability time in five of six System-Goal/no-pending comparisons, while the winning encoding varied across comparisons.Under fixed declaration order, enumerated was also smaller and faster on Two-Rivers; reduced-strategy sizes matched across encodings only in Two-Rivers and the two PyRoboSim models.Source: §6.5 · p. 52
  • In Crazyflie, pending memory destabilized one-hot synthesis time by two orders of magnitude: 1S took 19.7 s versus 2764.5 s for 1SP.System-Goal with pending memory was not established across the full grid because its one-hot PyRoboSim P1 configuration did not finish within the 10 h budget, which is not evidence of unrealizability.Source: §6.5 · pp. 52–53
  • System-Goal avoids the observed Fair-Outcome retry pathology, but neither formulation can force progress when a capability fails forever; this empirical preference is specific to the studied model.Specification evaluation should consider symbolic synthesis cost, operational validity of environment assumptions, and extracted-strategy progress in addition to realizability and proposition count.Source: §6.5 · p. 53

7 Conclusion

The conclusion argues that realizability alone is insufficient: encoding and liveness choices affect synthesis and task progress, while the pipeline checks specific deployability defects. The appendix formalizes the auditor’s state model, trap classification, and complexity.

7 Conclusion

  • The open-source pipeline spans capability-based GR(1) specification through executable FlexBE HFSM generation; state merging preserves output-trace equivalence, while translation is validated empirically.The translation validation uses forced-outcome simulation and hardware tests, not the reduction proof.Source: §7 · pp. 53–54
  • For the tested slugs/CUDD backend, enumerated encoding usually synthesizes faster, while System-Goal without pending memory is the only formulation confirmed realized under both encodings across the comparison grid.The authors recommend this pairing and auditing every realized state machine; proposition count does not reliably predict controller size or symbolic cost.Source: §7 · pp. 53–54
  • The authors identify backend-specific encoding effects as an open question and call for comparisons with other synthesizers and specification-guidance methods.They also propose detecting reachable cycles with available but unused exits toward the goal.Source: §7 · p. 54

A.1 Semantic Model

  • The auditor’s product state tracks the pending capability and consecutive-failure counters, updating them from capability activations and reported outcomes.Unbounded capabilities require no counter; all reported experiments use that setting.Source: §A.1 · p. 55
  • With completed reachable-product exploration, the auditor reports exactly reachable strict protocol violations, bounded-failure violations, and deadlocks.The product monitor checks capability activations and outcomes before extending transitions; multiple activations make the pending capability ambiguous.Source: §A.1 · pp. 55–56
  • A goal-unreachable trap is a reachable cyclic component with no path to a cyclic goal-containing component; conversely, a reachable goal-unreachable node implies such a trap when the strategy is deadlock-free.An SCC with a path to a cyclic goal component is not flagged, even if the environment could avoid that path indefinitely.Source: §A.1 · pp. 56–57

A.2 Practical Classification and an Example

  • The practical classifier uses Tarjan SCCs and backward reachability from cyclic goal components, flagging exactly the unmarked reachable cyclic components.This is sound and complete relative to the paper’s trap definition, following the deadlock check.Source: §A.2 · p. 57

A.3 Complexity

  • Audit complexity is O((n + m)(k+1)B); no evaluated configuration has finite failure bounds, so B = 1 and the reported bound is O((n + m)(k+1)).Finite-bound counters can make B grow exponentially; measured audit times include Python-harness and subprocess overhead.Source: §A.3 · pp. 57–58

A.4 Pipeline Integration

Pipeline integration distinguishes incomplete audits from confirmed results, keeps well-separation separate from strategy auditing, and checks the reduced automaton after state merging.

A.4 Pipeline Integration

  • An audit budget overrun returns AUDIT_INCOMPLETE, an unknown result rather than a pass or failure; deployment should normally treat it as fatal.A confirmed pass permits deployment with respect to the defined defect classes, while a confirmed failure rejects the strategy.Source: §A.4 · p. 58
  • Well-separation is a specification-level status distinct from realizability and the verdict on a particular extracted strategy; some NWS strategies still pass the audit.A different synthesis ordering could produce a strategy that exploits the same NWS specification, so the audit guarantee applies to the concrete strategy examined.Source: §A.4 · p. 58
  • A second audit after state merging checks that reduction introduced no new deadlocks or goal-unreachable traps for the configured goal labels.Strict protocol checks are skipped on reduced states because merged input-label metadata no longer represents a single concrete outcome observation.Source: §A.4 · p. 58
  • The completed auditor exhaustively checks every reachable strategy state and transition, while forced-outcome tests confirm that selected running HFSM transitions match audited behavior.Reported raw strategies range up to 677 states; execution tests manually force all declared capability-failure outcomes in Coffee and Two-Rivers, and selected outcomes in PyRoboSim and quadcopter tests.Source: §A.4 · p. 59

Appendix B Proofs for State-Merging Reduction (Section 5.6)

The reducer prunes unreachable states, then merges states with matching core outputs and input-indexed successors. Proofs show that this preserves executable capability behavior, while the guarantee does not extend to pending propositions or the generated FlexBE translation.

Appendix B Proofs for State-Merging Reduction (Section 5.6)

  • The merge test requires equal core outputs and identical input-indexed successor maps; each merge redirects targets while preserving exact input keys.The reducer repeats configured merge sweeps to a fixed point.Source: Appendix B · pp. 59–60
  • Pruning removes noninitial states that become zero-indegree, and no state on a path from the initial state is removed.The procedure is sound but may leave unreachable cycles that retain incoming edges from within those cycles.Source: Appendix B · pp. 59–60
  • The quotient invariant preserves available input keys and maps each reduced transition to the representative of its raw successor, supporting the merge-soundness proof.Every performed merge joins states that are output-trace equivalent in the original automaton.Source: Appendix B · p. 61
  • The reduced automaton preserves admissible environment-input sequences and identical core-output traces, hence the same capability activations and parameter choices.The guarantee applies to the reduced automaton, not directly to the FlexBE HFSM produced by translation.Source: Appendix B · p. 62
  • The reduction preserves capability-level consequences of a winning raw strategy, but not its full GR(1) proposition valuation or system-transition constraints.Pending propositions are discarded from the core-output projection used by the guarantee.Source: Appendix B · pp. 59, 62

B.1 What Reduction Does Not Preserve

Reduction preserves forward executable behavior, not every property of the raw strategy. In particular, pending propositions and some incoming-label information are not preserved, constraining which checks and guarantees apply after reduction.

B.1 What Reduction Does Not Preserve

  • The reduction theorem concerns forward behavior from a state and makes no claim about how a merged state was reached.Its output-trace equivalence matches admissible input sequences and core-output traces going forward.Source: §B.1 · p. 62
  • Merged states retain one representative’s pending-output valuation, so the reduced automaton is not generally a strategy over the full original GR(1) valuation.Core outputs are preserved exactly, while pending propositions are excluded from that projection.Source: §B.1 · p. 62
  • Unioned incoming-label metadata can include outcomes no single raw predecessor observed, so strict per-edge protocol monitoring cannot be applied unmodified after reduction.This restriction follows because the equivalence relation does not preserve backward arrival context.Source: §B.1 · pp. 62–63
  • For the pipeline’s goal-label types, reduction cannot create a goal-unreachable trap absent from the raw automaton, though it can mask an existing trap.The deployed pipeline audits the raw strategy first and reduces only a trap-free one; the post-reduction audit is a regression check.Source: §B.1 · p. 63
  • The fixed-point merge test need not produce the coarsest quotient, limiting compactness rather than correctness.The reported experiments found no further reductions beyond the first productive merge sweep.Source: §B.1 · p. 63

Appendix C Coffee Demonstration

The Coffee results show distinct trade-offs among encoding, liveness, and strategy choice. Well-separation diagnoses an assumption issue separately from realizability and controller usability, while ordering can select among different valid strategies.

Appendix C Coffee Demonstration

  • Enumerated encoding is leaner in symbolic size, but its strategy sizes are larger; the largest BDD footprints and realizability times occur for extended Fair-Outcome with pending memory.The reported maximum is 3193.8 peak nodes and 6.316 ms realizability for one-hot 3FP.Source: Appendix C · p. 64
  • All Coffee specifications are realizable and audited strategies pass, but extended Fair-Outcome with pending memory is not well-separated under either encoding.Minimized cores identify the grind-completion environment liveness assumption as the source; the check is a specification diagnostic, not a verdict that synthesis failed.Source: Appendix C · p. 64
  • Well-separation check times are sub-millisecond throughout, and the apparent 3FP timing increase is not evidence for its non-separation verdict.For enumerated encoding, 3FP’s 0.086 ms versus 0.041–0.077 ms elsewhere falls within observed run-to-run variation.Source: Appendix C · p. 64
  • Among 40 one-hot base-capability orderings, 22 yielded a four-state cycle and 18 a five-state strategy with a redundant repeated activation.The specification permits both; reduction leaves the strategies at three and four states, respectively, while enumerated 2S reports a strategy size of 6.Source: Appendix C · p. 64

C.1 Variable-Ordering Robustness

The Coffee ordering sweep finds that sensitivity is concentrated in extended configurations, especially one-hot cases with Fair-Outcome and pending memory. An explicit CUDD threshold largely removes initial-order effects where they occur.

C.1 Variable-Ordering Robustness

  • The sweep covered 7,140 Coffee synthesis trials across 16 configurations and a hand-written baseline, 42 declaration orderings, two reordering settings, and five repeats, with zero failures.The default CUDD trigger is 4,004 live nodes, above peak allocation in about 95% of Coffee trials; the authors note this is specific to Coffee’s small BDDs.Source: §C.1 · p. 65
  • With threshold 250 enabled, peak BDD nodes in extended one-hot pending cases become nearly independent of declaration order.For Fair-Outcome pending, the random-order mean falls from 7000.7 without reordering to 3193.8 with the threshold; fixed-order results are 6132 and 3066, respectively.Source: §C.1 · p. 65, Table C3 · p. 68
  • Sensitivity is concentrated rather than general: all basic configurations and the hand-written baseline are flat at 1022 peak nodes, while extended enumerated Fair-Outcome pending also varies.The latter ranges from 3066 for fixed orderings to 3014.9 for random orderings without reordering, and falls to 2044 with the threshold.Source: §C.1 · p. 65
  • For this capability model, the authors favor an explicit CUDD threshold over hand-tuned declaration order where ordering sensitivity occurs.Default automatic reordering did not trigger at these Coffee BDD sizes; the authors point to Fair-Outcome with pending memory as a pattern associated with sensitivity.Source: §C.1 · p. 65

Appendix D Two-Rivers Demonstration

Two-Rivers results show that encoding and liveness choices affect symbolic cost and realizability differently, while well-separation diagnoses Fair-Outcome assumption hazards that pending memory does not remove.

Appendix D Two-Rivers Demonstration

  • Both hand-written baselines are realizable, well-separated, and produce valid FlexBE HFSMs across 40 random orderings, with reduced size 22 versus 23 for capability-generated 2S/3S.Their mean realizability times are 0.086–0.102 s and peak BDD sizes 17,195–23,685 nodes, in the same order of magnitude as 2S/3S.Source: Appendix D · p. 69
  • Enumerated encoding lowers proposition counts and raw strategy sizes, but does not uniformly lower symbolic synthesis cost; System-Goal encoding comparisons reverse under random ordering.Under System-Goal, mean peak BDD size is higher for enumerated encoding in both no-pending and pending pairs; the gaps are within one standard deviation for realizability time.Source: Appendix D · p. 69
  • Every Fair-Outcome specification is non-well-separated, while all System-Goal specifications are well-separated; pending memory restores Fair-Outcome realizability but not well-separation.The 2FP/3FP configurations yield auditor-valid controllers despite remaining non-well-separated; 2F/3F are unrealizable.Source: Appendix D · p. 69
  • Well-separation checks take 6.22–9.88 ms across eight columns, remaining under 1% of Overall time in five columns but reaching 5.15% and 6.83% for unrealizable 2F/3F.Check time does not track well-separation status cleanly: 3F is the slowest non-well-separated case, while 3SP is the fastest well-separated case.Source: Appendix D · p. 69

D.1 Variable-Ordering Sensitivity

In Two-Rivers, the apparent encoding winner depends on declaration ordering: enumerated encoding wins under both tested fixed orders, but random-order means reverse that comparison. The appendix also reports distributional evidence and a tentative mechanism for the asymmetry.

D.1 Variable-Ordering Sensitivity

  • Random ordering can flip which encoding is faster: enumerated’s compact encoding is advantageous only under favorable variable orderings, while one-hot performance stays roughly flat across orderings.The asymmetry is distinct from Coffee’s ordering-magnitude sensitivity, where reordering changes absolute BDD size but not the winning encoding.Source: §D.1 · p. 70
  • A possible asymmetry mechanism is that randomization leaves enumerated’s high-fanout capability declaration fixed while shuffling other declarations, but the BDD variable-index assignment has not confirmed this explanation.The pipeline writes the capability declaration first in the output block; the authors present this as a plausible mechanism, not a demonstrated cause.Source: §D.1 · p. 70
  • Under both fixed declaration orderings, enumerated encoding is about 18–24% faster and 23% smaller; the random-seed reversal is specific to the mean, not a general domain property.Table D5 compares fixed alphabetic and domain-grouped trials with the random-order mean.Source: §D.1 · p. 70, Table D5 · p. 72
  • Even after removing the slowest 20% of enumerated trials, mean realizability time is 72.6 ms versus one-hot’s unfiltered 53.8 ms; 85 of 200 enumerated trials exceed one-hot’s worst trial.Table D7 summarizes the trimmed means; Table D6 covers the underlying 200-trial distribution.Source: §D.1 · p. 70, Table D7 · p. 72, Table D6 · p. 72

Appendix E PyRoboSim Demonstration

  • The PyRoboSim appendix provides full specification-size and BDD-node breakdowns, hand-written baseline and encoding comparisons, well-separation timing, and minimized-core details.The referenced summary covers PyRoboSim results by realizability, well-separation, strategy size, and headline timing rows.Source: Appendix E · p. 73

E.1 P0: Baseline (No Door Modeling)

PyRoboSim P0 shows that synthesis cost and proposition counts do not establish whether a strategy is deployable: Fair-Outcome-with-pending strategies are realizable but fail the auditor’s goal-progress check, while System-Goal strategies pass it.

E.1 P0: Baseline (No Door Modeling)

  • All 44 Fair-Outcome-with-pending trials trigger GOAL_UNREACHABLE_TRAP, and the pipeline produces no executable FlexBE controller for either encoding.The raw-strategy audit confirms the defect; the pipeline halts before state reduction.Source: §E.1 · p. 73
  • Fair-Outcome-with-pending costs do not clearly signal the defect: one-hot has fewer peak BDD nodes than 2S but takes longer, while enumerated 3FP is larger and slower than 3S.Raw extracted strategies are also larger for 2FP/3FP, but neither proposition count nor symbolic-cost metrics specifically signals that task completion is not guaranteed.Source: §E.1 · p. 73
  • System-Goal strategies 2S and 3S both reduce to 19 states, despite their differing pre-reduction sizes and encoding costs.This convergence is not universal: the paper notes that Coffee and quadcopter reduced sizes differ across encodings.Source: §E.1 · p. 73
  • For System-Goal P0, enumerated encoding averages 3,278,524.9 peak BDD nodes and 149.4 s realizability time, versus 5,102,846.0 nodes and 449.2 s for one-hot.Table E8 reports means over 20 random-seed declaration orderings under a CUDD reordering threshold of 250.Source: §E.1 · p. 73, Table E8 · p. 74
  • The hand-written Full baseline is faster than 2S under fixed orderings, but its 20-seed mean is slowest among System-Goal configurations and has a 399.5 s standard deviation.Its random-seed mean is 570.2 s, compared with 449.2 s for 2S and 149.4 s for 3S.Source: §E.1 · p. 74
  • MoveOnly averages 0.016 s realizability and 3,832.5 peak BDD nodes, serving as a sanity check that item-manipulation logic accounts for most symbolic cost rather than navigation.MoveOnly tracks only robot location and the finished flag.Source: §E.1 · p. 75
  • For the non-well-separated P0 configurations 2S/3S/2F/3F/2SP/3SP, one environment safety assumption suffices as a minimized witness; pending Fair-Outcome shifts the witness to liveness assumptions.The minimized cores are stable across declaration orderings; 2FP/3FP also fail the auditor with goal-unreachable traps.Source: §E.1 · p. 75
  • Among P0 configurations, only MoveOnly is well-separated; nevertheless, five other non-well-separated yet realizable configurations pass the auditor cleanly.The 2FP/3FP exceptions also have goal-unreachable traps, and all auditor-found goal-unreachable traps arose from non-well-separated specifications.Source: §E.1 · p. 75

E.2 P1: Adding Door Modeling

Adding door modeling to PyRoboSim raises synthesis costs, while auditor and declaration-ordering results expose limits that single-trial encoding comparisons miss. The quadcopter appendix reports a different encoding pattern: enumerated is faster but can yield larger strategies.

E.2 P1: Adding Door Modeling

  • Fair-Outcome without pending memory is unrealizable in P1, while 4FP is realizable at 12919.4 s but triggers the same goal-unreachable trap as P0 and Two-Rivers.The audit halts before reduction, so no executable FlexBE controller is produced for 4FP.Source: §E.2 · p. 76
  • FullP1 synthesis completes in 3871.9 s, but its well-separation check times out at 43,200 s, showing that the diagnostic can remain unresolved when synthesis completes.The timeout was reproduced on the faster machine.Source: §E.2 · p. 76
  • After door modeling, under the tested P1 ordering, one-hot 2S has 8.2× the peak BDD nodes and 109.9× the realizability time of enumerated 4S; both reduce to 27 states.Source: §E.2 · p. 76
  • The P1 main table is exploratory: it reports single alphabetic-ordering trials, not random-seed means, and one-hot 2S is the only one-hot configuration completed within the 10-hour budget.The remaining one-hot configurations have no completed run at that budget.Source: §E.2 · pp. 75–76, Table E9 · p. 77

E.3 Declaration-Ordering Sensitivity (4S/4F)

  • On the same alphabetic ordering, threshold-250 reordering makes 4S 15.6× slower and 4.6× larger than uncapped reordering, while 4F is 1.3× faster with about 5% more nodes.The impact of reordering policy depends on configuration; one-hot 2S has no threshold-250 run for comparison.Source: §E.3 · p. 78
  • Across 22 orderings, 4S’s mean realizability time is 9164.0 s with a 7629.1 s standard deviation, while 4F takes 20.2–76.2 s; qualitative outcomes remain unchanged.4S is realizable, audit-valid, and reduces to 27 states in all trials; 4F is unrealizable in all trials.Source: §E.3 · p. 78

Appendix F Quadcopter Demonstration Results

  • In the quadcopter results, enumerated encoding reduces input proposition count from 84 to 2 but does not reduce extracted or reduced strategy size; it is faster in all three comparable realizability pairs.For System-Goal, realizability time is 19.7 to 9.3 s for one-hot versus enumerated; Fair-Outcome is the main complexity driver within each encoding.Source: Appendix F · p. 79

F.1 Reduced Strategy Size versus Realized HFSM Size

Reduced-strategy states do not map one-to-one to FlexBE HFSM states: terminal and bootstrap contexts can become shared outcomes or wiring rather than executable states. The reported count gaps were checked against generated artifacts and do not indicate lost robot behavior.

F.1 Reduced Strategy Size versus Realized HFSM Size

  • The largest reported gaps—106 reduced states versus 54 realized HFSM states for 2S, and 318 versus 89 for 2SP—do not indicate lost robot behavior.Generated artifacts showed that non-realized reduced states were terminal or bootstrap/null contexts; retained capability values in terminal failed contexts are symbolic context, not additional actions.Source: §F.1 · p. 79
  • Auditing takes 6–18 ms across Table F11’s columns, even as |Slugs SM| reaches 347 for 2SP.The cited comparison notes strategies of 559 states for PyRoboSim’s hand-written FullP1 baseline and 677 states for this domain’s enumerated 2FP raw strategy.Source: §F.1 · pp. 79, 81
  • Terminal and bootstrap contexts project to root-container wiring or shared FlexBE outcomes, while executable action states are preserved.Thus reduced-strategy state counts and realized HFSM state-instantiation counts measure different things.Source: §F.1 · p. 79, Table F12 · p. 81

F.2 Budget Sensitivity of One-Hot Synthesis

The quadcopter results show budget sensitivity across one-hot declaration orders, and Fair-Outcome-with-pending configurations exhibit both well-separation and strategy-audit failures. The flight-tested configurations synthesized quickly on the deployment hardware and were flown.

F.2 Budget Sensitivity of One-Hot Synthesis

  • Enumerated encoding completed all 20 orderings at every tested budget, while one-hot 1SP required 36,000 s for 100% completion and one trial reached 12,558 s realizability time.One-hot 1F reached 100% completion at 3,600 s; 1SP needed ten times that budget to fully resolve.Source: §F.2 · p. 81
  • One-hot 1FP was realizable in 33,937 s but failed the GOAL_UNREACHABLE_TRAP audit and was not realized as a FlexBE HFSM.Enumerated 2FP resolved on faster hardware in 59,674 s, but its extracted strategy failed the same audit; it did not resolve on the original machine within 24 h.Source: §F.2 · pp. 81–82

F.3 Well-Separation

  • Both 1FP and 2FP were NON_WELL_SEPARATED, with P-all/E-just cases implicating environment-liveness assumptions.The 2FP well-separation check resolved even though its realizability remained unresolved on that machine within the 24 h synthesis budget.Source: §F.3 · p. 82

F.4 Hardware Failure-Handling Validation

  • On the deployment hardware, 1S and 2S synthesized end-to-end in 10.6 s and 10.5 s, respectively, and both configurations were flight-tested.The timing rows were from a faster machine and are not directly comparable to the other domains’ reported sweeps.Source: §F.4 · pp. 82–83
Loading 2609.30460v1…