CEDAR: Automata as Verifiable Interfaces for Language-Guided Embodied Action

Lekai Chen; Alvaro Velasquez; Ashutosh Trivedi

cs.AIAug 28, 2026

CEDAR: Automata as Verifiable Interfaces for Language-Guided Embodied Action

Authors: Lekai Chen, Alvaro Velasquez, Ashutosh Trivedi

Organizations: Department of Computer Science University of Colorado Boulder, USA

Abstract

Natural-language tasking of embodied agents is rarely just goal specification: users also impose constraints that must persist while the world changes. Code-generating LLM agents can produce plausible behaviors for such instructions, but their free-form programs provide no stable object to verify, compose with new constraints, or repair from a failing trace. We present CEDAR, a counterexample-guided framework that grounds instructions as regular languages over environment event traces. CEDAR uses a language model for semantic judgments and execution traces for correction, then represents both skills and specifications as deterministic finite automata. This turns constraints into executable finite-state objects: a learned skill can be intersected with a learned sleep at night or stay in this biome specification, yielding a controller that enforces the learned constraint by construction rather than by repeated prompting. In Minecraft, with the same simulator/API observations available to a program-generating baseline, CEDAR maintains temporal and spatial constraints that the baseline fails to preserve and amortizes reuse of learned skills, reducing cumulative LLM queries. These results suggest that regular languages offer a practical verification layer between natural-language instructions and embodied-agent policies.

Figures & tables

Figure 1: CEDAR workflow. The system grounds a natural-language goal or constraint into a compact symbolic alphabet, learns skill and specification DFAs using LLM membership queries (MQs) and environment or human counterexamples (CEs), stores reusable skill automata, and verifies execution by DFA composition. EQ denotes equivalence-query feedback from execution or human inspection.

Term	Meaning in CEDAR
Alphabet $\Sigma$	Task-specific set of actions, objects, and event-predicate symbols used to write traces.
Word $w$	Sequence of symbols in $\Sigma$ extracted from environment logs.
Skill DFA	Automaton whose accepted words correspond to successful execution of a task skill.
Specification DFA	Automaton whose accepted words satisfy a persistent natural-language constraint.
MQ	Query asking whether a word is consistent with an instruction; answered by the LLM.
EQ/CE	Test of a hypothesis DFA; a mismatch yields a counterexample trace.

Table 1: Language-grounding formulation.

Figure 2: DFA composition for constraint enforcement. A learned specification DFA such as “sleep at night” is intersected with a learned skill DFA such as “mine diamond ore.” The resulting controller accepts exactly the traces accepted by both learned automata. Rejecting sinks and nonessential transition detail are omitted for readability.

Figure 3: Sleep-at-night constraint. Action counts and average health for Voyager and CEDAR over repeated trials lasting three Minecraft days (aggregated over 24,000 ticks). Health denotes the averaged exact health value in the gameplay. Curves and error regions denote means and standard deviations. CEDAR suppresses night-time work because the constraint remains active throughout execution.

Figure 4: Mine-minerals-only-at-night constraint. Temporal distribution of actions and collected objects over five trials per method, with a fixed budget of 24,000 simulator ticks per trial. The direct compliance metric—the fraction of mineral-mining actions executed outside the night interval—is reported in Table 3 .

Method	Found diamond	Constraint compliant	Joint success	Mean health $\uparrow$
Voyager without assertions	4/5	0/5	0/5	$4.0\pm 3.16$
Voyager with assertions	4/5	2/5	0/5	$8.4\pm 4.56$
CodeAct without assertions	3/5	1/5	0/5	$4.8\pm 3.03$
CodeAct with assertions	0/5	3/5	0/5	$12.0\pm 5.83$
CEDAR	5/5	5/5	5/5	$\mathbf{18.4\pm 2.61}$

Table 2: Sleep-at-night assertion comparison. Exact 95% binomial confidence intervals are reported in Appendix H . Because

n=5

, the comparison is interpreted descriptively rather than as a high-powered estimate of population-level success probabilities.

Method	Actions	Underground	Overground	Items	Objects
Voyager	$106\pm 4.6$	$157\pm 15$	$48.6\pm 8.7$	$24.8\pm 6$	$229\pm 14$
CEDAR	$137\pm 12$	$189\pm 30$	$141\pm 17$	$57.4\pm 4.7$	$387\pm 13$

Table 3: Minecraft instruction following for “mine minerals only at night.” Values are mean

\pm

standard deviation for the corresponding recorded events.

Figure 5: Biome constraint. Background colors denote Minecraft biomes and heatmap intensity denotes bot activity. CEDAR remains in the requested windswept forest region, while Voyager moves across biome boundaries. The heatmaps show an aggregation of location visit frequencies over 5 trials.

