LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces

1 Introduction

Reactive synthesis is concerned with synthesizing programs (aka, strategies) for reactive computations (e.g., processes, protocols, controllers, robots) in active environments [Pnueli and Rosner, 1989; Finkbeiner, 2016; Ehlers et al., 2017], typically from temporal logic specifications. The most common specification language is possibly Linear Temporal Logic (LTL) [Pnueli, 1977]. The basic techniques for reactive synthesis share several similarities with Model Checking, and are based on the connections between Logics, Automata, and Games [Fijalkow and others, 2023]. Indeed, Reactive Synthesis for LTL involves the following Steps: (i) having a specification φ of the desired system behavior in LTL, in which one distinguishes controllable and uncontrollable variables; (ii) extracting from the specification an equivalent automaton on infinite words, corresponding to the infinite traces satisfying φ; (iii) (differently fromModel Checking) determinizing the automaton to obtain an arena for a game between the system and the environment; (iv) solving the game, by fixpoint computation, for an objective determined by the automaton's accepting condition (e.g., a parity objective for LTL), yielding a strategy for the system that fulfills the original specification.

Model Checking is mature, and its techniques may be exploited in Reactive Synthesis as well, including symbolic techniques based on Boolean encodings to compactly represent the game arena and compute fixpoints over it. However, despite this, LTL synthesis has lagged behind since the required determinization in Step (iii) remains a major performance obstacle: determinizing nondeterministic B¨uchi automata (NBA) is notoriously difficult [Vardi, 2007].

At first glance, the difficulty appears to be a simple consequence of the worst-case computational complexity gap: the NBA built from an LTL formula at Step (ii) is worst-case exponentially larger than the formula, and then determinizing it at Step (iii) requires a further exponential blowup, resulting in a 2EXPTIME-algorithm for reactive synthesis with LTL specifications (with a matching lower-bound). In comparison, model checking LTL specifications does not require the determinization step and is only PSPACE-complete. However there is more.

In AI, Reactive Synthesis has been studied with a focus on logics on finite traces (instead of infinite traces), e.g., LTLf [Gabbay et al., 1980; Baier and McIlraith, 2006; De Giacomo and Vardi, 2013; De Giacomo and Vardi, 2015]. In fact, LTLf synthesis [De Giacomo and Vardi, 2015] is one of the two main success stories of reactive synthesis so far (the other being the GR(1) fragment of LTL [Piterman et al., 2006]), and has brought about scalable results that are unprecedented [Zhu et al., 2017; Bansal et al., 2020; De Giacomo and Favorito, 2021; De Giacomo et al., 2022].

The reason behind such good results can not be explained by worst-case complexity arguments since the complexity of LTLf synthesis is exactly the same that of LTL, i.e., 2EXPTIME-complete. Furthermore, the basic steps of the LTLf synthesis algorithm are similar to Steps (i) to (iv) earlier outlined for LTL, with each step potentially introducing the same asymptotic blowup as the corresponding step for LTL. Indeed, for LTLf, Step (ii) produces a nondeterministic finite state automaton (NFA) which in the worst case is exponentially larger than the input formula, and Step (iii) determinizes that NFA to produce a DFA which in the worst case is exponentially larger than the NFA. It turns out that the difference between the practical performance of LTL and LTLf synthesis algorithms lies in the practical performance differences of Steps (ii) and (iii) of these algorithms: for LTLf, neither of these usually manifests its worst-case potential in practice! For LTL synthesis, Step (ii) is also shared by the modelchecking algorithm, which performs well in practice, thus indicating that Step (iii) is the main culprit. Indeed, the exponential blow-up of the determinization of NBA is serious also in practice [Althoff et al., 2006]. In comparison, for LTLf, Step (iii) not only does not usually introduce a blowup, but in fact it has been observed multiple times that determinizing an NFA results in a DFA that is smaller than the NFA [Tabakov and Vardi, 2005; Armoni et al., 2006; Rozier and Vardi, 2012; Tabakov et al., 2012].

Besides LTLf, another finite-trace logic that is gaining popularity in AI is Pure Past LTL (PPLTL) [Lichtenstein et al., 1985; De Giacomo et al., 2020; Bonassi et al., 2023b; Bonassi et al., 2023a; Bonassi et al., 2024; Cimatti et al., 2024]. This is a variant of LTLf that sees the trace backwards and has the notable property that one can obtain a symbolic (i.e., factorized) DFA directly from the formula in linear time. Moreover, while the size of the (non-symbolic) DFA corresponding to an LTLf formula can be double-exponential in the size of the formula itself, the size of the (non-symbolic) DFA corresponding to a PPLTL formula is at most a singleexponential in the size of the formula.

In this paper we show how to lift the DFA techniques at the base of the success story of LTLf and PPLTL to handle the expressive power of full LTL. To do so, we leverage the classic hierarchy of LTL properties - the safety-progress hierarchy [Manna and Pnueli, 1990]. 1 It consists of six classes of semantic properties, organized by inclusion. The bottom first level has the safety properties that intuitively express that nothing bad ever happens, and the guarantee (aka co-safety) properties that intuitively express that something good eventually happens. The second level has the obligation properties obtained by taking positive Boolean combinations of safety and guarantee properties. The third level has recurrence properties that intuitively express that something good occurs infinitely often, and persistence properties that intuitively say that nothing bad occurs infinitely often. The fourth level contains the reactivity properties which are positive Boolean combinations of recurrence and persistence properties. Each such property, which is interpreted over infinite traces, is defined in terms of sets of finite traces, which refer to finite prefixes of the infinite trace. For example, a set F of finite traces induces a basic safety (resp. progress) property that is satisfied by an infinite trace iff every prefix (resp. all but finitely many prefixes) of that trace are in F. The reactivity properties contain all properties expressible in LTL. 2

