Automated LTL Specification Generation from Industrial Aerospace Requirements
Zhi Maa, Xiao Lianga, Cheng Wenb, Rui Chenc d, Bin Guc, Shengchao Qina e, Cong Tiana, Mengfei Yangd
- aSchool of Computer Science and Technology , Xidian University , Xi'an , China
- bBeijing Sunwise Information Technology Ltd , China
- cBeijing Institute of Control Engineering , Beijing , China
- dChina Academy of Space Technology , Beijing , China
- eGuangzhou Institute of Technology , Xidian University , Guangzhou , China
Papers open inside SciRah from the original publisher or repository; SciRah never hosts them.
Abstract
In the development and verification of safety-critical aero-space software, Linear Temporal Logic (LTL) has been widely used to specify complex system properties derived from requirements. However, a significant gap remains in industrial practice: translating natural language (NL) requirements into formal LTL properties is a labor-intensive and error-prone process that requires rare expertise in both aerospace control engineering and formal methods. While recent NL-to-LTL tools (e.g., NL2SPEC, NL2TL, NL2LTL) are capable of automating parts of this process, they often fail on real requirement documents in industrial settings, due to complex domain terminology or implicit temporal and logical structure. To address these challenges, we present AeroReq2LTL, a framework that automates LTL property generation for aerospace requirements using large language models (LLMs), with two key industrial innovations: (i) a data dictionary that normalizes technical jargon into precise atomic propositions; and (ii) a template-based requirement language that makes temporal cues and logical relations explicit before translation. On a real aerospace dataset, AeroReq2LTL achieves 85% precision and 88% recall in LTL generation, and its outputs can be directly consumed by existing verification tools.
TL;DRAeroReq2LTL is presented, a framework that automates LTL property generation for aerospace requirements using large language models (LLMs), with two key industrial innovations: a data dictionary that normalizes technical jargon into precise atomic propositions and a template-based requirement language that makes temporal cues and logical relations explicit before translation. (Semantic Scholar)