cs.ROSep 24, 2026

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

Authors: David C. Conner, Joshua Luzier, William J. Doyle, Emma R. Faith, Aubrie B. Kooiker, Andrew J. Farney, Sebastian Fox, Evangelina Grimes, +2 more

Organizations: Capable Humanitarian Robotics and Intelligent Systems Lab (CHRISLab) School of Engineering and Computing, Christopher Newport University Newport News, Virginia, 23606, USA.

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

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.

Figures & tables

Figure 1: “PiHawk” drone flying under supervisory control of synthesized state machine in our indoor flight space.
TermForm
Environment
φia\varphi_{i}^{a}ψ:API\psi:AP_{I} with ∧,∨,¬\land,\lor,\neg only
φsa\varphi_{s}^{a}Gψ:API∪APO∪{Xy:y∈API}G\psi:AP_{I}\cup AP_{O}\cup\left\{Xy:y\in AP_{I}\right\}
φla\varphi_{l}^{a}GFψ:API∪APO∪{Xy:y∈API∪APO}GF\psi:AP_{I}\cup AP_{O}\cup\left\{Xy:y\in AP_{I}\cup AP_{O}\right\}
System
φig\varphi_{i}^{g}ψ:API∪APO\psi:AP_{I}\cup AP_{O} with ∧,∨,¬\land,\lor,\neg only
Table 1: Slugs Specification Structure
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.
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.
Figure 4: The realized FlexBE state machine for the extended coffee-maker example.
Figure 5: In this variation of the classic logic puzzle, the farmer must cross two rivers without leaving the goat unsupervised with either the corn or the wolf. This image shows a screenshot during execution of the synthesized state machine in FlexBE. (visualization adapted from Luzier and Conner (2024) )
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.
Figure 7: A simulated execution of the P1 configuration, which models storage-door state. In the initial state (left), butter0 is in the fridge and bread0 in the pantry, both closed, among the four other tracked items placed throughout the world. The synthesized controller opens both containers and delivers the two items to the dining table (right). The principal synthesis comparison of Section 6.3.1 uses the P0 configuration, which abstracts doors away, and Section 6.3.2 reports this door-modeling P1 configuration.
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.
Figure 10
Figure 11: The screenshot (top) shows FlexBE execution using collaborative autonomy to solicit operator approval before executing the planned trajectory on a Crazyflie nanocopter (bottom).
τ\taugr_aoutcome observedgr_prule
0F—F(initial)
1T (activate)—Tconjunct 1
2Fgr_f (failure)Tconjunct 2
3T (retry)—Tconjunct 1
4Fgr_c (completed)Fconjunct 3
5F—Fconjunct 4
Table 2: A six-step gr_a / gr_c / gr_f / gr_p trace of ( 4 ) for the Coffee gr capability. Each gr_p value is annotated with the conjunct of ( 4 ) that determines it.
QuestionWell-separation / assumption-falsification analysisPost-synthesis strategy auditor
Artifact checkedThe GR(1) specification and game before synthesis.The extracted Mealy strategy after synthesis.
Main failure exposedWhether the specification lets the system win by falsifying or depending on environment assumptions, including broader game-level fairness hazards.Whether the concrete strategy violates the activation–outcome protocol or enters a reachable cyclic region from which the configured goal is structurally unreachable.
What it catches in our examplesThe specification-level source of the Fair-Outcome retry hazard; that is, progress can depend on assumptions about future outcomes that the controller does not force.The realized symptom in the generated controller; that is, pending-without-activation cycles in which no completion outcome can occur and the task goal is cut off.
What it does not certifyThat a particular extracted or reduced strategy obeys the FlexBE capability protocol, respects bounded-failure counters, or remains free of concrete strategy-level traps.That every possible livelock has been excluded. SCCs with an available but unforced exit to a goal remain a game- or fairness-aware analysis problem.
BenefitDiagnoses the modeling weakness before committing to a controller.Validates the actual artifact that the pipeline will execute.
Table 3: Complementary roles of specification-level well-separation and the post-synthesis strategy auditor for the retry-liveness pathology studied in this paper.
DomainGoal condition ggInterpretation
Coffeebr_cRecurring successful brew completion in a controller designed to run forever.
Two-RiversfinishedSuccessful terminal output after all entities reach the far bank.
PyRoboSim P0/P1finishedSuccessful terminal output after the delivery task is complete.
Quadcopterfinished ∨\lor failedProgrammed terminal output; the audit certifies reachability of termination, not mission success alone.
Table 4: Configured goal condition gg (Section 5.2.3 ) supplied to the post-synthesis strategy auditor for each domain.
FactorLevels tested
Capability encodingOne-hot (Section 5.2.2 ) and enumerated (Section 5.2.2 )
Liveness formulationSystem-Goal (Section 5.2.3 ) and Fair-Outcome (Section 5.2.3 )
Pending memoryWithout or with a persistent proposition tracking whether a completion is still owed (Section 5.2.1 )
ComparisonsCoffee base and extended capability sets (Section 6.1 ), Two-Rivers (Section 6.2 ), PyRoboSim P0 without door modeling (Section 6.3.1 ), PyRoboSim P1 with door modeling (Section 6.3.2 ), and Crazyflie/PiHawk hardware (Section 6.4 )
Declaration orderingFixed alphabetic, fixed capability-grouped (“domain-grouped”), and NN random-seed orderings ( N=40N=40 for Coffee/Two-Rivers and N=20N=20 for PyRoboSim P0/Crazyflie). Each random seed shuffles the input declarations and the output declarations, except that the enumerated encoding’s shared capability declaration is always written first in the output block. PyRoboSim P1’s main table reports single fixed-ordering trials; Appendix 12.3 adds a 20-random-seed sweep for 4S / 4F .
CUDD reordering policyThreshold 250 for the principal experiment grid unless otherwise noted. PyRoboSim P1’s original single-ordering tables (Table 12 , Table 23 ) use the P1 configuration’s uncapped (“auto”) policy; Appendix 12.3 separately reports threshold-250 P1 ordering experiments for 4S / 4F .
Table 5: Experimental design factors compared across all six domain/subdomain comparisons (Section 4 ). Crossing encoding ×\times liveness ×\times pending gives up to eight named configurations per comparison, labeled by encoding digit ( 1 / 2 / 3 / 4 ), liveness letter ( S / F ), and an optional P suffix for pending memory, following this section’s naming convention. Not every combination is realizable or attempted in every domain, and each domain additionally reports one or two hand-written baselines outside this grid.
RowWhat It MeasuresTiming Source
Generate SpecsBuilding the GR(1) specification from the request’s capability subset (Section 3.2 ).Python harness
Well-SeparationAssumption-falsification check on the compiled specification (Section 5.3 ), a separate slugs invocation.slugs -internal
RealizabilityThe Synthesis time reported by slugs , the GR(1) fixed-point computation that decides realizability and, when realizable, yields the symbolic winning strategy as a byproduct rather than a separate pass.slugs -internal
ExtractionThe subsequent walk converting the symbolic strategy into the explicit Mealy machine slugs returns. Realizable rows only.slugs -internal
AuditingThe post-synthesis auditor’s pass over the extracted machine (Section 5.5 ).Python harness
Realize HFSMTranslating the reduced strategy into an executable FlexBE HFSM and generating its initial GUI layout (Section 3.2 ).Python harness
Table 6: The seven timing rows reported for every synthesis configuration in Section 6 , in pipeline order. Well-Separation , Realizability , and Extraction are internally reported times from slugs . The remaining four are Python pipeline-harness wall-clock measurements and so include interpreter and subprocess start-up overhead the three slugs -internal rows do not.
 12S3S2F3F2SP3SP2FP3FP
