💻 computer science

Bridging Natural Language and Formal Specification--Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs

This paper introduces Req2LTL, a modular framework that leverages large language models for hierarchical semantic decomposition and deterministic rule-based synthesis to automatically translate natural language software requirements into syntactically valid and semantically accurate Linear Temporal Logic specifications, achieving superior performance on real-world aerospace datasets.

Original authors: Zhi Ma, Cheng Wen, Zhexin Su, Xiao Liang, Cong Tian, Shengchao Qin, Mengfei Yang

Published 2026-06-16

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Zhi Ma, Cheng Wen, Zhexin Su, Xiao Liang, Cong Tian, Shengchao Qin, Mengfei Yang

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are trying to give instructions to a very strict, literal-minded robot. You speak in natural, flowing English (like "If the light turns red, wait until it turns yellow before going"). But the robot only understands a rigid, mathematical code called LTL (Linear Temporal Logic). If you make even a tiny mistake in your instructions, the robot might crash the system.

Currently, humans have to act as translators, manually rewriting these instructions into the robot's code. It's slow, boring, and prone to human error.

This paper introduces a new tool called REQ2LTL that automates this translation. Think of it as a "smart translator" that doesn't just guess the code; it breaks the problem down into manageable layers.

Here is how it works, using some creative analogies:

1. The Problem: The "Black Box" Translator

The authors tried using powerful AI models (like GPT-4o) to do the translation directly. They found that while the AI is great at understanding individual words, it often gets lost in the "big picture" logic.

The Analogy: Imagine asking a student to write a complex legal contract. If you just say, "Write the contract," the student might get the words right but mess up the order of events (e.g., saying "pay the money" before "sign the paper").
The Result: The AI often produced code that looked correct but had hidden logical traps, like missing a "wait" instruction or confusing "until" with "and."

2. The Solution: The "Onion" Strategy

To fix this, the team created a middle step called OnionL.

The Analogy: Think of a natural language requirement as an onion. It has many layers: the outer skin (the main goal), the middle layers (conditions and timing), and the core (the specific facts).
The Innovation: Instead of trying to peel the whole onion at once, the system peels it layer by layer.
1. Layer 1 (The Scope): It asks the AI, "Is this happening always? Eventually? Or only when a specific mode is active?" It builds the outer shell of the logic tree.
2. Layer 2 (The Details): It then digs deeper into each layer, breaking down complex sentences into smaller, atomic facts (like "temperature > 50" or "light is red").
3. The Result: The AI doesn't have to guess the whole structure at once. It just has to organize the layers, which is much easier for it to do correctly.

3. The Safety Net: The "Rule-Based Chef"

Once the AI has peeled the onion and organized the layers into a structured tree (the OnionL), the system passes it to a second part: a deterministic rule-based engine.

The Analogy: Think of the AI as a creative chef who chops the vegetables (the layers). The rule-based engine is a strict quality control inspector. It doesn't cook; it just checks: "Did you chop exactly two carrots? Is the knife sharp? Is the bowl clean?"
The Benefit: Because this part follows strict, unchangeable rules, it guarantees that the final code is syntactically perfect (100% correct structure). If the AI made a mistake in the layers, the inspector catches it before the final code is written.

4. The Human Safety Valve

Sometimes, the instructions are just too vague (e.g., "Do this as soon as possible"). The AI might guess wrong.

The Analogy: The system provides a visual map of the onion layers. If a human expert sees that the AI put the "wait" instruction in the wrong place, they can simply click on the map to fix it. It's like editing a flowchart rather than rewriting a whole paragraph of code.

What Did They Find?

The team tested this on real-world aerospace requirements (instructions for spacecraft navigation and control).

The Score: Their new system, REQ2LTL, got 88.4% of the meanings exactly right and 100% of the code structure correct.
Comparison: Previous methods (just asking the AI to translate directly) only got about 44% to 65% right.
Why it matters: In safety-critical fields like space travel, a 100% structural guarantee is vital. The system successfully bridged the gap between messy human language and perfect machine logic by using the "Onion" method to keep the AI focused and the rule-based engine to ensure safety.

In short, the paper claims that by breaking complex instructions into an "onion" of layers and using a strict rule-checker at the end, we can automate the creation of perfect safety codes for complex machines, something that was previously too difficult for AI to do alone.

Technical Summary: Bridging Natural Language and Formal Specification via Hierarchical Semantics Decomposition

Problem Statement
The accurate and automated translation of natural language (NL) software requirements into formal specifications, specifically Linear Temporal Logic (LTL), is a critical bottleneck for scaling formal verification in safety-critical industrial domains such as aerospace. Current industry practices rely heavily on manual translation by human experts, a process that is time-consuming and error-prone. While existing automated approaches—ranging from rule-based systems to learning-based methods—offer some automation, they face significant limitations. Rule-based methods lack flexibility and struggle with the variability of natural language, while learning-based approaches often fail to generalize beyond their training data. Furthermore, recent Large Language Models (LLMs), despite their proficiency in semantic extraction, struggle with the implicit temporal semantics, deeply nested logical structures, and context-specific constraints inherent in real-world industrial requirements. Direct application of LLMs often leads to "silent failures," where generated formulas are syntactically valid but semantically incorrect due to error compounding and a lack of structural validation.

