Source-linked AI summary
A note on the reduction from LTLf to LTL
Alexandre Duret-Lutz
TL;DR
The original LTLf-to-LTL reduction preserves finite-word satisfaction but does not generally produce formulas in the syntactic Obligation fragment. The paper revises the translation by separating Guarantee, Safety, and Obligation construction, ensuring syntactic LTLO membership while preserving alive-position equivalence and satisfiability behavior.
Problem
The original reduction yields LTL formulas denoting obligation properties but generally fails to produce formulas in the syntactic Obligation fragment.
Method
The revised translation introduces class-specific functions and uses them in the syntactic contexts requiring Guarantee, Safety, or Obligation formulas.
Results
For every LTLf formula f, tO(f) belongs to LTLO and is equivalent to the original translation at alive positions.
Takeaways & Limitations
The corrected reduction enables algorithms specialized to syntactic Obligation formulas to be applied to LTLf formulas.
Takeaways & Limitations
The original wrapper and inner translation are generally outside LTLO, requiring the revised construction to address both issues.
Abstract
from arXiv · showhide
LTLf, a finite word variant of LTL, can be reduced to LTL by introducing a new atomic proposition indicating the prefix of the infinite words that correspond to the finite words that the original LTLf formula was considering. Such a reduction was originally proposed by De Giacomo and Vardi (IJCAI'13). However, while any LTL formula reduced from LTLf describes an obligation property in the hierarchy of Manna and Pnueli (PODC'90), the aforementioned reduction does not provide an LTL formula that belongs to the syntactic obligation fragment of LTL. This note shows how the reduction was fixed in Spot in order to ensure that the resulting LTL formula is always a syntactic obligation. Doing so allows algorithms specialized to syntactic obligation to be used on LTLf formulas. For instance, in previous work (CAV'26) we described a specialized translation from syntactic obligations to minimal, weak, deterministic Büchi automata that would not be usable with the original reduction.
1 Preliminaries
The paper introduces the relevant LTL and LTLf semantics and recalls the syntactic hierarchy, focusing on the Bottom, Guarantee, Safety, and Obligation fragments. It also defines alive encodings and equivalence at alive positions for relating finite-word formulas to infinite-word formulas.
- LTLf semantics: LTLf interprets temporal operators over nonempty finite words, with strong operators requiring their promises before the word ends.Weak next is vacuously true at the last position, whereas strong next requires a next position.
- Syntactic hierarchy: The syntactic hierarchy classifies LTL formulas into Safety, Guarantee, Obligation, Persistence, Recurrence, and Reactivity classes.The paper uses grammars for the fragments most relevant to its reduction.
- Syntactic fragments: LTLB contains propositional formulas plus X, while LTLG and LTLS restrict weak and strong temporal operators, respectively.LTLG excludes G, W, and R; LTLS excludes F, U, and M.
- Syntactic fragments: LTLO extends LTLG and LTLS through Boolean connectives, X, and four mixed temporal operators.The mixed operators are φO U φG, φO R φS, φS W φO, and φG M φO.
- Alive encoding: An alive encoding marks the live prefix of an infinite word with alive, leaving positions from the finite-word end onward dead.The encoding applies to nonempty finite words.
- Alive-position equivalence: Two LTL formulas are equivalent at alive positions when they agree at every alive position of every conforming alive-encoded word.This relation is denoted ψ1 ≡fin ψ2.
2 The Original Reduction from LTLf to LTL
The original reduction injects live-prefix constraints into an LTL translation and preserves finite-word satisfaction on alive-encoded words. However, its wrapper and recursively translated formula are generally outside the syntactic Obligation fragment, motivating the revised construction.
- Reduction definition: The original reduction preserves satisfaction: an alive-encoded infinite word satisfies the translated formula exactly when its finite prefix satisfies the LTLf formula.Consequently, satisfiability over alive-encoded words corresponds to satisfiability over nonempty finite words.
- Reduction definition: The translation is homomorphic for Boolean operators and atomic propositions, while temporal operators receive live-prefix constraints.Strong operators require alive target positions, whereas weak operators permit dead positions as a trivial escape.
- Implementation: The implementation used these translation rules for Spot's from_ltlf function from version 2.2.2 through version 2.15.1.
- Problems with the original reduction: The original output is generally not syntactically Obligational despite always denoting an obligation property in the Manna–Pnueli hierarchy.The paper identifies two issues: the wrapper is not in LTLO, and the inner translation t(f) is generally not in LTLO.
- Problems with the original reduction: The wrapper alive U G¬alive is a Persistence formula rather than an LTLO formula, although it has an equivalent LTLO form on alive-encoded words.The replacement is F¬alive ∧ (alive W G¬alive).
- Problems with the original reduction: The inner translation fails structurally because one recursive function is used in both Guarantee and Safety contexts, producing mixed-class formulas.For example, translations of G(Fa) and F(Ga) are generally not in LTLO.
3 The New Reduction from LTLf to Syntactic Obligation
The revised reduction uses mutually recursive translations to preserve alive-position equivalence while ensuring the resulting formulas belong to the appropriate syntactic fragments, especially LTLO. A corrected wrapper completes the construction without changing satisfiability behavior on alive-encoded words.
- Translation framework: The translation defines tG, tS, and tO, with tB as an auxiliary restriction, and establishes their syntactic-class and equivalence invariants by structural induction.tG produces LTLG, tS produces LTLS, and tO produces LTLO while remaining equivalent to the original translation at alive positions.
- Revised top-level wrapper: The revised wrapper replaces alive U G¬alive with an equivalent LTLO expression on alive-encoded words.The replacement is F¬alive ∧ (alive W G¬alive), which avoids the original wrapper’s syntactic-class violation.
- The function tG: tG handles constrained LTLG contexts by converting weak operators to U-based forms and using tS where an LTLS subformula is required.Examples include G f encoded as tG(f) U ¬alive and f U g encoded as tG(f) U (alive ∧ tG(g)).
- The function tS: tS is dual to tG: it produces LTLS formulas by converting strong temporal operators to R-based forms and using tG for required LTLG subformulas.For the key case F f, tS(f) R alive matches the finite-prefix semantics because the live prefix eventually ends.
- The function tO: tO is the main translation, treating Boolean operators homomorphically and selecting tG or tS for constrained temporal operands while recursing with tO elsewhere.Its rules preserve membership in LTLO, including for U, R, W, and M.
- Correctness: Structural induction proves syntactic-class membership and alive-position equivalence, while the corrected wrapper preserves the original translation’s satisfiability behavior.The proof covers the mutually recursive translations and establishes tO(f) ≡fin t(f) at every alive position.
4 Availability in Spot
The new from_ltlf function is implemented in Spot for the upcoming 2.16 release, while the old reduction remains available through an environment variable.
- The new from_ltlf function has been implemented in Spot and is intended for the upcoming Spot 2.16 release.
- In the example, the new reduction produces a result that passes the syntactic-obligation check.
- The old reduction can still be selected in Spot 2.16 by setting SPOT_FROM_LTLF to 0.
- With the old reduction enabled, the example's result is not a syntactic obligation.