Method	Wooden Pickaxe	Iron Pickaxe	Diamond Pickaxe	Lava Bucket	Compass
Voyager w/o S.L.	$6.9\pm 2.1$ (25/25)	$30.4\pm 4.5$ (25/25)	$33.4\pm 10.4$ (11/25)	$26.4\pm 7.2$ (19/25)	$25.9\pm 2.9$ (17/25)
Voyager	$4.2\pm 3.5$ (25/25)	$16.2\pm 3.8$ (25/25)	$28.9\pm 10.7$ (17/25)	$22.3\pm 5$ (25/25)	$17.7\pm 2.8$ (25/25)
CEDAR w/o S.L.	$6.6\pm 2.8$ (25/25)	$30.4\pm 3.3$ (25/25)	$45.9\pm 11.1$ (18/25)	$27.2\pm 5.6$ (25/25)	$29.8\pm 2.1$ (9/25)
CEDAR	$5.5\pm 4$ (25/25)	$9.6\pm 6$ (25/25)	$19.8\pm 6.5$ (23/25)	$10.5\pm 8.5$ (25/25)	$10\pm 2.7$ (25/25)

Table 4: Minecraft goal completion. Each method–task condition contains 25 trials. Entries report prompting iterations as mean

\pm

standard deviation over successful trajectories only. Exact 95% binomial confidence intervals for success rates are reported in Appendix I . S.L. denotes a skill library.

Figure 6: iTHOR grounding-and-repair feasibility rollouts. Time-lapse frames for making toast, making coffee, and cooking a potato. The potato task initially produced a CE due to camera perspective; adding a LOOKUP action repaired the DFA without extra LLM queries. These rollouts show that the pipeline can run outside Minecraft, but they are not used as a comparative benchmark. Results are based on 3 runs.

Appendix figures & tables13 assets

Supplementary material from the paper’s appendix.

Appendix

Method	Logs	Table	Cobble	Furnace	Iron	Diamond
Voyager	4	13	25	34	41	75
CEDAR	18	20	23	28	30	37

Appendix

Table 5: Cumulative LLM queries on the Find a Diamond milestone sequence. Lower is better.

Figure 7: Cumulative LLM-query budget for the Find a Diamond milestone sequence. CEDAR pays an early alphabet-construction cost but amortizes it through DFA reuse and reaches the final milestone with fewer total queries.

Stage	Voyager	CEDAR
Task decomposition	$2.749\pm 1.238$	$3.943\pm 2.134$
Code/sample generation	$6.381\pm 1.990$	$5.548\pm 1.876$
Program description	$2.384\pm 1.208$	N/A
Skill addition	$2.653\pm 1.228$	$0.021\pm 0.008$
DFA construction	N/A	$18.548\pm 14.289$
Skill retrieval	$0.323\pm 0.235$	$0.089\pm 0.586$

Appendix

Table 6: Stage-wise wall-clock time in seconds, reported as mean

\pm

standard deviation over 5 independent measurements per stage.

Figure 8: RAG-based alphabet construction. From the global action, object, and event-predicate alphabet, retrieval selects task-relevant symbols that the LLM prunes into the finite alphabet used for DFA learning. The selected predicates are symbolic recodings of existing simulator/API observations, not additional perceptual inputs.

Metric	Absolute Acc.	Overlap Coef.	Cosine Sim.
RAG	$0.9372\pm 0.10$	$0.9208\pm 0.10$	$0.4500\pm 0.14$

Appendix

Table 7: RAG alphabet-construction performance over 44 validated skill DFAs.

Task	LLM calls	Outcome
Make Toast	2	success
Make Coffee	2	success
Cook Potato	2	success after CE fix
Make Salad	2	success
Store Plate in Fridge	2	success

Appendix

Table 8: iTHOR query budget for the feasibility study. The counterexample fix for Cook Potato did not require additional LLM calls. Each task is evaluated over 3 executions.

Item	Accuracy	Standard deviation
Dirt	0.9727	0.1629
Birch Log	0.8636	0.3432
Grass Block	1.0000	0.0000
Birch Leaves	0.9909	0.0949
Stone	0.9727	0.1629
Coal Ore	1.0000	0.0000

Appendix

Table 9: Counterexample discovery in Minecraft simulations after perturbing correct skill DFAs.

Figure 9: Counterexample collection by CE length. Shorter counterexamples are easier to surface during simulation; most observed CEs have length below seven, where collection probability remains high.

Specification	Human CEs	Final DFA states
Sleep at night	8	9
Mining only at night	5	5
Stay in windswept forest	4	2

Appendix

Table 10: Human counterexamples used for specification-DFA learning. The modality identifies trajectory annotation, demonstration logs, or direct formal trace judgment. Time reports the total annotation time used in the reported run rather than a theoretical intervention bound.

Figure 10: Human counterexample interfaces. Counterexamples can be supplied through trajectory annotation, demonstration logs, or direct formal words over the DFA alphabet.

Method	Found diamond	Constraint compliant	Joint success
Voyager w/o A.	4/5 $[0.284,0.995]$	0/5 $[0.000,0.522]$	0/5 $[0.000,0.522]$
Voyager w/ A.	4/5 $[0.284,0.995]$	2/5 $[0.053,0.853]$	0/5 $[0.000,0.522]$
CodeAct w/o A.	3/5 $[0.147,0.947]$	1/5 $[0.005,0.716]$	0/5 $[0.000,0.522]$
CodeAct w A.	0/5 $[0.000,0.522]$	3/5 $[0.147,0.947]$	0/5 $[0.000,0.522]$
CEDAR	5/5 $[0.478,1.000]$	5/5 $[0.478,1.000]$	5/5 $[0.478,1.000]$