Methodology: The REQ2LTL Framework
To address these challenges, the authors propose REQ2LTL, a modular framework that bridges NL and LTL through a novel hierarchical intermediate representation called OnionL. The framework operates via a two-stage pipeline that combines the semantic extraction capabilities of LLMs with the structural guarantees of deterministic rule-based synthesis.

Intermediate Representation (OnionL):
OnionL is a tree-structured intermediate language designed to explicitly encode temporal semantics, scopes, and logical relations. It decomposes requirements into three compositional elements:
- Atomic Propositions (APs): Predicate-level facts annotated with semantic subfields (Component, Variable, Relation, Formula).
- Scopes: Contextual boundaries corresponding to unary operators (e.g., Globally, Eventually, Next) or mode-based antecedents.
- Relations: Logical or temporal dependencies (e.g., And, Or, Implies, Until) connecting subformulas.
  This structure mirrors the compositional syntax of LTL, serving as a semantic bridge that allows LLMs to focus on local semantic parsing while delegating global logical composition to rule-based mechanisms.
Stage 1: REQ2ONIONL (Semantic Decomposition):
This module utilizes a prompt-guided LLM to transform free-form NL requirements into structured OnionL trees. It employs a specific Chain-of-Thought algorithm named BUILDING-ONIONL, which operates in two stages:
- Macro-Structure Extraction: Identifies global temporal or mode-based scopes to construct the top-level node.
- Recursive Clause Decomposition: Recursively breaks down clauses into nested scopes, relations, and normalized atomic propositions.
  The process is guided by a knowledge repository defining OnionL's recursive grammar and reinforced by few-shot examples of industrial patterns.
Stage 2: ONIONL2LTL (Rule-Based Synthesis):
This module performs a deterministic, rule-based translation of the validated OnionL tree into a standardized LTL formula.
- Validation: Before translation, the system performs a depth-first traversal to verify structural well-formedness (e.g., correct arity of operators, valid scope nesting). For safety-critical applications, the framework supports a "human-in-the-loop" mechanism where the OnionL structure is visualized (via Mermaid diagrams) for engineer inspection and correction.
- Translation: A post-order traversal converts each node into its corresponding LTL syntax (e.g., mapping Globally to $G$ , Implies to $\rightarrow$ ). This process ensures that every output is syntactically valid by construction.

Key Contributions

OnionL Intermediate Representation: A hierarchical language explicitly encoding temporal semantics and logical relations, acting as a robust semantic bridge between NL and LTL.
Hierarchical Semantic Decomposition: A two-stage, prompt-driven algorithm (BUILDING-ONIONL) that systematically decomposes requirements, significantly improving structural integrity and semantic accuracy.
REQ2LTL Framework: An automated pipeline combining LLM-based decomposition with deterministic rule-based translation and validation. It achieves superior accuracy and perfect syntactic correctness compared to existing methods.

Experimental Results
The authors evaluated REQ2LTL on both academic benchmarks (Circuit, Navigation, Office Email) and a real-world industrial dataset of 112 aerospace requirements.

Industrial Performance: On the aerospace dataset, REQ2LTL achieved 88.4% semantic accuracy (Exact Match) and 100% syntactic correctness. This significantly outperformed state-of-the-art baselines (e.g., NL2SPEC, NL2LTL, NL2TL), which struggled with nested logic and implicit temporal cues, achieving exact match rates between 55% and 65%.
Academic Performance: On academic benchmarks, REQ2LTL demonstrated consistent high performance (Binary Accuracy >94%, BLEU >0.97), generalizing effectively even in less ambiguous settings.
Ablation Studies: Experiments confirmed that the combination of structured modeling (OnionL), staged prompting, and verification feedback is essential. Removing the structured intermediate representation caused semantic accuracy to drop to 65.2%, while removing staged prompting reduced it to 58.9%.
Error Analysis: The framework effectively eliminated errors related to temporal misinterpretation, conditional confusion, and loss of nesting, which were prevalent in zero-shot and other baseline methods. Remaining errors were primarily attributed to inherent linguistic ambiguity in the input requirements.

Significance and Claims
The paper claims that REQ2LTL effectively bridges the gap between informal natural language requirements and formal specifications, providing a practical foundation for scalable adoption in safety-critical industrial systems. By introducing a structured intermediate representation and a hybrid LLM-rule-based architecture, the framework mitigates the limitations of direct LLM translation, specifically addressing the challenges of implicit temporal semantics and deep logical nesting. The authors emphasize that the framework's ability to ensure 100% syntactic correctness through rule-based synthesis, combined with high semantic fidelity, makes it a viable tool for industrial verification workflows. Additionally, the inclusion of a visualized, human-in-the-loop validation step addresses the issue of linguistic ambiguity, allowing engineers to efficiently correct semantic errors without breaking the automation pipeline. The authors note that while the current work focuses on LTL, future extensions could target more expressive temporal logics like Signal Temporal Logic (STL) and Metric Temporal Logic (MTL).