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

Priscilla Kyei Danso; Mohammad Saqib Hasan; Niranjan Balasubramanian; Omar Chowdhury

cs.LOApr 8, 2026

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

Authors: Priscilla Kyei Danso, Mohammad Saqib Hasan, Niranjan Balasubramanian, Omar Chowdhury

Organizations: Stony Brook University, Stony Brook, USA

Abstract

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 LTL formulas. Using both human-generated and synthetic ground-truth data, we evaluate effectiveness along syntactic and semantic dimensions. The results reveal three findings: (1) in line with prior findings, LLMs perform better on syntactic aspects of LTL than on semantic ones; (2) they generally benefit from more detailed prompts; and (3) reformulating the task as a Python code-completion problem substantially improves overall performance. We also discuss challenges in conducting a fair evaluation on this task and conclude with recommendations for future work.

Figures & tables

RQ	Task	Input	Output	Metric	Dataset	Size	Interfaces	Oracle
RQ ${}_{\text{syn}}^{1}$	Atomic proposition extraction	NL	AP set	Levenshtein, Jaccard	$\mathbb{DS}^{\mathsf{prop}}_{\mathbf{5}}$	144	Minimal, Detailed	Manual
RQ ${}_{\text{syn}}^{2}$	Well-formedness	LTL	Yes/No	Accuracy, F1	$\mathbb{DS}^{\mathsf{syntax}}_{\mathbf{6}}$	299	Minimal, Detailed	Grammar
RQ ${}_{\text{sem}}^{1}$	NL $\rightarrow$ Future LTL	NL + AP	LTL	Equiv., Entail.	$\mathbb{DS}^{\mathsf{tricky}}_{\mathbf{1}}$ , $\mathbb{DS}^{\mathsf{book}}_{\mathbf{3}}$	306, 141	Minimal, Detailed, Python	NuSMV
RQ ${}_{\text{sem}}^{2}$	Trace classification	LTL + trace	Yes/No	Accuracy, F1	$\mathbb{DS}^{\mathsf{trace}}_{\mathbf{4}}$	306	Minimal, Detailed, Python	NuSMV
RQ ${}_{\text{sem}}^{3}$	Trace generation	LTL	$(\tau^{+}/\tau^{-})$	Trace satisfaction	$\mathbb{DS}^{\mathsf{trace}}_{\mathbf{4}}$	306	Minimal, Detailed, Python	NuSMV
RQ ${}_{\text{sem}}^{4}$	NL $\rightarrow$ Past LTL	NL + AP	Past-LTL	Equiv., Entail.	$\mathbb{DS}^{\mathsf{pastltl}}_{\mathbf{2}}$	294	Minimal, Detailed, Python	NuSMV

Table 1. Task–evaluation mapping across experiments, research questions, datasets, and interfaces.

Figure 1. Performance per model and interface (precision, recall, F1-score, Jaccard similarity, Levenshtein similarity) for Atomic Proposition Extraction. Line chart comparing Detailed vs. Minimal interface performance across F1, precision, recall, Jaccardi, and Levenshtein metrics.

Figure 2. Detailed vs. Minimal Interface performance. Accuracy represents the fraction of correctly classified formulas. Precision and Recall measure soundness and completeness, respectively. FPR and FNR denote the rates of incorrectly accepted malformed formulas and incorrectly rejected well-formed formulas. Heatmap of Detailed vs. Minimal Interface performance.