Well SeparatedYesYesYesYesYesYesYesYesNo
RealizableYesYesYesYesYesYesYesYesYes
FlexBE HFSM RealizedYesYesYesYesYesYesYesYesYes
∣API∣\left|AP_{I}\right|436363636
∣APO∣\left|AP_{O}\right|335353838
|Slugs SM|74.574.574.574.57
Table 7: [ N=40N=40 random-seed orderings.] Coffee synthesis results with one-hot labeling. Reported values are the mean over 40 random declaration orderings under a CUDD reordering threshold of 250. Integer-valued count means indicate identical samples, while non-identical count means are shown with one decimal digit, with a companion row giving ±\pm one standard deviation wherever the underlying trials disagree. Column 1 is the hand-written baseline. The leading digit 2 / 3 denotes the base/extended capability set, S / F denotes System-Goal/Fair-Outcome liveness, and P adds pending propositions.
 2S3S2F3F2SP3SP2FP3FP
Well SeparatedYesYesYesYesYesYesYesNo
RealizableYesYesYesYesYesYesYesYes
FlexBE HFSM RealizedYesYesYesYesYesYesYesYes
∣API∣\left|AP_{I}\right|22222222
∣APO∣\left|AP_{O}\right|24242727
|Slugs SM|68686868
Table 8: [ N=40N=40 random-seed orderings.] Coffee synthesis results with the enumerated capability encoding (same reporting convention and column legend as Table 7 ). The enumerated encoding has no hand-written baseline, so column 1 is omitted.
Figure 12: The extended Coffee example’s raw synthesized Mealy strategy and its state-merged reduction (Section 5.6 ), using the mealy2dot visual convention introduced in Fig. 3 (Section 3.3 ). Each of the three capabilities’ fail outcome ( bd_f , gr_f , br_f ) loops back to re-activate the same capability rather than advancing, so the raw strategy repeats the same activation–fail–reactivate pattern at three points in its cycle. Reduction collapses each of those points to a single state carrying its own self-loop, leaving exactly the three states realized as the executable FlexBE state machine in Fig. 4 . This one-hot extended-capability, System-Goal, no-pending configuration reduces from 7 to 3 states identically across all 40 declaration orderings ( 3S in Table 7 ) – unlike the smaller non-uniqueness case discussed below, this reduction is deterministic.
Figure 13: Representative symbolic (raw, pre-reduction) and reduced Mealy graphs for the two strategy shapes discussed above, both from the one-hot 2S configuration, using the mealy2dot visual convention introduced in Fig. 3 (Section 3.3 ). In the top pair, runs in which gr_a is not declared first among the output propositions yield the direct four-state cycle, which state-merging reduces to three states. In the bottom pair, declaring gr_a first yields a fifth, redundant bd re-activation state before grinding. This extra state survives reduction, leaving four states rather than three. Both reduced strategies are valid and executable for the identical specification.
 2S3S2F3F2SP3SP2FP3FP
