End-to-End Abstraction-Based Control with LLM-Enhanced NL-to-LTL Translation
This work presents an LLM-enhanced pipeline to translate natural language requirements into formal Linear Temporal Logic (LTL) specifications for Abstraction-Based Controller Design. The system uses a multi-step process involving LLM translation, human validation, and synthesis using Spot and Dionysos to generate safe controllers. Findings show translation accuracy degrades systematically as the target LTL formula complexity increases.