Figure 3. Semantic performance of NL $\rightarrow$ LTL translation evaluated via bidirectional entailment. Equiv. denotes semantic equivalence ( $\varphi_{\mathit{GT}}\Leftrightarrow\varphi_{\mathit{Pred}}$ ), Sound. denotes ground-truth-to-prediction entailment ( $\varphi_{\mathit{GT}}\Rightarrow\varphi_{\mathit{Pred}}$ ), Compl. denotes prediction-to-ground-truth entailment ( $\varphi_{\mathit{Pred}}\Rightarrow\varphi_{\mathit{GT}}$ ), and Syntax reports well-formed LTL outputs. Heatmap of Detailed vs. Minimal vs. Python Interface performance of NL$\rightarrow$LTL translation. — Figure 3. Semantic performance of NL $\rightarrow$ LTL translation evaluated via bidirectional entailment. Equiv. denotes semantic equivalence ( $\varphi_{\mathit{GT}}\Leftrightarrow\varphi_{\mathit{Pred}}$ ), Sound. denotes ground-truth-to-prediction entailment ( $\varphi_{\mathit{GT}}\Rightarrow\varphi_{\mathit{Pred}}$ ), Compl. denotes prediction-to-ground-truth entailment ( $\varphi_{\mathit{Pred}}\Rightarrow\varphi_{\mathit{GT}}$ ), and Syntax reports well-formed LTL outputs. Heatmap of Detailed vs. Minimal vs. Python Interface performance of NL $\rightarrow$ LTL translation.

Dataset	Equiv.	Sound.	Compl.	Syntax
Little Tricky Logic	23.9%	33.7%	31.8%	48.7%
Textbook	24.8%	35.2%	31.3%	50.0%

Table 2. Semantic and syntactic correctness of predicted LTL formulas by dataset. ( Equiv. ) is the logical equivalence between the predicted and ground truth formulas (

\varphi_{\text{pred}}\equiv\varphi_{\text{gt}}

). ( Sound. ) holds when the ground truth formula entails the generated formula (

\varphi_{\text{gt}}\models\varphi_{\text{pred}}

), while ( Compl. ) holds when the predicted formula entails the predicted formula (

\varphi_{\text{pred}}\models\varphi_{\text{gt}}

). Syntax is the percentage of syntactically valid LTL formulas.

Interface	True Sat.	False Sat.	True Viol.	False Viol.	Sound.	Compl.
Minimal	56.1%	43.9%	59.0%	41.0%	56.1%	59.0%
Detailed	64.3%	35.7%	71.2%	28.8%	64.3%	71.2%
Python	78.0%	22.0%	81.3%	18.7%	78.0%	81.3%

Table 3. Classification outcomes for satisfying and violating traces. ( True Sat. ) denotes correctly accepted satisfying traces, while ( False Sat. ) denotes satisfying traces incorrectly rejected. ( True Viol. ) denotes correctly rejected violating traces, while ( False Viol. ) denotes violating traces incorrectly accepted. ( Sound. ) corresponds to acceptance accuracy on satisfying traces, and ( Compl. ) corresponds to rejection accuracy on violating traces. Results are aggregated by interface type.

Figure 4. Trace generation results on Little Tricky Logic dataset ( Greenman et al., 2022 ) for different interfaces. Line Chart of Detailed vs. Minimal vs. Python Interface performance of Trace generation.

RQ	Task	$\mathcal{M}$ (Minimal Interface)	$\mathcal{D}$ (Detailed Interface)	$\mathcal{P}$ (Python Interface)
$\text{RQ}_{\text{syn}}^{1}$	Atomic Proposition Extraction	$J=\textbf{0.83}$ ( Claude-3-Sonnet )	$J=\textbf{0.86}$ (+3.61%) ( Gemini-1.5-Flash )	N/A
		$L_{d}=\textbf{3.66}$ ( Claude-3-Sonnet )	$L_{d}=\textbf{3.05}$ (-16.67%) ( Gemini-1.5-Flash )
$\text{RQ}_{\text{syn}}^{2}$	LTL Well-Formedness Validation	Acc= 52.19% (Avg.)	Acc= 84.33% ( $\Delta_{\text{acc}}=+10.86\%$ ) ( Gemini-1.5-Flash )	N/A
		$F_{1}=\textbf{57.96\%}$ (Avg.)	$F_{1}=\textbf{85.08\%}$ ( $\Delta_{F_{1}}=+17.87\%$ ) ( Gemini-1.5-Flash )
			$\epsilon_{r}=\textbf{20.4\%}$ (Total Reduction)