Well SeparatedYesYesNoNoYesYesNoNo
RealizableYesYesNoNoYesYesYesYes
FlexBE HFSM RealizedYesYesNoNoYesYesYesYes
∣API∣\left|AP_{I}\right|1310131013101310
∣APO∣\left|AP_{O}\right|108108119119
|Slugs SM|3726––37263726
Table 9: [ N=40N=40 random-seed orderings.] Two-Rivers synthesis results. Reported values are means over 40 random declaration orderings under a CUDD reordering threshold of 250 ( N=200N=200 trials per column, 40 orderings ×\times 5 repeats). Integer-valued count means indicate identical samples, while non-identical count means are shown with one decimal digit, with a companion row giving ±\pm one standard deviation wherever the underlying trials disagree. Columns marked unrealizable have no extracted strategy.
 Full2S2F2SP2FP
Well SeparatedNoNoNoNoNo
RealizableYesYesNoYesYes
FlexBE HFSM RealizedYesYesNoYesNo
∣API∣\left|AP_{I}\right|3334343434
∣APO∣\left|AP_{O}\right|1617172020
|Slugs SM|11647–47108
Table 10: [ N=20N=20 random-seed orderings.] PyRoboSim P0 synthesis results, full hand-written baseline and one-hot capability encoding. Full is the hand-written baseline shown here (item 1b above); the MoveOnly sanity-check baseline (item 1a above) appears in Table 22 . The leading digit 2 denotes the one-hot capability encoding (item 2). S / F denotes System-Goal/Fair-Outcome liveness, and P adds pending propositions. Reported values are means over 20 random-seed declaration orderings under a CUDD reordering threshold of 250, with a companion row giving ±\pm one standard deviation wherever the underlying trials disagree. Columns marked unrealizable have no extracted strategy. 2FP is realizable but shows FlexBE HFSM Realized: No because the post-synthesis auditor (Section 5.5 ) halts the pipeline before reduction, discussed below.
 3S3F3SP3FP
