Generating and Verifying LTL Specifications from Natural Language Requirements
| Forschungsthema: | Formal Methods and Requirements Engineering |
|---|---|
| Typ: | SA |
| Datum: | 2025-10-01 |
| Betreuer: |
Tianhai Liu Andreas Bremer |
| Aushang: |
Generating and Verifying LTL Specifications from Natural Language Requirements
Abstract
Natural language requirements are widely used in practice, but they are often ambiguous, incomplete, or inconsistent. Formal specifications, such as Linear Temporal Logic (LTL), enable rigorous verification but are difficult to write manually.
This project investigates techniques for automatically translating natural language requirements into LTL specifications and verifying their correctness. The work may include the use of large language models (LLMs) to extract structured intent models, the transformation of these models into LTL formulas, and the application of formal verification tools (e.g., model checking or realizability checking) to validate the resulting specifications.
A particular focus may be placed on detecting inconsistencies between requirements, identifying unrealizable specifications, and suggesting automated repairs.
Literature
- ConformalNL2LTL: Translating Natural Language Instructions into Temporal Logic Formulas with Conformal Correctness Guarantees (2025)
- Req2LTL: Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs (2025)
- GinSign: Grounding Natural Language Into System Signatures for Temporal Logic Translation (2025)