$\text{RQ}_{\text{sem}}^{1}$	NL $\to$ Future LTL Generation	$\text{Equiv}=\textbf{65.56\%}$ ( Gemini-1.5-Flash )	$\text{Equiv}=\textbf{64.75\%}$ ( Claude-3-Sonnet )	$\text{Equiv}=\textbf{72.13\%}$ ( Claude-3-Sonnet )

Table 4. Summary of Key Findings

Figure 5. Semantic performance of NL

\rightarrow

LTL (Past) translation evaluated via bidirectional entailment. Equiv. denotes semantic equivalence (

\varphi_{\mathit{GT}}\Leftrightarrow\varphi_{\mathit{Pred}}

), Sound. denotes ground-truth-to-prediction entailment (

\varphi_{\mathit{GT}}\Rightarrow\varphi_{\mathit{Pred}}

), Compl. denotes prediction-to-ground-truth entailment (

\varphi_{\mathit{Pred}}\Rightarrow\varphi_{\mathit{GT}}

), and Syntax reports well-formed LTL outputs. Bar chart comparing Detailed vs. Minimal vs. Python interface performance of NL

\rightarrow

LTL (Past) translation evaluated via bidirectional entailment and semantic equivalence.

Condition	Approach	Equiv.	Sound.	Compl.	Prec.	Recall	F1
With AP	Few-shot	37.50	46.88	58.82	37.50	46.88	41.67
	Zero-shot	53.12	65.62	64.71	53.12	65.62	58.72
	Self-refine	59.38	62.50	70.59	59.38	62.50	60.90
No AP	Few-shot	44.44	61.11	46.51	44.44	61.11	51.46
	Zero-shot	47.22	61.11	44.19	47.22	61.11	53.28
	Self-refine	40.00	51.43	42.86	40.00	51.43	45.00

Table 5. Security dataset results: Comparing AP vs. No AP + manual alignment.

Condition	Approach	Equiv.	Sound.	Compl.	Prec.	Recall	F1
With AP	Few-shot	53.85	71.15	67.31	53.85	71.15	61.30
	Zero-shot	46.30	72.22	53.70	46.30	72.22	56.42
	Self-refine	50.94	77.36	58.49	50.94	77.36	61.43
No AP	Few-shot	48.08	65.38	55.77	48.08	65.38	55.41
	Zero-shot	48.08	69.23	57.69	48.08	69.23	56.75
	Self-refine	49.02	70.59	60.78	49.02	70.59	57.86

Table 6. Matched baseline results from

\mathbb{DS}^{\mathsf{tricky}}_{\mathbf{1}}

on 56 samples

Appendix figures & tables17 assets

Supplementary material from the paper’s appendix.

Appendix

		Minimal Interface						Detailed Interface
Model	App.	Acc	Prec	Rec	F1	FPR	FNR	Acc	Prec	Rec	F1	FPR	FNR
C-Sonnet	FS	54.5	58.5	32.0	41.4	22.8	68.0	80.0	87.5	70.0	77.8	10.0	30.0
	ZS	55.9	58.7	40.7	48.0	28.9	59.3	77.7	86.7	65.3	74.5	10.0	34.7
	ZS-SR	55.5	66.0	23.3	34.5	12.1	76.7	77.3	95.6	57.3	71.7	2.7	42.7
Gemini	FS	52.5	55.3	28.0	37.2	22.8	72.0	84.3	81.2	89.3	85.1	20.7	10.7
	ZS	49.2	48.8	26.0	33.9	27.5	74.0	76.0	81.5	67.3	73.7	15.3	32.7

Appendix

Table 7.

\mathbb{RQ}^{\mathsf{syn}}_{\mathbf{1}}

: Well-formed Classification - Comprehensive Model Performance Results

		Minimal Interface						Detailed Interface