We revisit Manna and Pnueli's hierarchy, and extract from it extensions of LTLf and PPLTL, which we call LTLf+ and PPLTL+, that can express arbitrary LTL properties on infinite traces. These logics retain a crucial characteristic for reactive synthesis of their base logics: one can exploit the techniques for translating LTLf and PPLTL formulas into DFAs [De Giacomo and Vardi, 2015; De Giacomo et al., 2020]. By taking a simple product of these DFAs one can form the game arena for strategy extraction of LTLf+/PPLTL+ specifications. Naturally, the game objectives for LTLf+/PPLTL+ go beyond the simple adversarial reachability for LTLf/PPLTL. In particular, we exploit the Emerson-Lei condition [Emerson and Lei, 1987] for handling Boolean combinations, and the possibility of translating these conditions into parity conditions (typically used for LTL) or to fixpoint computations [Hausmann et al., 2024]. Beside studying Reactive Synthesis in LTLf+/PPLTL+, we also study satisfiability and model checking problems of these logics, and provide both upper bounds and corresponding lower bounds.

1 The hierarchy was introduced by Lichtenstein et al. in 1985, later described in detail by Manna and Pnueli in 1990; also, see the survey [Piterman and Pnueli, 2018].

2 The hierarchy is not limited to LTL, i.e., to properties that are expressible in first-order logic (FO) over infinite sequences [Kamp, 1968], but extends to omega-regular properties, i.e., to monadicsecond order logic (MSO) over infinite sequences. Indeed, all the results we present here can be extended to omega-regular properties by substituting LTLf (resp. PPLTL) by its MSO-complete variant LDLf (resp. PPLDL) [De Giacomo and Vardi, 2013].

We believe that the importance of this work is not in the presentation of new logics, new algorithmic techniques, or new hard to achieve lower-bounds. In fact, the logics LTLf+/PPLTL+ can be easily extracted from Manna and Pnueli's work, the algorithms we present, though new, employ variations of known building blocks, and the same goes for the lower bounds. The main contribution of this paper is in observing that if one combines the exact building blocks we use, in the exact way that we do, one can obtain for the first time, for natural LTLf-based and PPLTL-based logics that are as expressive as LTL, synthesis algorithms that are DFA based - and thus avoid the notoriously difficult stumbling block of determinizing automata over infinite words which has been the bane of putting LTL synthesis into practical use. In many ways, this paper has been "hiding in plain sight" and could have been written many decades ago, as all the necessary pieces were available for everyone to see for a very long time. The fact that it was never written, and that nobody noticed how to obtain the algorithms we present and tried to put them into practical use, is a strong indication to us that this information should be finally brought to the attention of the AI and reactive synthesis communities.

2 Preliminaries

Trace Properties. Let Σ be a finite alphabet. If S ⊆ Σ, then Sω (resp. S∗ ) is the set of infinite (resp. finite) sequences over S. The empty sequence is denoted ε. Indexing sequences starts at 0, and we write τ = τ0τ1 . . . . For 0 ≤ i < |τ|, write τ≤i for the prefix τ0 . . . τi, and τ≥i for the suffix τiτi+1 . . . of τ. Let AP be a finite non-empty set of atoms. A trace is a non-empty finite or infinite sequence τ over Σ = 2AP (valuations of atoms); in particular, the empty sequence ε is not a trace. The length of τ is denoted |τ | ∈ N ∪ {∞}. A finite-trace property is a set of finite traces. An infinite-trace property is a set of infinite traces. A trace satisfies a property Z if it is in Z. Let L be a logic for representing infinite-trace (resp. finite-trace) properties (we will later consider a few instantiations of L). The set of infinite (resp. finite) traces satisfying a formula φ of L is denoted [φ]. An infinite-trace (resp. finite-trace) property Z is definable (aka, expressible) in L iff there is some formula φ of L such that Z = [φ].

Transition Systems. A nondeterministic transition system T = (Σ,Q, I, δ) consists of a finite input alphabet Σ (typically, Σ = 2AP ), a finite set Q of states, a set I ⊆ Q of initial states, and a transition relation δ ⊆ Q×Σ×Q. The size of T is |Q|, the number of its states. We say that T is total if for every q, a there exists q′ such that (q, a, q′ ) ∈ δ. Unless stated otherwise, nondeterministic transition systems are assumed to be total. In case I = {ι} is a singleton and δ is functional, i.e., for every q, a there is a unique q′ such that (q, a, q′ ) ∈ δ, the transition system is called deterministic instead of nondeterministic; in this case we write ι instead of I, and δ(s, a) = s′ instead of (s, a, s′ ) ∈ δ. A run (aka path) induced by the trace τ is a sequence ρ = ρ0ρ1 . . . of states, where ρ0 ∈ I and ρi+1 ∈ δ(ρi, τi) for 0 ≤ i < |τ|. We simply say that τ has the run ρ and that ρ is a run of τ. In a nondeterministic transition system T, a trace may have any number of runs (including none). If a trace τ has a run in T, we say that T generates τ. For i ∈ {1, 2}, let Ti = (Σ,Qi, ιi, δi) be deterministic transition systems over the same alphabet. The product T1 × T2 is the deterministic transition system (Σ,Q′ , ι′ , δ′ ) where Q′ = Q1 × Q2, ι′ = (ι1, ι2), and δ((q1, q2), a) = (δ1(q1, a), δ2(q2, a)). This naturally extends to a product of n-many systems. For an infinite run ρ, define inf(ρ) ⊆ Q to be the set of states q ∈ Q such that q = ρi for infinitely many i.