Appendix

Table 11: Observed success counts and exact two-sided 95% Clopper–Pearson confidence intervals for the five-trial sleep-at-night comparison. The intervals describe marginal binary outcomes and do not remove the uncertainty caused by the small sample. A.: aseertions .

Task	Voyager w/o S.L.	Voyager	CEDAR w/o S.L.	CEDAR
Wooden	25/25 $[0.863,1.000]$	25/25 $[0.863,1.000]$	25/25 $[0.863,1.000]$	25/25 $[0.863,1.000]$
Iron	25/25 $[0.863,1.000]$	25/25 $[0.863,1.000]$	25/25 $[0.863,1.000]$	25/25 $[0.863,1.000]$
Diamond	11/25 $[0.244,0.651]$	17/25 $[0.465,0.851]$	18/25 $[0.506,0.879]$	23/25 $[0.740,0.990]$
Lava	19/25 $[0.549,0.906]$	25/25 $[0.863,1.000]$	25/25 $[0.863,1.000]$	25/25 $[0.863,1.000]$
Compass	17/25 $[0.465,0.851]$	25/25 $[0.863,1.000]$	9/25 $[0.180,0.575]$	25/25 $[0.863,1.000]$

Appendix

Table 12: Task-success counts and exact two-sided 95% Clopper–Pearson confidence intervals over 25 trials per method–task condition. S.L. denotes a skill library.

Metric	Diamond $\cap$ Sleep	Mine $\cap$ Night	Explore $\cap$ Biome
Skill DFA states	7	N/A	N/A
Specification DFA states	9	3	2
Reachable product states	17	3	2

Appendix

Table 13: Component and reachable product-automaton sizes for the evaluated skill–constraint compositions. The worst-case product size is

|Q_{g}||Q_{c}|

; the reported product sizes exclude unreachable states.

Language-Conditioned Robot Control

Language-conditioned robot control connects natural-language instructions to grounded, safe actions across tasks and robot embodiments.

See all 74 papers

Learning Context-Free Grammars for Grammar-Constrained Decoding via Declarative Agentic Programming with Guarantees
Aug 6, 2026Kevin Cheang, Geoff Hulette, Rahul Kumar +5LLM-Based Program Synthesis Linear Temporal Logic
Amazon Web Services · Purdue University
STAGE: Diagnosing Semantic Transfer at Grounded Execution in Embodied Agents
Sep 11, 2026Baosheng Jin, Yushen Liang, Hua ShenLanguage-Conditioned Robot Manipulation Vision-Language-Action Models
Center for Data Science, NYU Shanghai Shanghai, China
Think Twice, Act Once: Verifier-Guided Action Selection For Embodied Agents
May 12, 2026Nishad Singhi, Christian Bialas, Snehal Jauhri +4OOD Generalization Embodied AI
Technical University of Darmstadt & hessian.AI

Aug 6, 2026J/K move · Enter open · S save

Learning Context-Free Grammars for Grammar-Constrained Decoding via Declarative Agentic Programming with Guarantees

Kevin Cheang, Geoff Hulette, Rahul Kumar, Felipe R. Monteiro+4

Amazon Web Services · Purdue University

LLM-Based Program Synthesis Linear Temporal Logic Grammar-Constrained Decoding

Open paper AskPDF arXiv

Language models (LMs) are increasingly used to interact with external services via programs written in domain-specific languages (DSLs). Unfortunately, since DSLs are often low-resource and esoteric, LMs frequently produce syntactically invalid programs in these languages. Grammar-constrained decoding can eliminate such failures, but requires syntactic constraints. These are usually in the form of a context-free grammar for the target language, an artifact that is hard to come by for third-party DSLs. In this work, we define an agent, called Autogrammar, that automatically learns context-free grammars from documentation and execution data. Autogrammar is formalized as a Kripke structure whose nondeterministic choices are resolved by a language model, enabling declarative control of agent behavior via linear temporal logic constraints. We evaluate four versions of Autogrammar on three DSLs (i.e., Amazon CloudWatch Logs Insights, Dynatrace Query Language, and Datadog Search Syntax) and find that it generates grammars that achieve near perfect precision on unseen data; that temporal restrictions reduce execution time by 3.8x without incurring statistically-significant loss in precision; that execution data is crucial while documentation is dispensable; and that grammar-constrained decoding using Autogrammar-generated grammars significantly improves end-to-end LM performance on eight out of ten real tasks, matching or exceeding the performance of a professionally-maintained grammar. In comparison, the context-free grammars generated by existing LM baselines and a state-of-the-art formal technique perform significantly worse over the same evaluation.

Abstract

Language-Conditioned Robot Control

Explore similar work

Learning Context-Free Grammars for Grammar-Constrained Decoding via Declarative Agentic Programming with Guarantees

STAGE: Diagnosing Semantic Transfer at Grounded Execution in Embodied Agents

Think Twice, Act Once: Verifier-Guided Action Selection For Embodied Agents