Model	Approach	Acc	Prec	Rec	F1	FPR	FNR	Acc	Prec	Rec	F1	FPR	FNR
Claude-Sonnet	Few-shot	54.52	58.54	32.00	41.38	22.82	68.00	80.00	87.50	70.00	77.78	10.00	30.00
	Zero-shot	55.85	58.65	40.67	48.03	28.86	59.33	77.67	86.73	65.33	74.52	10.00	34.67
	Zero-shot SR	55.52	66.04	23.33	34.48	12.08	76.67	77.33	95.56	57.33	71.67	2.67	42.67
Gemini	Few-shot	52.51	55.26	28.00	37.17	22.82	72.00	84.33	81.21	89.33	85.08	20.67	10.67
	Zero-shot	49.16	48.75	26.00	33.91	27.52	74.00	76.00	81.45	67.33	73.72	15.33	32.67

Appendix

Table 8.

\mathbb{RQ}^{\mathsf{syn}}_{\mathbf{2}}

:Atomic Proposition Extraction - Classification Performance Metrics Across Models and Approaches

	Minimal Interface						Detailed Interface
Model	Prec	Rec	F1	Jaccard	Lev.	Matched	Prec	Rec	F1	Jaccard	Lev.	Matched
Gemini	81.88	77.00	78.74	67.57	89.16	758/1023	82.56	79.14	79.81	68.75	91.56	772/1023
GPT-4o	79.80	76.04	77.38	63.60	86.97	745/1023	84.09	79.96	81.20	71.74	90.68	785/1023
GPT-4o-Mini	76.22	73.39	74.18	58.20	85.15	724/1023	81.92	77.67	79.05	68.32	89.60	758/1023
Claude-Sonnet	74.46	71.06	71.97	57.38	83.77	709/1023	83.70	79.48	80.75	70.41	89.71	780/1023
GPT-3.5-Turbo	26.53	24.39	25.05	19.07	30.54	239/1023	80.24	76.81	77.63	65.64	88.32	757/1023

Appendix

Table 9.

\mathbb{RQ}^{\mathsf{syn}}_{\mathbf{2}}

:Atomic Proposition Extraction - Metrics by Model (Proposition Phrase Matching)

SR = Self-Refine, Lev. = Levenshtein Similarity. All values are percentages.
	Minimal Interface					Detailed Interface
Approach	Prec	Rec	F1	Jaccard	Lev.	Prec	Rec	F1	Jaccard	Lev.
Few-shot	66.41	62.99	64.05	51.88	73.73	85.17	80.82	82.14	72.26	91.00
Zero-shot	66.39	63.19	64.20	52.33	73.20	81.17	77.44	78.44	67.35	89.41
Zero-shot Self-Refine	70.54	66.95	68.15	55.28	78.43	81.16	77.56	78.48	67.30	89.51

Appendix

Table 10.

\mathbb{RQ}^{\mathsf{syn}}_{\mathbf{2}}

:Atomic Proposition Extraction - Metrics by Approach

	Minimal Interface		Detailed Interface
Error Type	Count	%	Count	%
Semantic Mismatch	588	55.3	521	64.6
Complete Failure	275	25.9	9	1.1
Partial Extraction	179	16.8	235	29.1
Over Extraction	21	2.0	42	5.2
Total Errors	1063	100.0	807	100.0

Appendix

Table 11.

\mathbb{RQ}^{\mathsf{syn}}_{\mathbf{2}}

:Atomic Proposition Extraction - Error Type Distribution

		Equivalence Analysis				Performance Metrics
Model	Approach	Interface	Equiv	Not-Eq	N/M	Eq-Acc%	Syn.Corr%	Prec%	F1%
Claude-Sonnet	Few-shot	Detailed	235	182	458	28.27	49.49	28.27	28.27
	Few-shot	Minimal	154	207	430	20.71	46.70	20.71	20.71
	Few-shot	Python	269	145	456	33.29	47.73	33.29	33.29
	Zero-shot	Detailed	239	171	464	29.87	49.51	29.87	29.87
	Zero-shot	Minimal	151	187	459	22.02	47.65	22.02	22.02

Appendix

Table 12.

\mathbb{RQ}^{\mathsf{sem}}_{\mathbf{1}}