Automata on finite traces. A finite automaton is a pair A = (T, F ), where T is a transition system and F ⊆ Q is the set of final states. The size of A is the size T . If T is nondeterministic, then A is called a nondeterministic finite automaton (NFA); if T is deterministic, then A is called a deterministic finite automaton (DFA). A finite trace is accepted by A if it has a run that ends in a state of F. The set of finite traces accepted by A is called the language of A, and is denoted L(A). Two automata A, B are equivalent if L(A) = L(B).

Games and synthesis. An arena is a deterministic transition system D = (Σ,Q, ι, δ) where Σ = 2AP and AP is partitioned into X ∪ Y for some sets X, Y of atoms (we use T to denote general transition systems, and D to denote arenas). Elements of 2Y (resp. 2X ) are called environment moves (resp. agent moves). An objective O over D is a subset of Qω . Elements of O are said to satisfy O. A game is a pair G = (D,O). A strategy is a function σ : (2Y )∗ → (2X ) that maps sequences of environment moves to agent moves (including the empty sequence, because the agent moves first). An outcome of σ is an infinite trace τ over 2AP such that (i) τ0∩X = σ(ε), and (ii) for i > 0 we have τi ∩X = σ(τ0 ∩Y · τ1 ∩Y · · · τi-1 ∩Y ). A strategy σ is winning if for every outcome τ , the run ρ ∈ Qω induced by the trace τ in D satisfies O. The following computational problem is called game solving: given G = (D, O), decide if there is a winning strategy, and if so, to return a finite representation of one. Intuitively, in a game, the agent moves first, the environment responds, and this repeats producing an infinite trace τ . The agent is trying to ensure that the run induced by τ satisfies the objective, while the environment is trying to ensure it does not.

Emerson-Lei (EL) automata and games. An EL condition [Emerson and Lei, 1987] over a set Q of states is a triplet (Γ, λ, B), where Γ is a finite set of labels, λ: Q → 2Γ is a labeling function that assigns to a state a (possibly empty) subset of labels, and B : 2Γ → {true, false} is a Boolean function over the set Γ (treated as variables). 3 For a state q ∈ Q and a label l ∈ λ(q), we say that q visits l. We will sometimes (but not always) write B as a Boolean formula over the set Γ of variables, with the usual syntax and semantics, e.g., the formula l1 ∧ l2 ∧ ¬l3 denotes the Boolean function that assigns true to a set Z ⊆ Γ iff Z contains l1 and l2 but not l3. For a sequence ρ ∈ Qω , we denote by infλ (ρ) = ⋃{λ(q) : q ∈ inf(ρ)}, i.e., the set of labels that are visited infinitely many times by states on ρ. The EL condition (Γ, λ, B) induces the objective O = {ρ ∈ Qω : B(infλ (ρ)) = true}, i.e., ρ ∈ O if the set of labels that are visited infinitely often satisfies B; in this case we say that ρ satisfies the EL condition. An EL automaton is a pair A = (T, (Γ, λ, B)), where T is a transition system, and (Γ, λ,B) is an EL condition over the states of T . If T is deterministic then A is called a deterministic EL automaton (DELA). An EL game is a DELA (D, (Γ, λ,B)) where D is an arena. DELA are closed under Boolean operations, with very simple constructions, and trivial proofs:

Proposition 1. Given a DELA A = (T, (Γ, λ, B)), the DELA B = (T, (Γ, λ, ¬B)) accepts the complement of L(A). Given DELA A = (T1, (Γ1, λ1, B1)) and B = (T2, (Γ2, λ2, B2)), with Γ1 and Γ2 being disjoint, let T be the product of T1 and T2. We have that the DELA C = (T, (Γ1 ∪ Γ2, λ, B)), where λ(p, q) = λ1(p) ∪ λ2(q), accepts the language L(A) ∪ L(B) if we take B = B1 ∨ B2, and the language L(A) ∩ L(B) if we take B = B1 ∧ B2.

Theorem 1. [Hausmann et al., 2024] EL games can be solved in time polynomial in the size of the arena and exponential in the number of labels.

3 Linear Temporal Logics on Finite Traces

Let AP be a finite non-empty set of atoms.

LTLf. LTLf formulas are given by the syntax:

Here p ∈ AP, X ("next") and U ("until") are the future operators. Common abbreviations include WXφ = ¬X¬φ ("weak next"). We interpret LTLf formulas over (non-empty) finite traces. Intuitively, we evaluate starting in position 0 of the trace, Xφ says that φ holds in the next step, and φ1 Uφ2 says that φ2 holds eventually, and φ1 holds at every point in time until then. In LTLf, one can predicate about both ends of the finite trace: the first instant of the trace by avoiding temporal operators (as in LTL), and the last instant by using the abbreviation last := ¬Xtrue. There is an algorithm that converts a given LTLf formula φ into an equivalent NFA of size exponential in the size of φ, and also into an equivalent DFA of size double-exponential in φ [De Giacomo and Vardi, 2013; De Giacomo and Vardi, 2015].

3 This definition is implicit in [Emerson and Lei, 1987]. However, later references to the EL-condition in the literature, e.g., [Hunter and Dawar, 2005], often give a special case where the Boolean formula is over states (not labels). This special case would not allow us to achieve optimal complexities.