Well SeparatedNoNoNoNo
RealizableYesNoYesYes
FlexBE HFSM RealizedYesNoYesNo
∣API∣\left|AP_{I}\right|25252525
∣APO∣\left|AP_{O}\right|12121515
|Slugs SM|38–3884
Table 11: [ N=20N=20 random-seed orderings.] PyRoboSim P0 synthesis results, enumerated capability encoding (item 3 above). The leading digit 3 denotes this encoding. The remaining reporting convention and column legend match Table 10 . The enumerated encoding has no hand-written baseline. 3FP is realizable but shows FlexBE HFSM Realized: No for the same reason as 2FP .
Figure 14: A goal-unreachable trap in the synthesized strategy for the P0 one-hot Fair-Outcome-with-pending configuration ( 2FP , alphabetic ordering). States 72, 73, and 83 (orange) form a closed strongly-connected component reachable from state 63 (white). No edge leaves the highlighted cycle. State 63 is itself entered from elsewhere in the strategy, marked with a “ … ” stub rather than expanded, since this excerpt is a small cut-out of the full strategy graph rather than the whole reachable state machine. Uses the mealy2dot visual convention introduced in Fig. 3 (Section 3.3 ). Rendered with mealy2dot on the raw (unreduced) strategy.
 FullP12S4S4F4SP4FP
Well SeparatedTIME OUTNoNoNoNoNo
RealizableYesYesYesNoYesYes
FlexBE HFSM RealizedYesYesYesNoYesNo
∣API∣\left|AP_{I}\right|485240404040
∣APO∣\left|AP_{O}\right|141913131717
|Slugs SM|5595946–46118
Table 12: [Exploratory: budget-limited, single fixed ordering ( n=1n=1 ). See Section 6.3.2 .] PyRoboSim P1 (door-modeling) synthesis results. FullP1 is the hand-written baseline. 2S is the one-hot capability encoding (System-Goal liveness only – 2F / 2SP / 2FP were not completed at this budget). The leading digit 4 denotes the enumerated capability encoding evaluated over the P1 domain (distinct from P0’s 3 -family columns despite sharing an encoding). S / F denotes System-Goal/Fair-Outcome liveness, and P adds pending propositions. Unlike the P0 tables, reported values are a single trial under a fixed alphabetic declaration ordering ( n=1n=1 ), not a random-seed mean; therefore no ±\pm standard-deviation rows are shown – see Section 6.3.2 for why this is not directly comparable to the P0 tables. These single-ordering rows also use P1’s uncapped (“auto”) CUDD reordering policy; Appendix 12.3 reports the corresponding threshold-250 ordering experiment for 4S / 4F . FullP1 ’s well-separation check did not complete under a dedicated 43200 s (12 h) cap, so its Well Separated row reports TIME OUT rather than a completed verdict. The full specification-size and BDD-node breakdown appears in Appendix 12.2 .
 1S2S1F2F1SP2SP
Well SeparatedYesYesYesYesYesYes
RealizableYesYesYesYesYesYes
FlexBE HFSM RealizedYesYesYesYesYesYes
∣API∣\left|AP_{I}\right|842842842
∣APO∣\left|AP_{O}\right|9146914612479
|Slugs SM|119.3131102131187.0347
Table 13: [ N=20N=20 random-seed orderings for the six configurations shown. 1FP/2FP excluded from this 20-seed summary; additional Fair-Outcome-with-pending results appear in Section 6.4.1 .] Quadcopter supervisory-synthesis results. The leading digit 1 / 2 denotes the one-hot/enumerated capability encoding (the reverse of PyRoboSim’s 2 / 3 convention, since each domain assigns its own digit-to-encoding mapping; Section 6 ). Reported values are means over 20 random-seed declaration orderings under a CUDD reordering threshold of 250 and a 36,000 s per-trial synthesis budget, with a companion row giving ±\pm one standard deviation wherever the underlying trials disagree. Alphabetic and domain-grouped fixed orderings are excluded from the mean. All six configurations complete all 20 trials at this budget, including 1SP (Section 6.4.1 ), and 1SP is well-separated across all 22 declaration orderings. Integer-valued count means indicate identical samples, while non-identical count means are shown with decimal digits.
DomainEncodingPeak BDD NodesRealizabilityHFSM Realized|Reduced|
Coffee (base)One-Hot1,0220.081 msYes3.5
Coffee (base)Enumerated1,0220.050 msYes4
Coffee (extended)One-Hot1,0222.149 msYes3
Coffee (extended)Enumerated1,0220.059 msYes4
Two-RiversOne-Hot13,13353.787 msYes23
Two-RiversEnumerated19,59790.677 msYes23
Table 14: System-Goal liveness without pending memory, both encodings, across every domain/subdomain studied. This is the only formulation confirmed as a realized FlexBE HFSM across all six domain/subdomain comparisons under both encodings. Section 6.1 , Section 6.2 , Section 6.3.1 , Section 6.3.2 , and Section 6.4 report the corresponding Fair-Outcome and pending-memory comparisons in full. Bold marks the smaller value in each one-hot/enumerated pair per metric (ties left unbolded). PyRoboSim P1 rows are single alphabetic trials under the uncapped (“auto”) reordering policy, while the other rows use threshold 250. Coffee’s base capability set has no failure-prone capabilities, so its liveness variants coincide and that row informs only the encoding axis.
Appendix figures & tables12 assets