\mathtt{NL}\!\!\!\rightarrow\!\!\mathtt{LTL}

(Future) generation - Equivalence and Performance Metrics

All values are percentages. Averages computed across all models and approaches.
Interface	Soundness	Completeness	Eq-Acc	Syn.Corr	Precision	F1
Python	62.45	55.83	46.21	69.81	46.21	46.21
Detailed	47.89	44.52	32.11	76.28	32.11	32.11
Minimal	48.27	45.96	31.85	75.68	31.85	31.85

Appendix

Table 13.

\mathbb{RQ}^{\mathsf{sem}}_{\mathbf{1}}

\mathtt{NL}\!\!\!\rightarrow\!\!\mathtt{LTL}

(Future) generation - Average Performance by Interface Type

Abbreviation	Full Name
Yes/No/N/M	Entailment: Yes / No / Not Meaningful
Sound.	Soundness (percentage)
Compl.	Completeness (percentage)
Equiv	Equivalent
Not-Eq	Not Equivalent
Eq-Acc	Equivalence Accuracy (percentage)

Appendix

Table 14. Abbreviations for Entailment Analysis Tables

		Python Interface			Detailed Interface			Minimal Interface
Model	Approach	Acc	Prec	F1	Acc	Prec	F1	Acc	Prec	F1
Gemini-Pro	Few-shot	69.08	71.50	68.18	—	—	—	—	—	—
	Zero-shot	69.19	71.49	68.36	—	—	—	—	—	—
	ZS-SR	64.54	68.07	62.75	—	—	—	—	—	—
Gemini-Flash	Few-shot	70.31	73.73	69.15	73.04	73.38	72.94	76.00	77.60	75.60
	Zero-shot	70.31	73.47	69.12	72.55	72.94	72.43	71.60	72.00	71.40

Appendix

Table 15.

\mathbb{RQ}^{\mathsf{sem}}_{\mathbf{2}}

: Trace Characterization Performance Across Interfaces

Interface	Avg Accuracy	Avg Precision	Avg F1	Models Tested
Python	75.46	77.79	73.56	4
Detailed	66.36	67.10	65.41	5
Minimal	61.31	64.47	59.33	5
Averages computed across all model-approach combinations for each interface.

Appendix

Table 16.

\mathbb{RQ}^{\mathsf{sem}}_{\mathbf{2}}

: Average Trace Characterization Performance by Interface

		Python Interface				Detailed Interface				Minimal Interface
Model	Approach	Acc	Prec	F1	Err%	Acc	Prec	F1	Err%	Acc	Prec	F1	Err%
Claude-Sonnet	Few-shot	75.49	79.92	73.53	17.60	74.51	80.24	71.84	16.83	62.42	64.07	60.07	20.59
	Zero-shot	73.36	77.73	71.07	21.22	73.69	77.78	71.60	19.12	54.25	54.48	53.02	25.49
	ZS-SR	74.51	78.33	72.66	19.41	72.71	76.43	70.65	19.44	57.03	57.24	56.39	22.88
Gemini-Flash	Few-shot	69.74	72.90	67.49	22.20	72.06	76.26	69.63	16.99	65.52	67.15	63.81	24.67
	Zero-shot	56.91	57.55	54.98	30.76	67.97	69.93	66.32	23.86	68.14	70.79	65.97	21.90

Appendix

Table 17.

\mathbb{RQ}^{\mathsf{sem}}_{\mathbf{3}}

: Trace Generation - Performance Comparison Across Interfaces

All values are percentages. Averages computed across all models and approaches.
Interface	Avg Acc	Avg Prec	Avg F1	Avg Pos.Sat	Avg Err%
Python	68.92	71.30	67.02	62.61	23.47
Detailed	66.17	68.66	64.61	61.50	21.53
Minimal	58.88	60.72	57.13	54.41	22.71

Appendix

Table 18.

\mathbb{RQ}^{\mathsf{sem}}_{\mathbf{3}}

