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

arXiv: https://arxiv.org/abs/2608.27797 · HTML: https://mlsanity.com/paper/2608.27797/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 8 of its 18 references that are in the map.
- First posted on arXiv 28 Aug 2026.

## Builds on (most cited first, 8 of 8)

- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [Executable Code Actions Elicit Better LLM Agents](https://mlsanity.com/paper/2402.01030/) (2024)
- [Ghost in the Minecraft: Generally Capable Agents for Open-World Environments via Large Language Models with Text-based Knowledge and Memory](https://mlsanity.com/paper/2305.17144/) (2023)
- [Joint Inference of Reward Machines and Policies for Reinforcement Learning](https://mlsanity.com/paper/1909.05912/) (2019)
- [Data-Efficient Learning of Natural Language to Linear Temporal Logic Translators for Robot Task Specification](https://mlsanity.com/paper/2303.08006/) (2023)
- [When TableQA Meets Noise: A Dual Denoising Framework for Complex Questions and Large-scale Tables](https://mlsanity.com/paper/2509.17680/) (2025)
- [Rethinking Table Pruning in TableQA: From Sequential Revisions to Gold Trajectory-Supervised Parallel Search](https://mlsanity.com/paper/2601.03851/) (2026)
- [Joint Verification and Refinement of Language Models for Safety-Constrained Planning](https://mlsanity.com/paper/2410.14865/) (2024)

## Abstract (arXiv)

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.