End-to-End Abstraction-Based Control with LLM-Enhanced NL-to-LTL Translation
For researchers and practitioners in safe control of cyber-physical systems, this work provides an evaluation framework and integration pathway to make formal methods more accessible via LLMs, though the results highlight current limitations in handling complex specifications.
The paper proposes an LLM-enhanced pipeline for Abstraction-Based Controller Design (ABCD) that translates natural language requirements into Linear Temporal Logic (LTL) specifications. Experiments show that translation accuracy degrades systematically with LTL formula complexity, revealing a scaling law linking LLM success rate to specification complexity.
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.