: Trace Generation - Average Trace Generation Performance by Interface

Model	Avg Accuracy	Avg Precision	Avg F1
Claude-Sonnet	66.47	68.35	63.75
Gemini-Flash	66.37	68.53	64.68
GPT-4o	66.36	69.45	63.38
Gemini-2.5-Flash	71.93	75.39	69.94
GPT-4o-Mini	60.58	61.61	58.66
Gemini-Pro	65.90	67.82	63.96

Appendix

Table 19.

\mathbb{RQ}^{\mathsf{sem}}_{\mathbf{3}}

: Trace Generation - Model Ranking by Average Accuracy

		Equivalence Analysis				Performance Metrics
Model	Approach	Interface	Equiv	Not-Eq	N/M	Eq-Acc%	Syn.Corr%	Prec%	F1%
Claude-Sonnet	Few-shot	Detailed	184	93	285	33.21	49.47	33.21	33.21
	Few-shot	Minimal	135	103	287	28.36	42.96	28.36	28.36
	Few-shot	Python	178	98	288	32.25	49.47	32.25	32.25
	Zero-shot	Detailed	193	84	287	34.84	49.82	34.84	34.84
	Zero-shot	Minimal	93	95	322	24.73	40.14	24.73	24.73

Appendix

Table 20.

\mathbb{RQ}^{\mathsf{sem}}_{\mathbf{4}}

\mathtt{NL}\!\!\!\rightarrow\!\!\mathtt{LTL}

(Past) generation - Equivalence and Performance Metrics

All values are percentages. Averages computed across all models and approaches (excluding zero-result rows).
Interface	Soundness	Completeness	Eq-Acc	Syn.Corr	Precision	F1
Python	64.07	60.39	52.59	71.12	52.59	52.59
Detailed	58.16	58.76	45.49	71.68	45.49	45.49
Minimal	58.16	58.33	43.92	68.69	43.92	43.92

Appendix

Table 21.

\mathbb{RQ}^{\mathsf{sem}}_{\mathbf{4}}

\mathtt{NL}\!\!\!\rightarrow\!\!\mathtt{LTL}

(Past) generation - Average Performance by Interface for Past NL→LTL Generation

Model	Avg Eq-Acc	Avg Soundness	Avg Completeness
Gemini-2.5-Flash	71.69	84.80	82.64
Gemini-Pro	69.40	83.07	79.52
GPT-4o	63.40	77.78	79.75
GPT-4o-Mini	59.59	77.72	74.93
GPT-3.5-Turbo	38.99	60.68	66.47
Claude-Sonnet	30.58	38.72	39.05

Appendix

Table 22.

\mathbb{RQ}^{\mathsf{sem}}_{\mathbf{4}}

\mathtt{NL}\!\!\!\rightarrow\!\!\mathtt{LTL}

(Past) generation - Model Ranking by Average Equivalence Accuracy

Model	Provider	Version/Checkpoint	API Endpoint
Claude-3-Sonnet	Anthropic	claude-3-sonnet-20240229	claude.anthropic.com
Claude-3.5-Sonnet	Anthropic	claude-3-5-sonnet-20241022	claude.anthropic.com
Claude-4.5-Sonnet	Anthropic	claude-sonnet-4-5-20250929	claude.anthropic.com
Gemini-1.5-Pro	Google	gemini-1.5-pro-001	google.generativeai.google.com
Gemini-1.5-Flash	Google	gemini-1.5-flash-001	google.generativeai.google.com
Gemini-2.5-Flash	Google	gemini-2.5-flash-001	google.generativeai.google.com

Appendix

Table 23. LLM Models Evaluated With Details and Access Information

Explore similar work

May 20, 2026

NeuroNL2LTL: A Neurosymbolic Framework for Natural Language Translation of Linear Temporal Logic

