Automatic Generation of Safety-compliant Linear Temporal Logic via Large Language Model: A Self-supervised Framework
Junle Li, Meiqi Tian, Bingzhuo Zhong
TL;DR
AutoSafeLTL tackles the problem of generating safety-compliant LTL specifications from natural language for CPS. It couples LLM-driven extraction with a formal verification loop that uses automata-based language inclusion checks (Ramsey-based) to enforce safety restrictions, supported by two agents: LLM-as-an-Aligner for atomic proposition alignment and LLM-as-a-Critic for counterexample-guided refinement. The approach demonstrates zero safety-violation rate in experiments and achieves substantial semantic alignment with original instructions, illustrating a practical synergy between AI and formal verification. Collectively, the work shows how self-supervised AI methods can produce formally guaranteed, safety-aware specifications at scale for AI-enabled CPS."
Abstract
Converting high-level tasks described by natural language into formal specifications like Linear Temporal Logic (LTL) is a key step towards providing formal safety guarantees over cyber-physical systems (CPS). While the compliance of the formal specifications themselves against the safety restrictions imposed on CPS is crucial for ensuring safety, most existing works only focus on translation consistency between natural languages and formal specifications. In this paper, we introduce AutoSafeLTL, a self-supervised framework that utilizes large language models (LLMs) to automate the generation of LTL specifications complying with a set of safety restrictions while preserving their logical consistency and semantic accuracy. As a key insight, our framework integrates Language Inclusion check with an automated counterexample-guided modification mechanism to ensure the safety-compliance of the resulting LTL specifications. In particular, we develop 1) an LLM-as-an-Aligner, which performs atomic proposition matching between generated LTL specifications and safety restrictions to enforce semantic alignment; and 2) an LLM-as-a-Critic, which automates LTL specification refinement by interpreting counterexamples derived from Language Inclusion checks. Experimental results demonstrate that our architecture effectively guarantees safety-compliance for the generated LTL specifications, achieving a 0% violation rate against imposed safety restrictions. This shows the potential of our work in synergizing AI and formal verification techniques, enhancing safety-aware specification generation and automatic verification for both AI and critical CPS applications.