From Ambiguous Language to Verifiable Plans: Integrating Formal Synthesis and Dynamic Affordance Reasoning

Abstract

Translating ambiguous human instructions into verifiable robot actions in semistructured environments requires bridging the semantic–execution gap between high-level intent and formally monitored execution. Existing symbolic planners rely on fixed, manually specified state vocabularies, while learning-based methods offer flexibility but lack formal guarantees. We present a hierarchical reactive planning framework for specification-preserving runtime adaptation. The central idea is to treat the active LTL$_{f}$/DFA specification as a runtime contract that is instantiated from scene context, preserved under object rebinding when proposition effects are unchanged, and regenerated only when the product-automaton state indicates that specification preservation is no longer possible. VLPGen constructs a scene-conditioned symbolic interface by synthesizing task-relevant LTL$_{f}$ specifications and proposition vocabularies from visual–linguistic context, thereby avoiding a predefined task-level predicate inventory while operating under a fixed primitive skill library. ContextualAfford enables execution-time functional substitution by grounding task-conditioned affordances to identify substitutes that preserve the proposition effects of the active task role, so object identity may change while the induced DFA transition remains the same. A monitor-guided recovery mechanism uses the current product-automaton state to decide whether execution can remain within the active specification or must trigger global specification regeneration. On a Franka Panda manipulator under dynamic uncertainty, the framework achieves 94.5% task success in static settings, 84% under functional-equivalence substitution, and 72% on long-horizon multistep sequences. We also release ContextaFF, a benchmark of 550 images with pixel-level affordance annotations and natural language instructions for language-grounded functional equivalence evaluation.