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.30460

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

View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

cs.RO cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

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. 2026-09-24. Realizability Is Not Enough: Encoding, Liveness, and Auditing of Synthesized Robot Supervisors. https://arxiv.org/abs/2609.30460

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Structured-Diffuser: Diffusion with Task-Conditioned Structured Priors for Motion Planning

We propose Structured-Diffuser, a diffusion planner that embeds task and motion structure directly into the noise model. Unlike standard diffusion-based planners that rely on zero-mean, isotropic Gaussian corruption, we introduce task-conditioned structured Gaussians whose means and covariances are derived from Gaussian Process Motion Planning (GPMP), explicitly encoding trajectory smoothness and task semantics in the prior. We first formulate diffusion under a task-conditioned, non-isotropic Gaussian prior with closed-form forward and posterior expressions. Building on this formulation, our hierarchical design separates prior instantiation from trajectory denoising. At the upper level, sparse task-centric key states and timings are obtained, which instantiate a structured Gaussian prior (mean and covariance). At the lower level, the full trajectory is denoised under this prior, treating the upper-level outputs as noisy observations. Experiments across three motion-planning tasks show improved task success and training efficiency, with additional gains in data efficiency, trajectory smoothness, and position--velocity consistency where evaluated. Ablation studies further show that explicitly structuring the corruption process provides benefits beyond neurally conditioning the denoising network alone. Overall, our approach concentrates the prior's probability mass around task-relevant, temporally structured trajectories. We additionally demonstrate deployment on a physical G1 humanoid.

cs.RO↗

arXiv2026

SANDO: Safe Autonomous Trajectory Planning for Dynamic Unknown Environments

This paper presents SANDO, a safe trajectory planner for 3D dynamic unknown environments. Existing soft-constraint planners are fast but do not guarantee collision-free paths, while hard-constraint methods typically ensure safety at the cost of longer computation. SANDO addresses this trade-off through three contributions. First, a heat map-based A* global planner steers the path away from high-risk regions, and a spatiotemporal safe flight corridor (STSFC) generator produces time-layered polytopes that inflate obstacles only by their worst-case reachable set at each time layer, rather than over the entire horizon. Second, trajectory optimization is formulated as a mixed-integer quadratic program with hard collision-avoidance constraints, and variable elimination reduces the number of decision variables. Third, a formal safety analysis establishes collision-free guarantees under explicit velocity-bound, size-bound, and estimation-error assumptions. Ablation studies confirm that variable elimination yields up to 7.4 times faster optimization and that STSFCs are critical for feasibility in dense dynamic environments. In simulations against state-of-the-art methods, SANDO achieves a 100% success rate across all forest and dynamic benchmark difficulty levels with no constraint violations, and perception-only experiments demonstrate the full perception-to-planning pipeline. Hardware experiments with fully onboard planning, perception, and localization demonstrate six safe flights in static environments and twelve among dynamic obstacles.

cs.RO↗

arXiv2026

Cloak: Zero-Shot Cross-Embodiment Manipulation by Masking the End-Effector from the VLA

We present Cloak, a training recipe that endows a Vision-Language-Action (VLA) model with zero-shot cross-embodiment transfer by cloaking the end-effector from its own wrist camera. The end-effector occupies a large and consistent region of the wrist view and masking it allows for embodiment-agnostic visual reasoning. Cloak renders a mask in simulation from the robot's known geometry, accurately and in real time, with no segmentation or generative models. During training, we augment the mask so the model generalizes to embodiments unseen at training time. We demonstrate the recipe with Cloak-VLA, a VLA trained with Cloak on a single parallel-jaw gripper dataset. No data of new embodiments is ever collected. Cloak-VLA transfers zero-shot to various unseen embodiments, including another gripper, another arm, and a five-fingered hand, while preserving the source embodiment's performance. By decoupling the wrist view from its own embodiment, Cloak allows data to outlive the hardware it was collected on.

cs.RO↗