Supplementary material from the paper’s appendix.

Appendix

 12S3S2F3F2SP3SP2FP3FP
Well SeparatedYesYesYesYesYesYesYesYesNo
RealizableYesYesYesYesYesYesYesYesYes
FlexBE HFSM RealizedYesYesYesYesYesYesYesYesYes
∣API∣\left|AP_{I}\right|436363636
∣APO∣\left|AP_{O}\right|335353838
∣φia∣\left|\varphi_{i}^{a}\right|336363636
Appendix
Table 15: [ N=40N=40 random-seed orderings.] Coffee synthesis results with one-hot labeling, full detail underlying Table 7 . Reported values are the mean over 40 random declaration orderings under a CUDD reordering threshold of 250; integer-valued count means indicate identical samples, while non-identical count means are shown with one decimal digit, with a companion row giving ±\pm one standard deviation wherever the underlying trials disagree. Column 1 is the hand-written baseline; the leading digit 2 / 3 denotes the base/extended capability set, S / F denotes System-Goal/Fair-Outcome liveness, and P adds pending propositions.
 2S3S2F3F2SP3SP2FP3FP
Well SeparatedYesYesYesYesYesYesYesNo
RealizableYesYesYesYesYesYesYesYes
FlexBE HFSM RealizedYesYesYesYesYesYesYesYes
∣API∣\left|AP_{I}\right|22222222
∣APO∣\left|AP_{O}\right|24242727
∣φia∣\left|\varphi_{i}^{a}\right|22222222
Appendix
Table 16: [ N=40N=40 random-seed orderings.] Coffee synthesis results with the enumerated capability encoding, full detail underlying Table 8 (same reporting convention and column legend as Table 15 ). The enumerated encoding has no hand-written baseline, so column 1 is omitted.
Cap.Enc.Live.Pend.Alpha noneAlpha thr250Dom. noneDom. thr250Rand. noneRand. thr250
Basefull——102210221022102210221022
Baseenum.FN102210221022102210221022
Baseenum.FY102210221022102210221022
Baseenum.SN102210221022102210221022
Baseenum.SY102210221022102210221022
Base1-hotFN102210221022102210221022
Appendix
Table 17: Mean CUDD peak BDD nodes across variable-ordering and CUDD-reordering treatments, for all 16 Coffee configurations plus the hand-written baseline ( N=420N=420 trials per row: 5 repeats ×\times ( 22 fixed + 4040 random declaration orderings) ×\times 2 reordering settings; 0 failures throughout). “thr250” is the first-reordering threshold of 250 live nodes; integer-valued means indicate identical samples, while non-identical means are shown with one decimal digit.
 2S3S2F3F2SP3SP2FP3FP
