End-to-End Abstraction-Based Control
with LLM-Enhanced NL-to-LTL Translation

Abstract

Abstraction-Based Controller Design (ABCD) offers a principled framework for the safe control of complex Cyber-Physical Systems (CPSs), but interfacing real-world requirements with its formal synthesis machinery remains a major bottleneck: such requirements are most naturally expressed in Natural Language (NL), whereas ABCD requires formal specifications such as Linear Temporal Logic (LTL). Large Language Models (LLMs) offer a promising way to bridge this gap by translating NL requirements into formal specifications.

This paper makes three contributions. First, we formalize an LLM-enhanced pipeline for ABCD, in which NL requirements are translated into LTL and used within a formal synthesis workflow. Second, we implement this pipeline in the Dionysos toolbox and introduce a benchmark for evaluating NL-to-LTL translation under both logical diversity and linguistic variation.

Third, through experiments with state-of-the-art LLMs, we show that translation accuracy degrades systematically as the target specifications become more complex, across several measures including Abstract Syntax Tree (AST) size, temporal depth, and Büchi automaton size, while also accounting for the length of the NL input. These results reveal a scaling law that links LLM success rate to the intrinsic complexity of the underlying LTL formula. Together, these contributions provide both an evaluation framework and a practical integration pathway for making ABCD more accessible while preserving the rigor of formal methods.

Benchmark Construction

We introduce a benchmark for evaluating NL-to-LTL translation beyond a limited set of hand-written templates. LTL formulas are generated with controlled AST size, back-translated into canonical English, and then paraphrased using multiple LLMs to introduce linguistic diversity.

Benchmark construction pipeline from LTL formulas to diverse NL-LTL pairs.

Interactive NL Interface for ABCD

We implement an interactive interface for synthesizing ABCD controllers from NL requirements. The user enters an NL requirement, the system generates the corresponding LTL formula, and the controller synthesis pipeline is executed through Dionysos.jl.

Interactive NL interface for ABCD synthesis.

Citation

@misc{bayat2026endtoend,
  title         = {End-to-End Abstraction-Based Control from Natural Language with LLM-Enhanced NL-to-LTL Translation},
  author        = {Bayat, Amir and Jungers, Raphaël M.},
  year          = {2026},
  archivePrefix = {arXiv},
  eprint        = {2606.30163},
  doi           = {10.48550/arXiv.2606.30163}
}