PPLTL. PPLTL formulas are given by the syntax:

Here p ∈ AP , Y ("yesterday") and S ("since") are the past operators, analogues of "next" and "until", respectively, but in the past. Common abbreviations include Oφ = trueSφ ("(at least) once in the past"), Hφ = ¬O¬φ ("historically" or "hitherto"), first = ¬Y true. We interpret PPLTL formulas over (non-empty) finite traces starting at the last position of the trace. One can also predicate about both ends of the finite trace: the last instant of the trace by avoiding temporal operators, and the first instant by using the abbreviation first := ¬Y true. We say that an automaton A is equivalent to an LTLf/PPLTL formula φ if L(A) = [φ]. There is an algorithm that converts a given PPLTL formula φ into an equivalent DFA of size exponential in φ [De Giacomo et al., 2020].

Remark 1. LTLf and PPLTL define the same set of finite trace properties, namely, the properties definable by FOL over finite traces, or equivalently by the star-free regular expressions [Gabbay et al., 1980; Lichtenstein et al., 1985]. However, translating LTLf into PPLTL, and vice-versa, is at least exponential in the worst case, see [Artale et al., 2023] and the discussions in [De Giacomo et al., 2020; Bonassi et al., 2023b; Geatti et al., 2024].

LTL, and LTL with past Linear Temporal Logic (LTL) [Pnueli, 1977] is perhaps the most used logic for specifying temporal properties. LTL formulas have the same syntax as LTLf, but are interpreted over infinite traces, which allows LTL to capture liveness properties which cannot be fully done using finite trace semantics. LTL with past, i.e., enhanced with the past operators "yesterday" and "since", is expressively equivalent to LTL [Zuck, 1987].

4 LTLf+ and PPLTL+

Based on LTLf (resp. PPLTL), we define the logic LTLf+ (resp. PPLTL+) for specifying infinite-trace properties. We do so by quantifying over prefixes of infinite traces relativized to LTLf/PPLTL finite-trace properties. Formally, for a finitetrace property Z, we define four fundamental infinite-trace properties as follows: ∀Z (resp. ∃Z) denotes the set of infinite traces τ such that every (resp. some) non-empty finite prefix of τ satisfies Z; ∀∃Z (resp. ∃∀Z) denotes the set of infinite traces τ such that infinitely many (resp. all but finitely many, aka almost all) finite prefixes of τ satisfies Z. Notice that these properties cover the entire safety-progress hierarchy. Based on these we now define our logics.

Syntax. Fix a set AP of atoms. The syntax of LTLf+ (resp. PPLTL+) is given by the following grammar:

where Φ are formulas in LTLf (resp. PPLTL) over AP. We use common abbreviations, e.g., Ψ ⊃ Ψ′ for ¬Ψ ∨ Ψ′ . The formulas ∀Φ, ∃Φ, ∀∃Φ, ∃∀Φ are called infinite-trace formulas, and the formulas Φ are called finite-trace formulas.

Semantics. For an LTLf/PPLTL formula Φ, recall that we write [Φ] ⊆ (2AP )+ for the set of (non-empty) finite traces that satisfy Φ. For an LTLf+/PPLTL+ formula Ψ let [Ψ] ⊆ (2AP )ω denote the set of infinite-trace properties, defined recursively as follows:

• [Ψ ∨ Ψ′ ] = [Ψ] ∪ [Ψ′ ], [Ψ ∧ Ψ′ ] = [Ψ] ∩ [Ψ′ ], and [¬Ψ] = (2AP )ω \ [Ψ];
• [∀Φ] = ∀[Φ], [∃Φ] = ∃[Φ], [∀∃Φ] = ∀∃[Φ], and [∃∀Φ] = ∃∀[Φ].

In words, the Boolean operations are handled as usual, and [∀Φ] (resp. [∃Φ]) denotes the set of infinite traces τ such that every (resp. some) non-empty finite prefix of τ satisfies Φ, and [∀∃Φ] (resp. [∃∀Φ]) denotes the set of infinite traces τ such that infinitely many (resp. all but finitely many) finite prefixes of τ are in Φ. Note that ∀Φ and ∃Φ are dual since ∀Φ ≡ ¬∃¬Φ, as are ∀∃Φ and ∃∀Φ since ∀∃Φ ≡ ¬∃∀¬Φ. We write τ |= Ψ to mean that τ ∈ [Ψ].

In the terminology of the safety-progress hierarchy [Manna and Pnueli, 1990]: [∀Φ] is a safety property; [∃Φ] is a guarantee property; [∃∀Φ] is a persistence property; [∀∃Φ] is a recurrence property; and [Ψ] is a reactivity property.

Examples. We illustrate LTLf+ and PPLTL+with some examples. To specify properties of the initial instant we use propositional formulas ϕ as abbreviations for ∀ϕ in LTLf+, and for ∀(H(first ⊃ ϕ)) in PPLTL+.