Well SeparatedYesYesNoNoYesYesNoNo
RealizableYesYesNoNoYesYesYesYes
FlexBE HFSM RealizedYesYesNoNoYesYesYesYes
∣API∣\left|AP_{I}\right|1310131013101310
∣APO∣\left|AP_{O}\right|108108119119
∣φia∣\left|\varphi_{i}^{a}\right|96969696
Appendix
Table 18: [ N=40N=40 random-seed orderings.] Two-Rivers synthesis results, full detail underlying Table 9 . Reported values are means over 40 random declaration orderings under a CUDD reordering threshold of 250 ( N=200N=200 trials per column: 40 orderings ×\times 5 repeats). Integer-valued count means indicate identical samples, while non-identical count means are shown with one decimal digit, with a companion row giving ±\pm one standard deviation wherever the underlying trials disagree. Columns marked unrealizable have no extracted strategy.
OrderingEncodingRealizability (ms)Peak BDD Nodes
AlphabeticOne-Hot68.113,286
AlphabeticEnumerated51.810,220
Domain-groupedOne-Hot70.313,286
Domain-groupedEnumerated57.510,220
Random (mean, N=200N{=}200 )One-Hot53.813,132.7
Random (mean, N=200N{=}200 )Enumerated90.719,596.9
Appendix
Table 19: Two-Rivers System-Goal, no-pending realizability and peak BDD nodes under fixed declaration order, versus the 40-random-seed mean already reported for 2S / 3S in Table 18 . Fixed orderings are single deterministic trials.
EncodingMean (ms)Median (ms)Std. Dev. (ms)Min (ms)Max (ms)
One-Hot53.853.99.629.386.3
Enumerated90.777.844.841.4229.5
Appendix
Table 20: Realizability-time distribution across the 200 random-seed trials underlying 2S / 3S in Table 18 (System-Goal liveness, no pending memory).
Trials DiscardedTrials RemainingEnumerated Mean (ms)
020090.7
5 (2.5%)19587.1
10 (5%)19084.6
20 (10%)18079.9
40 (20%)16072.6
Appendix
Table 21: Enumerated mean realizability time (System-Goal, no pending) after discarding the slowest random-seed trials, out of N=200N{=}200 .
 MoveOnlyFull2S3S2F3F2SP3SP2FP3FP
Well SeparatedYesNoNoNoNoNoNoNoNoNo
RealizableYesYesYesYesNoNoYesYesYesYes
FlexBE HFSM RealizedYesYesYesYesNoNoYesYesNoNo
∣API∣\left|AP_{I}\right|8333425342534253425
∣APO∣\left|AP_{O}\right|8161712171220152015
∣φia∣\left|\varphi_{i}^{a}\right|417189189189189
Appendix
Table 22: [ N=20N=20 random-seed orderings.] PyRoboSim P0 synthesis results, full detail underlying Table 10 and Table 11 . MoveOnly / Full are the hand-written baselines; the leading digit 2 / 3 denotes one-hot/enumerated capability encoding, S / F denotes System-Goal/Fair-Outcome liveness, and P adds pending propositions. Reported values are means over 20 random-seed declaration orderings under a CUDD reordering threshold of 250, with a companion row giving ±\pm one standard deviation wherever the underlying trials disagree; the alphabetic and domain-grouped fixed orderings are not part of this mean. Columns marked unrealizable have no extracted strategy; 2FP / 3FP are realizable but show FlexBE HFSM Realized: No because the post-synthesis auditor (Section 5.5 ) halts the pipeline before reduction, discussed below.
 FullP12S4S4F4SP4FP
Well SeparatedTIME OUTNoNoNoNoNo
RealizableYesYesYesNoYesYes
FlexBE HFSM RealizedYesYesYesNoYesNo
∣API∣\left|AP_{I}\right|485240404040
∣APO∣\left|AP_{O}\right|141913131717
∣φia∣\left|\varphi_{i}^{a}\right|323624242424
Appendix
Table 23: [Exploratory: budget-limited, single fixed ordering ( n=1n=1 ); see Section 6.3.2 .] PyRoboSim P1 (door-modeling) synthesis results, full detail underlying Table 12 . FullP1 is the hand-written baseline. 2S is the one-hot capability encoding (System-Goal liveness only; 2F / 2SP / 2FP were not completed at this budget). The leading digit 4 denotes the enumerated capability encoding evaluated over the P1 domain (distinct from P0’s 3 -family columns in Table 22 despite sharing an encoding). S / F denotes System-Goal/Fair-Outcome liveness, and P adds pending propositions. Unlike Table 22 , reported values are a single trial under a fixed alphabetic declaration ordering ( n=1n=1 ), not a random-seed mean; therefore no ±\pm standard-deviation rows are shown. These single-ordering rows use P1’s uncapped (“auto”) CUDD reordering policy; Table 24 reports the corresponding threshold-250 ordering experiment for 4S / 4F . FullP1 ’s well-separation check did not complete under a 43200 s (12 h) cap, so its Well Separated row reports TIME OUT rather than a completed verdict.
OrderingColumnRealizability (s)Peak BDD Nodes
Alphabetic, auto4S235.25,643,484
Alphabetic4S3679.625,725,784
Domain-grouped4S3617.525,725,784
Random (mean, N=20N{=}20 )4S9164.026,155,841.6
Alphabetic, auto4F31.3713,356
Alphabetic4F24.0751,170
Appendix
Table 24: PyRoboSim P1’s 4S / 4F realizability and peak BDD nodes under fixed vs. random declaration order, extending Table 23 ’s single alphabetic trial with a 22-ordering sweep (2 fixed + 20 random, threshold-250 reordering). The “Alphabetic, auto” rows repeat the single uncapped-policy trial of Table 23 for a direct policy comparison.
 1S2S1F2F1SP2SP
