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

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.

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.

Environment
Term	Form
$\varphi_{i}^{a}$	$\psi:AP_{I}$ with $\land,\lor,\neg$ only
$\varphi_{s}^{a}$	$G\psi:AP_{I}\cup AP_{O}\cup\left\{Xy:y\in AP_{I}\right\}$
$\varphi_{l}^{a}$	$GF\psi:AP_{I}\cup AP_{O}\cup\left\{Xy:y\in AP_{I}\cup AP_{O}\right\}$
System
$\varphi_{i}^{g}$	$\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.

Panel of Figure 7 — 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.

Panel of Figure 11 — 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).

$\tau$	gr_a	outcome observed	gr_p	rule
0	F	—	F	(initial)
1	T (activate)	—	T	conjunct 1
2	F	gr_f (failure)	T	conjunct 2
3	T (retry)	—	T	conjunct 1
4	F	gr_c (completed)	F	conjunct 3
5	F	—	F	conjunct 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.

Question	Well-separation / assumption-falsification analysis	Post-synthesis strategy auditor
Artifact checked	The GR(1) specification and game before synthesis.	The extracted Mealy strategy after synthesis.
Main failure exposed	Whether 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 examples	The 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 certify	That 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.
Benefit	Diagnoses 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.

Domain	Goal condition $g$	Interpretation
Coffee	br_c	Recurring successful brew completion in a controller designed to run forever.
Two-Rivers	finished	Successful terminal output after all entities reach the far bank.
PyRoboSim P0/P1	finished	Successful terminal output after the delivery task is complete.
Quadcopter	finished $\lor$ failed	Programmed terminal output; the audit certifies reachability of termination, not mission success alone.

Table 4: Configured goal condition

g

(Section 5.2.3 ) supplied to the post-synthesis strategy auditor for each domain.