Effectively translating between natural language (NL) and formal logics like Linear Temporal Logic (LTL) requires expertise that limits formal verification's reach in safety-critical development. Template-based approaches sacrifice expressiveness for reliability; neural methods achieve fluency but provide no correctness guarantees. We present NeuroNL2LTL, a neurosymbolic architecture unifying learned translation with formal verification. NeuroNL2LTL routes translation through an intermediate representation whose mapping to LTL is structure-preserving by construction. Generated specifications undergo satisfiability and non-triviality checking; a minimal-edit repair mechanism corrects near-miss outputs before they reach downstream tools. The central innovation is verifier-in-the-loop training: verification outcomes serve as reward signals for reinforcement learning, producing neural components that optimize directly for formal correctness. On 200,000+ requirements spanning aerospace, robotics, autonomous vehicles, and ten additional domains, NeuroNL2LTL achieves 28% semantic equivalence with reference specifications while ensuring 86% of outputs are verified satisfiable. The system also generates contextually grounded explanations from LTL, enabling domain experts to validate specifications without specialized training. This work demonstrates that formal verification can function as both training objective and runtime filter for neural specification systems, allowing us to build neural-based tools whose reliability derives from logical guarantees rather than statistical confidence.

Paapa Kwesi Quansah, Ernest Bonnah

Baylor University, Waco TX 76706, USA

Formal Verification Neuro-Symbolic AI Linear Temporal Logic

Ask PDF

Aug 3, 2026

Infinite Trace Objectives with Finite Trace Techniques: Translating LTL to LTLf+

Linear Temporal Logic (LTL) is one of the most widely adopted languages for specifying temporal extended objectives in AI, with applications ranging from reactive synthesis to stochastic planning in Markov decision processes and reinforcement learning. Traditionally, solving any of these problems requires translating the LTL specification to a nondeterministic automata on infinite words and then determinizing it, a step that is notoriously difficult in theory and in practice. Recent work has introduced LTLf+, which lifts the finite-trace logic LTLf to infinite traces. LTLf+ has the same expressive power as LTL, yet it retains most of the crucial advantages of its base logic LTLf. Most reasoning in LTLf+ rests on finite automata on finite words, for which we have not only a canonical minimal representation but also an efficient determinization procedure. In this work we present the first translation from LTL to LTLf+. We first normalize an LTL formula into the syntactic reactivity fragment of the Manna-Pnueli hierarchy, to create the general fragment-based shape of LTLf+. We then present linear translations for each individual component of that fragment. As a consequence of this translation, the expanding body of techniques developed for LTLf+ now becomes available to many AI problems currently formulated in LTL. We further show that this comes at no asymptotic cost, as the pipeline from LTL to automaton via LTLf+ remains doubly exponential.

Christoph Weinhuber, Maximilian Prokop, Giuseppe De Giacomo +1

University of Oxford · 2Technical University of Munich · 3Masaryk University Brno +1

Temporal Reasoning Formal Verification Linear Temporal Logic

Ask PDF

Mar 5, 2026

LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoning

Translating informal requirements into formal specifications is challenging due to the ambiguity and variability of natural language (NL). This challenge is particularly pronounced when relying on compact (small and medium) language models, which may lack robust knowledge of temporal logic and thus struggle to produce syntactically valid and consistent formal specifications. In this work, we focus on enabling resource-efficient open-weight models (4B--14B parameters) to generate correct linear temporal logic (LTL) specifications from informal requirements. We present LTLGuard, a modular toolchain that combines constrained generation with formal consistency checking to generate conflict-free LTL specifications from informal input. Our method integrates the generative capabilities of model languages with lightweight automated reasoning tools to iteratively refine candidate specifications, understand the origin of the conflicts and thus help in eliminating inconsistencies. We demonstrate the usability and the effectiveness of our approach and perform quantitative evaluation of the resulting framework.

Medina Andresel, Cristinel Mateis, Dejan Nickovic +3

AIT Austrian Institute of Technology, Vienna, Austria · Aristotle University of Thessaloniki, Thessaloniki, Greece · Northeatern University, Boston, MA, USA

Autoformalization Linear Temporal Logic Formal Verification Constrained Generative Modeling

Ask PDF