Well SeparatedYesYesYesYesYesYes
RealizableYesYesYesYesYesYes
FlexBE HFSM RealizedYesYesYesYesYesYes
∣API∣\left|AP_{I}\right|842842842
∣APO∣\left|AP_{O}\right|9146914612479
∣φia∣\left|\varphi_{i}^{a}\right|842842842
Appendix
Table 25: [ N=20N=20 random-seed orderings for the six configurations shown; 1FP/2FP excluded from this 20-seed summary; additional Fair-Outcome-with-pending results appear in Section 13.2 .] Quadcopter supervisory-synthesis results, full detail underlying Table 13 . The leading digit 1 / 2 denotes the one-hot/enumerated capability encoding (the reverse of PyRoboSim’s 2 / 3 convention, since each domain assigns its own digit-to-encoding mapping; Section 6 ). Reported values are means over 20 random-seed declaration orderings under a CUDD reordering threshold of 250 and a 36,000 s per-trial synthesis budget, matching the Coffee, Two-Rivers, and PyRoboSim reporting convention, with a companion row giving ±\pm one standard deviation wherever the underlying trials disagree; alphabetic and domain-grouped fixed orderings are excluded from the mean. All six configurations complete all 20 trials at this budget, including 1SP (Section 13.2 ), and 1SP is well-separated across all 22 declaration orderings just like the other five configurations, once its well-separation check is given a longer timeout (Section 13.3 ). Integer-valued count means indicate identical samples, while non-identical count means are shown with one decimal digit.
ConfigurationReducedExecutable actionsTerminal/bootstrap contextsRealized HFSM
1F685115 failed + 1 finished + 1 begin_game54
1S836615 failed + 1 finished + 1 begin_game69
1SP14110531 failed + 4 finished + 1 begin_game108
2F1065153 failed + 1 finished + 1 null/bootstrap54
2S1065153 failed + 1 finished + 1 null/bootstrap54
2SP31886227 failed + 4 finished + 1 null/bootstrap89
Appendix
Table 26: Crazyflie reduced-strategy states versus realized FlexBE HFSM state instantiations for representative alphabetic, threshold-250 rows. Terminal/bootstrap contexts are reduced-strategy states that project to root-container wiring or shared FlexBE terminal outcomes rather than separate executable capability states.

Explore similar work

CardsList

  1. Temporal logics and formal synthesis for robot planning and control

    Jun 19, 2026Jana Tumova, Joris Verhagen, Matti VahsRobotic ControlSignal Temporal Logic

    KTH Royal Institute of Technology

  2. Learning to adapt GR(1) specifications through degradation

    Sep 10, 2026Tiberiu-Andrei Georgescu, Dalal Alrajeh, Sebastian UchitelProgram Synthesis

    Imperial College London, London, United Kingdom · Universidad de Buenos Aires, CONICET, Universidad de San Andrés, Argentina

  3. Correct-by-Construction Behavior Tree Synthesis from Signal Temporal Logic Specifications with Application to Robotic Missions

    Jul 21, 2026Jiaheng Dong, Jingyi Huang, Liang HanSignal Temporal LogicRobot Task Planning

    Sino-French Engineer School,Beihang University, Beijing 100191, China