Syntax Is Easy, Semantics Is Hard: Evaluating LLMs for LTL Translation

ArXi:2604.07321v1 Announce Type: cross 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.