Syntax Is Easy, Semantics Is Hard: Evaluating LLMs for LTL Translation
Propositional Linear Temporal Logic (LTL) is a popular formalism for specifying desirable requirements and security and privacy policies for software, networks, and systems. Yet expressing such requirements and policies in LTL remains challenging because of its intricate semantics. Since many security and privacy analysis tools require LTL formulas as input, this difficulty places them out of reach for many developers and analysts. Large Language Models (LLMs) could broaden access to such tools by translating natural language fragments into LTL formulas. This paper evaluates that premise by assessing how effectively several representative LLMs translate assertive English sentences into LT...
| Authors | Priscilla Kyei Danso, Mohammad Saqib Hasan, Niranjan Balasubramanian et al. |
|---|---|
| Primary category | cs.LO |
| Published | 8 April 2026 |
| Last updated at source | 8 April 2026 |
Silytics shows public metadata from arXiv and links to the original. Information may be incomplete or out of date. Last refreshed 17 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.