Preconditions and effect specifications in planning domains [Geffner and Bonet, 2013], non-Markovian domains [Gabaldon, 2011] are essentially safety properties, which can all be expressed with formulas of the form ∀Φ, see also [Aminof et al., 2025]. For example - below ϕx are propositional formulas - conditional effect axioms can be expressed in LTLf+ and PPLTL+ by ∀G(ϕc ⊃ (Xa ⊃ Xϕe)) and ∀H(Yϕc ⊃ (a ⊃ ϕe)). Frame axioms can be expressed as ∀ G(ϕc ∧ X a ⊃ (p ≡ X p)) and ∀ H(Y ϕc ∧ a ⊃ (Y p ≡ p)). Initial conditions ϕinit can be expressed as mentioned above. Fairness of effects, e.g., assuming that action a under condition ϕc can effect two effects ϕe1 or ϕe2 , can be expressed as ∀∃ F(ϕc ∧ X(a ∧ last)) ⊃ ∧i ∀∃ F(ϕc ∧ X(a ∧ last ∧ ϕei )) and ∀∃((Yϕc) ∧ a) ⊃ ∧i ∀∃((Yϕc) ∧ a ∧ ϕei ), see e.g., [D'Ippolito et al., 2018]. Arbitrary LTLf temporally extended goals Φ [De Giacomo and Vardi, 2013] can be expressed using formulas of the form ∃Φ, e.g., eventually reaching a state where ϕg holds while guaranteeing to maintain a safety condition ϕs can be expressed as ∃(Fϕg ∧ Gϕs) and ∃(ϕg ∧ Hϕs). Some LTL formulas, though not all [Esparza et al., 2024], are also easy to express, for example G(ϕ1 ⊃ Fϕ2) can be expressed as ∀∃(G(ϕ1 ⊃ Fϕ2)) in LTLf+ and ∀∃(¬ϕ1 Sϕ2 ∨ H¬ϕ1) in PPLTL+. Note that although in these examples the sizes of the LTLf formulas and corresponding PPLTL are polynomially (linearly, in fact) related, this is not always the case, see Remark 1.

Expressive Power. The logics PPLTL+, LTLf+, and LTL have the same expressive power.

Theorem 2. The logics LTLf+, PPLTL+, and LTL define the same infinite-trace properties.

Proof. For Q ∈ {∀, ∃, ∀∃, ∃∀}, write QPPLTL for the fragment of PPLTL+ consisting of formulas of the form QΦ

for Φ in PPLTL. Recall from [Manna and Pnueli, 1990] that: a reactivity formula is defined as a Boolean combination of formulas from ∀∃PPLTL, and that every formula in ∀PPLTL, ∃PPLTL, ∃∀PPLTL is equivalent to a reactivity formula. 4 Thus, PPLTL+ defines the same properties as the reactivity formulas. Also, recall from [Manna and Pnueli, 1990] that the reactivity formulas define the same infinitetrace properties as LTL. Finally, use the fact that PPLTL and LTLf define the same finite-trace properties [De Giacomo et al., 2020].

PNF. The LTLf+ (resp. PPLTL+) formulas in positive normal-form (PNF) are given by the following grammar: Ψ ::= ∀Φ | ∃Φ | ∀∃Φ | ∃∀Φ | Ψ ∨ Ψ | Ψ ∧ Ψ where Φ are formulas in LTLf (resp. PPLTL) over AP. We can convert, in linear time, a given LTLf+ (resp. PPLTL+) formula into one that is in positive normal-form, in the usual way, by pushing negations into the finite-trace formulas Φ.

Remark 2. We observe that PPLTL+ can be viewed as a syntactical variant of the normal form of LTL, enhanced with past operators, as originally introduced by Manna and Pnueli in defining the safety-progress hierarchy in [Manna and Pnueli, 1990]. Specifically, it suffices to use G instead of ∀ and F instead of ∃, without altering the meaning of the PPLTL+ formulas. Consequently, our results for PPLTL+ apply directly to Manna and Pnueli's normal form as well.

5 Reactive Synthesis

In this section we study reactive synthesis [Pnueli and Rosner, 1989] for PPLTL+ and LTLf+ specifications.

Definition 1. The LTLf+ synthesis problem (resp. PPLTL+ synthesis problem) asks, given Ψ in LTLf+ (resp. PPLTL+), to decide if there is a strategy σ such that every outcome of σ satisfies Ψ (such a strategy is said to enforce Ψ), and, if so, to return a finite representation of such a strategy.

We solve the LTLf+/PPLTL+ synthesis problem with an automata-theoretic approach based on DFAs, in a 4-step Synthesis Algorithm, as follows. For convenience, we begin with a formula Ψ in positive normal-form. The formula Ψ can be thought of as a Boolean formula ̂Ψ without negations over a set of the form [k] = {1, 2, . . . , k} (for some k); thus Ψ can be formed from ̂Ψ by replacing, for every i ∈ [k], every occurrence of i in ̂Ψ by a certain infinite-trace formula of the form QiΦi, where Qi ∈ {∃, ∀, ∃∀, ∀∃}. Elements of [k] are called component numbers.

Step (1). For each i ∈ [k], convert the finite-trace formula Φi into an equivalent DFA Ai = (Di, Fi). Say Di = (Σ, Qi, ιi, δi). We assume, without loss of generality, that the initial state has no incoming transitions. Note that one only has to do this conversion once for each finite-trace formula, even if it appears in multiple infinite-trace formulas.

Step (2). For each i ∈ [k], build a transition systemD′i = (Σ,Qi, ιi, δ′i ), a set F ′ i ⊆ Qi, and an objective Oi over Qi:

4 This equivalence may involve a blowup, but this is not relevant to understand expressive power.

1. Say Qi = ∃∀. Let δ′i = δi, F ′ i = Fi, and Oi = {ρ : inf(ρ) ∩ (Q \ F ′ i ) = ∅}.
2. Say Qi = ∀. If ιi is not a final state, make it into a final state, i.e., define F ′ i = Fi ∪ {ιi}. Let δ′i be like δi except that every non-final state is a sink, i.e., define δ′i (q, a) to be q if q ̸∈ F ′ i , and otherwise to be δi(q, a). Let Oi = {ρ : inf(ρ) ∩ F ′ i ̸= ∅}.
3. Say Qi = ∃. If ιi is a final state, make it into a nonfinal state, i.e., define F ′ i = Fi \ {ιi}. Let δ′i be like δi except that every final state q is a sink, i.e., define δ′i (q, a) to be q if q ∈ F ′ i , and otherwise to be δi(q, a). Let Oi = {ρ : inf(ρ) ∩ F ′ i ̸= ∅}. 5

The next Theorem connects the formula QiΦi to the runs in the transition system D′i that satisfy the objective Oi, and follows by the construction in Step (1) and Step (2).

Theorem 3. An infinite trace satisfies QiΦi iff the run it induces in D′i satisfies the objective Oi.

Proof. Let τ be an infinite trace and let ρ (resp. ρ′ ) be the run in Di (resp. D′i ) induced by τ. Recall that the empty string is not a trace, and so a non-empty prefix of τ corresponds to a prefix of its run of length > 1.

We look at each case separately.

1. τ satisfies ∀∃Φi iff (by Definition of ∀∃) infinitely many prefixes of τ satisfy Φi iff infinitely many prefixes of ρ end in Fi iff inf(ρ) ∩ Fi ̸= ∅ iff (since ρ′ = ρ and F ′ i = Fi) ρ′ satisfies Oi.
2. τ satisfies ∃∀Φi iff (by Definition of ∃∀) almost all prefixes of τ satisfy Φi iff almost all prefixes of ρ end in Fi iff it is not the case that infinitely many prefixes of ρ end in Qi \ Fi iff inf(ρ) ∩ (Q \ Fi) = ∅ iff (since ρ′ = ρ and F ′ i = Fi) ρ′ satisfies Oi.
3. τ satisfies ∀Φi iff (by Definition of ∀) all non-empty prefixes of τ satisfy Φi iff ρn ∈ Fi for all n > 0 iff (since the transitions from the initial state and final states in Di are unchanged in D′i ) ρ′n ∈ F ′ i for all n > 0 iff ρ′n ∈ F ′ i for infinitely many n (since all non-final states are sinks) iff inf(ρ′ ) ∩F ′ i ̸= ∅ iff ρ′ satisfies Oi.
4. τ satisfies ∃Φi iff (by Definition of ∃) some non-empty prefix of τ satisfies Φi iff ρn ∈ Fi for some n > 0 iff (since the transitions from the initial state and nonfinal states in Di are unchanged in D′i , and taking the least such n) ρ′n ∈ F ′ i for some n > 0 iff ρ′n ∈ F ′ i for infinitely many n (since all final states are sinks) iff inf(ρ′ ) ∩ F ′ i ̸= ∅ iff ρ′ satisfies Oi.

This completes the proof.

Call a state qi ∈ Qi marked if either (a) Qi ̸= ∃∀ and qi ∈ F ′ i , or (b) Qi = ∃∀ and qi ∈ Qi \ F ′ i . Thus, by the construction in Step (2), in case Qi ̸= ∃∀, the objective Oi says that some marked state is seen infinitely often, and in case Qi = ∃∀ the objective Oi says that no marked state is seen infinitely often.

5 We make two remarks about the cases Q ∈ {∀, ∃}: by our assumption that the initial state has no incoming transitions, redefining whether the initial state is a final state or not does not change the set of non-empty strings accepted by the DFA Ai; we could have defined either or both these cases to have an objective like the ∃∀ case (instead of the ∀∃ case) since seeing a sink is the same as seeing it infinitely often which is the same as seeing it from some point on.

Step (3). Build the product transition system D = ∏i∈[k] D′i . Let Q be the state set of D. Define an EL condition (Γ, λ,B) over Q as follows: Γ = [k] (i.e., the labels are the component numbers), λ(q) = {i ∈ [k] : qi is marked} (i.e., a state is labeled by the numbers of those components that are in marked states), and the Boolean formula B is formed from the Boolean formula ̂Ψ by simultaneously replacing, for every i with Qi = ∃∀, every occurrence of i by ¬i. Define the deterministic EL-automaton AΨ = (D, (Γ, λ, B)).

Example 1. Say Ψ = ∀∃Φ1 ∨ ∃∀Φ2. Then the label set is Γ = {1, 2}. Let τ be an infinite trace, let ρ (resp. ρi ) be the induced run in D (resp. D′i ). By Theorem 3, τ |= Ψ iff ρ1 satisfies O1 or ρ2 satisfies O2. By definition of Oi, this is iff ρ1 sees a marked state of D′1 infinitely often or ρ2 does not see a marked state of D′2 infinitely often. And this is iff the set of labels i ∈ {1, 2} for which ρi sees a marked state infinitely often, satisfies the Boolean formula B := 1 ∨ ¬2.

Theorem 4. Ψ is equivalent to the EL-automaton AΨ.

Proof. In Step (2), for i ∈ [k], the objective Oi is induced by the following EL-condition (Γi, λi,Bi) over Qi. Let Γ = {i}, i.e., the only label is i. For qi ∈ Qi, let λi(qi) = {i} if qi is marked, and λi(qi) = {} otherwise. Then, for a run ρ in D′i , we have that infλi (ρ) = {i} iff some state seen infinitely often in ρ is marked (and otherwise infλi (ρ) = {}). We consider the two cases:

1. Say Qi ̸= ∃∀. Recall that qi is marked iff qi ∈ F ′ i . Thus, ρ ∈ Oi iff inf(ρ) ∩ F ′ i ̸= ∅ iff infλi (ρ) = {i} iff ρ satisfies the EL-condition (Γi, λi,Bi) where Bi is the Boolean formula i.
2. Say Qi = ∃∀. Recall that qi is marked iff qi ∈ Qi \ F ′ i . Thus, ρ ∈ Oi iff inf(ρ)∩(Qi \F ′ i ) = ∅ iff infλi (ρ) = {} iff ρ satisfies the EL-condition (Γi, λi,Bi) where Bi is the Boolean formula ¬i.

By Theorem 3, Ψ is equivalent to the Boolean combination formed from ̂Ψ by replacing each occurrence of index i by the EL-automaton Ai := (D′i , (Γi, λi,Bi)). Applying Proposition 1 to this Boolean combination results in an EL-automaton whose transition system is the product D, and whose EL-condition is (Γ, λ,B) where Γ = [k], λ((q1, · · · , qn)) = ⋃i λi(qi), and B is formed from ̂Ψ by simultaneously replacing, for every i with Qi = ∃∀, every occurrence of i by ¬i. Now notice that this is exactly the definition of AΨ in Step (3) of the Synthesis Algorithm.

Step (4). Solve the EL game AΨ. By Theorem 1, this can be done in time polynomial in the size of the arena and exponential in the number of labels. This completes the description of the algorithm.

Since, for an LTLf+ (resp. PPLTL+) formula Ψ, the size of the arena D is double-exponential (resp. single-exponential)

in the size of Ψ, and the number of labels k is linear in the size of Ψ, we get:

Theorem 5. The LTLf+ (resp. PPLTL+) synthesis problem is in 2EXPTIME (resp. EXPTIME).

We observe that our algorithms are (worst-case) optimal:

Theorem 6. The LTLf+ (resp.PPLTL+) synthesis problem is 2EXPTIME-complete (resp. EXPTIME-complete).

Proof. For the lower bounds, synthesis is 2EXPTIME-hard already for the fragment of LTLf+ consisting of formulas of the form ∃Φ [De Giacomo and Vardi, 2015], and synthesis is EXPTIME-hard already for the fragment of PPLTL+ for formulas of the form ∃Φ [De Giacomo et al., 2020].

Remark 3. PPLTL+ synthesis is in EXPTIME (Theorem 5), which is exponentially cheaper than LTL synthesis, which is 2EXPTIME-hard [Pnueli and Rosner, 1990]. This means that LTL is, in the worst case, exponentially more succinct than PPLTL+. One may be tempted to think that the fact that PPLTL+ synthesis is cheaper than LTL synthesis is because LTL is always more succinct than PPLTL+. However, it turns out this is not true. Indeed, PPLTL+ is, in the worst case, exponentially more succinct than LTL [Markey, 2003, Section 3]. This leads to the interesting phenomenon of two logics with the same expressive power, incomparable succinctness, yet solving a logic problem for one of them is exponentially cheaper. This phenomenon holds for the finite-trace logics LTLf/PPLTL [Artale et al., 2023], and so the fact that PPLTL+ synthesis is in EXPTIME shows that this phenomenon can be lifted to all LTL-definable infinitetrace properties.

Finally, we remark that Step (4) requires solving an EL game built from the product of the DFAs with a simple Boolean formula (that mimics the given formula Ψ). This can be implemented based on fixpoint computations [Hausmann et al., 2024], which has the potential for efficient symbolic implementations. Alternatively, one may convert the EL game to a parity game, and solve the parity game using existing algorithms and solvers [van Dijk, 2018]. The literature provides hints on how to perform this transformation [Hunter and Dawar, 2005; Casares et al., 2022]. However, one has to be careful not to blow up the state space in a way that would degrade the overall complexity stated in Theorem 5.

6 Satisfiability andModel Checking

We now study other standard reasoning tasks for our logics, i.e., satisfiability and model checking. Let L be one of LTLf/PPLTL. The L+ satisfiability problem asks, given Ψ in L+, to decide whether [Ψ] ̸= ∅. For a nondeterministic transition system T, that is not assumed to be total, with input alphabet Σ = 2AP , we say that T satisfies Ψ if every infinite trace generated by T satisfies Ψ. 6 The L+ model checking problem asks, given Ψ in L+, and a nondeterministic labeled transition system T , whether T satisfies Ψ.

6 There are many ways to define transitions systems for verification. Commonly, these are state-labeled directed graphs. For technical convenience, instead of labeling the state with l, we will instead label all outgoing edges with l, and thus we can view these as (not necessarily total) nondeterministic transition systems.

Theorem 7. The LTLf+ (resp. PPLTL+) satisfiability and model checking problems are EXPSPACE-complete (resp. PSPACE-complete).

Satisfiability Upper Bound. Given Ψ, build the equivalent EL-automaton AΨ = (D, (Γ, λ,B)) of Step (3) above. Recall that |Γ| = k, which is linear in |Ψ|. Satisfiability can be solved by checking if there is an infinite run in D that satisfies the EL-condition. This can be done in time polynomial in the size of D and k, as follows. Check if there is a state s of D such that (i) there is a path from the initial state to s, and (ii) there is a path (that uses at least one transition) from s to s such that the set of labels visited on this path is a satisfying assignment of B. However, since the size of D is doublyexponential (resp. exponential) in the size |Ψ| of the given formula, this algorithm would run in 2EXPTIME for LTLf+ (resp. EXPTIME for PPLTL+). These complexities can be lowered to EXPSPACE (resp. PSPACE) by exploiting the fact that reachability in directed-graphs is in NLOGSPACE [Papadimitriou, 2007], and, as usual, doing things "on-the-fly".

Model Checking Upper Bound. Given a nondeterministic transition system T and an LTLf+/PPLTL+ formula Ψ, we have that T satisfies Ψ iff it is not the case that there is an infinite trace generated by T that satisfies ¬Ψ. Thus, since deterministic complexity classes are closed under complement, it is enough to provide an optimal algorithm for the following problem: given a nondeterministic transition system T and a LTLf+/PPLTL+ formula Ψ, decide if there is an infinite trace generated by T that satisfies Ψ. To do this we proceed as in the "on-the-fly" algorithm for satisfiability. However, we add to the current state of D a component consisting of the current state of T .

Lower Bounds. The lower bounds already hold for formulas of the form ∀Φ and ∃Φ. This can proven by relying on results and techniques from [De Giacomo and Vardi, 2013; Vardi and Stockmeyer, 1985; Kupferman and Vardi, 2000; Bansal et al., 2023].

Remark 4. The EXPSPACE-completeness result for satisfiability and model checking in LTLf+ may appear surprising since satisfiability and model checking for LTL are both PSPACE-complete [Clarke et al., 2018], but in fact confirms and extends a recent EXPSPACE-hardness result for model checking the fragment of LTLf+ limited to the guarantee class [Bansal et al., 2023]. We remark that despite this theoretical worst-case complexity, we expect model checking and satisfiability of LTLf+ to be much more tractable in practice, the same way and for the same reason that the 2EXPTIMEhardness for LTLf synthesis does not manifest in practice (as discussed in the Introduction). Finally, observe that our results show that the complexity of satisfiability and model checking of PPLTL+ is the same as for LTL.

7 RelatedWork

The guarantee and safety fragment of LTLf+/PPLTL+, i.e., formulas of the form ∃Φ and ∀Φ for Φ in LTLf/PPLTL, has been studied in the literature (under other names), i.e., as LTLf synthesis [De Giacomo and Vardi, 2015], LTLf synthesis under environment specifications [Aminof et al., 2025], and LTLf model-checking (non-terminating semantics) [Bansal et al., 2023]. Synthesis for the Safety fragment has been studied in [Cimatti et al., 2024]

Reactive synthesis is deeply related to Planning [De Giacomo and Rubin, 2018; Camacho et al., 2019; De Giacomo et al., 2023], and in particular to (strong) planning for temporally extended goals in fully observable nondeterministic domains [Cimatti et al., 2003; Bacchus and Kabanza, 1998; Calvanese et al., 2002; Baier and McIlraith, 2006; Baier et al., 2007; Gerevini et al., 2009]. Following, e.g., [De Giacomo and Rubin, 2018] it is easy to design optimal algorithms for handling LTLf+/PPLTL+ goals, and would be interesting to extend this to best-effort planning and synthesis [De Giacomo et al., 2023; Aminof et al., 2021b; Aminof et al., 2021a; Aminof et al., 2023a], and also to stochastic best-effort [Aminof et al., 2022; Aminof et al., 2023b].

The safety-progress hierarchy has mainly been used to understand the expressivity of fragments of LTL. However, recent results that convert arbitrary LTL formulas into a normal form consisting of a combination of classes in the hierarchy in single exponential time [Esparza et al., 2020; Esparza et al., 2024] are providing new interest in the hierarchy. Our work shares this interest, though sidesteps the LTL normalization, and focuses instead on specifying directly using finite traces, and then lifting to infinite traces through quantification on prefixes.

8 Conclusion

We studied two logics LTLf+/PPLTL+ that have the same expressive power as LTL, and showed how to apply DFA techniques to build arenas for synthesis, typical for handling the base finite-trace logics, thus side-stepping the difficulty of determinizing automata on infinite traces, typical of LTL synthesis. Our approach only relies on the base logic being closed under negation and having conversions into DFAs. Thus, it would also work for any other base logic with these properties, e.g., linear dynamic logic on finite traces [De Giacomo and Vardi, 2015] or pure past linear dynamic logic [De Giacomo et al., 2020]. We thus advocate revisiting Manna and Pnueli's safety-progress hierarchy, focusing on (i) using it directly for representation, by putting emphasis on the finite-trace components of infinite properties, and (ii) solving computational problems by exploiting DFA-based arena constructions.

A key characteristic of Planning is that the system continuously receives a goal, "thinks" about how to achieve it, synthesizes a plan, executes the plan, and repeats [Geffner and Bonet, 2013]. However, if we consider goals on infinite traces, e.g., expressed in LTLf+/PPLTL+, this loop needs to be revised, by considering that the agent will receive its new goal while executing for the previous ones, as in live synthesis [Finkbeiner et al., 2022; Zhu and De Giacomo, 2022]. This observation puts goal reasoning [Aha, 2018] at the center of the stage when dealing with infinite trace goals, and is an avenue of future research.

Acknowledgments

This work is supported in part by the ERC Advanced Grant WhiteMech (No. 834228), the PRIN project RIPER (No. 20203FFYLK), the PNRR MUR project FAIR (No.PE0000013), the UKRI Erlangen AI Hub on Mathematical and Computational Foundations of AI, NSF grants IIS1527668, CCF-1704883, IIS-1830549, CNS-2016656, DoD MURI grant N00014-20-1-2787, and an award from the Maryland Procurement Office.