Factor	Levels tested
Capability encoding	One-hot (Section 5.2.2 ) and enumerated (Section 5.2.2 )
Liveness formulation	System-Goal (Section 5.2.3 ) and Fair-Outcome (Section 5.2.3 )
Pending memory	Without or with a persistent proposition tracking whether a completion is still owed (Section 5.2.1 )
Comparisons	Coffee 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 ordering	Fixed alphabetic, fixed capability-grouped (“domain-grouped”), and $N$ random-seed orderings ( $N=40$ for Coffee/Two-Rivers and $N=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 policy	Threshold 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.

Row	What It Measures	Timing Source
Generate Specs	Building the GR(1) specification from the request’s capability subset (Section 3.2 ).	Python harness
Well-Separation	Assumption-falsification check on the compiled specification (Section 5.3 ), a separate slugs invocation.	slugs -internal
Realizability	The 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
Extraction	The subsequent walk converting the symbolic strategy into the explicit Mealy machine slugs returns. Realizable rows only.	slugs -internal
Auditing	The post-synthesis auditor’s pass over the extracted machine (Section 5.5 ).	Python harness
Realize HFSM	Translating 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.

	1	2S	3S	2F	3F	2SP	3SP	2FP	3FP
Well Separated	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	No
Realizable	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes
FlexBE HFSM Realized	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes
$\left\|AP_{I}\right\|$	4	3	6	3	6	3	6	3	6
$\left\|AP_{O}\right\|$	3	3	5	3	5	3	8	3	8
\|Slugs SM\|	7	4.5	7	4.5	7	4.5	7	4.5	7

Table 7: [

N=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.

	2S	3S	2F	3F	2SP	3SP	2FP	3FP
Well Separated	Yes	Yes	Yes	Yes	Yes	Yes	Yes	No
Realizable	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes
FlexBE HFSM Realized	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes
$\left\|AP_{I}\right\|$	2	2	2	2	2	2	2	2
$\left\|AP_{O}\right\|$	2	4	2	4	2	7	2	7
\|Slugs SM\|	6	8	6	8	6	8	6	8

Table 8: [

N=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.

	2S	3S	2F	3F	2SP	3SP	2FP	3FP
Well Separated	Yes	Yes	No	No	Yes	Yes	No	No
Realizable	Yes	Yes	No	No	Yes	Yes	Yes	Yes
FlexBE HFSM Realized	Yes	Yes	No	No	Yes	Yes	Yes	Yes
$\left\|AP_{I}\right\|$	13	10	13	10	13	10	13	10
$\left\|AP_{O}\right\|$	10	8	10	8	11	9	11	9
\|Slugs SM\|	37	26	–	–	37	26	37	26

Table 9: [

N=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=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.

	Full	2S	2F	2SP	2FP
Well Separated	No	No	No	No	No
Realizable	Yes	Yes	No	Yes	Yes
FlexBE HFSM Realized	Yes	Yes	No	Yes	No
$\left\|AP_{I}\right\|$	33	34	34	34	34
$\left\|AP_{O}\right\|$	16	17	17	20	20
\|Slugs SM\|	116	47	–	47	108

Table 10: [

N=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.

	3S	3F	3SP	3FP
Well Separated	No	No	No	No
Realizable	Yes	No	Yes	Yes
FlexBE HFSM Realized	Yes	No	Yes	No
$\left\|AP_{I}\right\|$	25	25	25	25
$\left\|AP_{O}\right\|$	12	12	15	15
\|Slugs SM\|	38	–	38	84

Table 11: [

N=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.

	FullP1	2S	4S	4F	4SP	4FP
Well Separated	TIME OUT	No	No	No	No	No
Realizable	Yes	Yes	Yes	No	Yes	Yes
FlexBE HFSM Realized	Yes	Yes	Yes	No	Yes	No
$\left\|AP_{I}\right\|$	48	52	40	40	40	40
$\left\|AP_{O}\right\|$	14	19	13	13	17	17
\|Slugs SM\|	559	59	46	–	46	118

Table 12: [Exploratory: budget-limited, single fixed ordering (

n=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=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 .

	1S	2S	1F	2F	1SP	2SP
Well Separated	Yes	Yes	Yes	Yes	Yes	Yes
Realizable	Yes	Yes	Yes	Yes	Yes	Yes
FlexBE HFSM Realized	Yes	Yes	Yes	Yes	Yes	Yes
$\left\|AP_{I}\right\|$	84	2	84	2	84	2
$\left\|AP_{O}\right\|$	91	46	91	46	124	79
\|Slugs SM\|	119.3	131	102	131	187.0	347

Table 13: [

N=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.

Domain	Encoding	Peak BDD Nodes	Realizability	HFSM Realized	\|Reduced\|
Coffee (base)	One-Hot	1,022	0.081 ms	Yes	3.5
Coffee (base)	Enumerated	1,022	0.050 ms	Yes	4
Coffee (extended)	One-Hot	1,022	2.149 ms	Yes	3
Coffee (extended)	Enumerated	1,022	0.059 ms	Yes	4
Two-Rivers	One-Hot	13,133	53.787 ms	Yes	23
Two-Rivers	Enumerated	19,597	90.677 ms	Yes	23

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

	1	2S	3S	2F	3F	2SP	3SP	2FP	3FP
Well Separated	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	No
Realizable	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes
FlexBE HFSM Realized	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes
$\left\|AP_{I}\right\|$	4	3	6	3	6	3	6	3	6
$\left\|AP_{O}\right\|$	3	3	5	3	5	3	8	3	8
$\left\|\varphi_{i}^{a}\right\|$	3	3	6	3	6	3	6	3	6

Appendix

Table 15: [

N=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.

	2S	3S	2F	3F	2SP	3SP	2FP	3FP
Well Separated	Yes	Yes	Yes	Yes	Yes	Yes	Yes	No
Realizable	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes
FlexBE HFSM Realized	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes
$\left\|AP_{I}\right\|$	2	2	2	2	2	2	2	2
$\left\|AP_{O}\right\|$	2	4	2	4	2	7	2	7
$\left\|\varphi_{i}^{a}\right\|$	2	2	2	2	2	2	2	2

Appendix

Table 16: [

N=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 none	Alpha thr250	Dom. none	Dom. thr250	Rand. none	Rand. thr250
Base	full	—	—	1022	1022	1022	1022	1022	1022
Base	enum.	F	N	1022	1022	1022	1022	1022	1022
Base	enum.	F	Y	1022	1022	1022	1022	1022	1022
Base	enum.	S	N	1022	1022	1022	1022	1022	1022
Base	enum.	S	Y	1022	1022	1022	1022	1022	1022
Base	1-hot	F	N	1022	1022	1022	1022	1022	1022

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=420

trials per row: 5 repeats

\times

(

2

fixed +

40

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.

	2S	3S	2F	3F	2SP	3SP	2FP	3FP
Well Separated	Yes	Yes	No	No	Yes	Yes	No	No
Realizable	Yes	Yes	No	No	Yes	Yes	Yes	Yes
FlexBE HFSM Realized	Yes	Yes	No	No	Yes	Yes	Yes	Yes
$\left\|AP_{I}\right\|$	13	10	13	10	13	10	13	10
$\left\|AP_{O}\right\|$	10	8	10	8	11	9	11	9
$\left\|\varphi_{i}^{a}\right\|$	9	6	9	6	9	6	9	6

Appendix

Table 18: [

N=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=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.

Ordering	Encoding	Realizability (ms)	Peak BDD Nodes
Alphabetic	One-Hot	68.1	13,286
Alphabetic	Enumerated	51.8	10,220
Domain-grouped	One-Hot	70.3	13,286
Domain-grouped	Enumerated	57.5	10,220
Random (mean, $N{=}200$ )	One-Hot	53.8	13,132.7
Random (mean, $N{=}200$ )	Enumerated	90.7	19,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.

Encoding	Mean (ms)	Median (ms)	Std. Dev. (ms)	Min (ms)	Max (ms)
One-Hot	53.8	53.9	9.6	29.3	86.3
Enumerated	90.7	77.8	44.8	41.4	229.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 Discarded	Trials Remaining	Enumerated Mean (ms)
0	200	90.7
5 (2.5%)	195	87.1
10 (5%)	190	84.6
20 (10%)	180	79.9
40 (20%)	160	72.6

Appendix

Table 21: Enumerated mean realizability time (System-Goal, no pending) after discarding the slowest random-seed trials, out of

N{=}200

	MoveOnly	Full	2S	3S	2F	3F	2SP	3SP	2FP	3FP
Well Separated	Yes	No	No	No	No	No	No	No	No	No
Realizable	Yes	Yes	Yes	Yes	No	No	Yes	Yes	Yes	Yes
FlexBE HFSM Realized	Yes	Yes	Yes	Yes	No	No	Yes	Yes	No	No
$\left\|AP_{I}\right\|$	8	33	34	25	34	25	34	25	34	25
$\left\|AP_{O}\right\|$	8	16	17	12	17	12	20	15	20	15
$\left\|\varphi_{i}^{a}\right\|$	4	17	18	9	18	9	18	9	18	9

Appendix

Table 22: [

N=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.

	FullP1	2S	4S	4F	4SP	4FP
Well Separated	TIME OUT	No	No	No	No	No
Realizable	Yes	Yes	Yes	No	Yes	Yes
FlexBE HFSM Realized	Yes	Yes	Yes	No	Yes	No
$\left\|AP_{I}\right\|$	48	52	40	40	40	40
$\left\|AP_{O}\right\|$	14	19	13	13	17	17
$\left\|\varphi_{i}^{a}\right\|$	32	36	24	24	24	24

Appendix

Table 23: [Exploratory: budget-limited, single fixed ordering (

n=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=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.

Ordering	Column	Realizability (s)	Peak BDD Nodes
Alphabetic, auto	4S	235.2	5,643,484
Alphabetic	4S	3679.6	25,725,784
Domain-grouped	4S	3617.5	25,725,784
Random (mean, $N{=}20$ )	4S	9164.0	26,155,841.6
Alphabetic, auto	4F	31.3	713,356
Alphabetic	4F	24.0	751,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.

	1S	2S	1F	2F	1SP	2SP
Well Separated	Yes	Yes	Yes	Yes	Yes	Yes
Realizable	Yes	Yes	Yes	Yes	Yes	Yes
FlexBE HFSM Realized	Yes	Yes	Yes	Yes	Yes	Yes
$\left\|AP_{I}\right\|$	84	2	84	2	84	2
$\left\|AP_{O}\right\|$	91	46	91	46	124	79
$\left\|\varphi_{i}^{a}\right\|$	84	2	84	2	84	2

Appendix

Table 25: [

N=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.

Configuration	Reduced	Executable actions	Terminal/bootstrap contexts	Realized HFSM
1F	68	51	15 failed + 1 finished + 1 begin_game	54
1S	83	66	15 failed + 1 finished + 1 begin_game	69
1SP	141	105	31 failed + 4 finished + 1 begin_game	108
2F	106	51	53 failed + 1 finished + 1 null/bootstrap	54
2S	106	51	53 failed + 1 finished + 1 null/bootstrap	54
2SP	318	86	227 failed + 4 finished + 1 null/bootstrap	89

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

Jun 19, 2026

Temporal logics and formal synthesis for robot planning and control

As robots move from controlled environments into real-world settings, it becomes increasingly crucial to ensure that they perform as expected. A key step toward that goal is a rigorous specification of the desired robot behavior, capturing intricate temporal, spatial, and logical requirements. Complementing this, plan and control synthesis methods are needed to fulfill these specifications with provable guarantees. This manuscript presents temporal logics - particularly linear and signal temporal logic - as expressive specification languages for robot behavior over time. We then discuss principles of formal synthesis, from discrete graph- and game-based approaches to sampling-based motion planning, trajectory optimization, and control-certificate-based synthesis. Finally, we outline challenges in deploying formal synthesis in real-world robotics, emphasizing the interplay between modeling fidelity, computational tractability, and the types of rigorous guarantees that can be achieved.

Jana Tumova, Joris Verhagen, Matti Vahs

KTH Royal Institute of Technology

Robotic Control Signal Temporal Logic Robotics Formal Verification Robot Motion Planning Linear Temporal Logic

Ask PDF

Sep 10, 2026

Learning to adapt GR(1) specifications through degradation

Reactive synthesis is a powerful tool for generating correct-by-construction controllers from formal specifications. GR(1) is an assume-guarantee specification framework that enables efficient synthesis, allowing synthesised controllers to be used in a wide array of applications. The limitation of such controllers is that, should they encounter environment behaviour unspecified in the assumptions of the specification, the specified system guarantees are no longer ensured. Our work proposes an approach based on oracle-guided inductive synthesis to adapt the specification to be consistent with the observed assumption violation, while degrading system guarantees as little as possible to maintain realisability. Our methodology discovers multiple potential solutions, so we propose a preference criteria, based on the ability of the specification to enable robustness under adaptation. Although our approach is capable of degrading the entire specification, for our case studies we successfully discover degradations that preserve the entire set of original guarantees.

Tiberiu-Andrei Georgescu, Dalal Alrajeh, Sebastian Uchitel

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

Program Synthesis

Ask PDF

Jul 21, 2026

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

Behavior Trees (BTs) are widely adopted for complex task execution in robotics, providing modular, reactive control but lacking formal guarantees. However, existing correct-by-construction synthesis from Linear Temporal Logic (LTL) cannot express quantitative timing constraints. This letter synthesizes correct-by-construction BTs from Signal Temporal Logic (STL) specifications. The workspace is modeled as a timed transition system and abstracted into a zone graph, and an augmented state space tracking both logical progress and timing constraints is introduced. A hierarchical fixed-point algorithm computes winning sets for an STL fragment encompassing safety, reachability, response, recurrence, and persistence, yielding BT subtrees with a runtime constraint function. Correctness guarantees are proven and complexity bounds are derived. Simulations demonstrate specification satisfaction with strictly positive robustness, and a physical quadrotor experiment with six STL specifications validates practical deployability.

Jiaheng Dong, Jingyi Huang, Liang Han

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

Signal Temporal Logic Robot Task Planning Behavior Trees

Ask PDF