arXiv CSopen access

Symbolic Synthesis for LTLf+ Obligations

Symbolic Synthesis for LTLf + Obligations

arXiv:2604.18532v1 [cs.LO] 20 Apr 2026

Giuseppe De Giacomo1 , Christian Hagemeier1 , Daniel Hausmann2 , Nir Piterman3 1 University of Oxford, UK 2 University of Liverpool, UK 3 University of Gothenburg and Chalmers University of Technology, Sweden [email protected], {christian.hagemeier,giuseppe.degiacomo}@cs.ox.ac.uk, [email protected] Abstract We study synthesis for obligation properties expressed in LTLf +, the extension of LTLf to infinite traces. Obligation properties are positive Boolean combinations of safety and guarantee (co-safety) properties and form the second level of the temporal hierarchy of Manna and Pnueli. Although obligation properties are expressed over infinite traces, they retain most of the simplicity of LTLf . In particular, we show that they admit a translation into symbolically represented deterministic weak automata (DWA) obtained directly from the symbolic deterministic finite automata (DFA) for the underlying LTLf properties on trace prefixes. DWA inherit many of the attractive algorithmic features of DFA, including Boolean closure and polynomial-time minimization. Moreover, we show that synthesis for LTLf + obligation properties is theoretically highly efficient – solvable in linear time once the DWA is constructed. We investigate several symbolic algorithms for solving DWA games that arise in the synthesis of obligation properties and evaluate their effectiveness experimentally. Overall, the results indicate that synthesis for LTLf + obligation properties can be performed with virtually the same effectiveness as LTLf synthesis.

1

Introduction

Linear Temporal Logic (LTL) (Pnueli 1977) and its finitetrace variants are commonly used in computer science and artificial intelligence, e.g., in planning for temporally extended goals and declarative control knowledge (Bacchus and Kabanza 1998; De Giacomo and Vardi 1999; Bacchus and Kabanza 2000; Calvanese, De Giacomo, and Vardi 2002; Baier and McIlraith 2006; Baier, Fritz, and McIlraith 2007; Gerevini et al. 2009). Reactive synthesis concerns the automatic construction of programs (typically called strategies) from temporal specifications for systems (e.g. agents, processes, protocols, controllers, or robots) that interact with their environments during execution (Pnueli and Rosner 1989; Finkbeiner 2016; Ehlers et al. 2017). It is closely related to strong planning for temporally extended goals in fully observable nondeterministic domains (Cimatti et al. 2003; Bacchus and Kabanza 1998; Bacchus and Kabanza 2000; Calvanese, De Giacomo, and Vardi 2002; Baier, Fritz, and McIlraith 2007; Gerevini et al. 2009; De Giacomo and Rubin 2018; Camacho, Bienvenu, and McIlraith 2019). Significant advances in reactive synthesis have been achieved using the GR(1)

fragment of LTL (Piterman, Pnueli, and Sa’ar 2006), and by restricting attention to finite traces using LTLf (De Giacomo and Vardi 2015). These successes were largely based on the use of symbolic techniques for handling temporal formulas, which substantially enhances scalability and computational capacity. Recently, the symbolic techniques underlying LTLf have been extended to infinite traces through the logic LTLf + (Aminof et al. 2025b). The key promise of LTLf + is that finite automata (as used in LTLf ) and the symbolic representations that efficiently support them can also be leveraged in the setting of infinite traces. LTLf + builds on the socalled Manna-Pnueli (or safety-progress) hierarchy of temporal formulas. This hierarchy was originally introduced in (Lichtenstein, Pnueli, and Zuck 1985) and subsequently developed in detail by Manna and Pnueli in (Manna and Pnueli 1990) and (Manna and Pnueli 1992; Manna and Pnueli 1995; Manna and Pnueli 2010); see also the survey (Piterman and Pnueli 2018). In this paper, we concentrate on the lowest levels of the hierarchy, namely safety and guarantee (also known as co-safety) properties, as well as their Boolean closure, referred to as obligation properties, which are our main focus. Obligation properties are very common in practice. Specifications used in model checking or synthesis frequently belong to the lower levels of the temporal hierarchy, namely safety, guarantee, and obligation. For instance, among the 55 specification patterns of Dwyer et al. (Dwyer, Avrunin, and Corbett 1998), 25 are obligation properties. Similarly, Somenzi & Bloem’s compilation of 25 LTL formulas “found in the literature” (Somenzi and Bloem 2000) contains 13 obligation properties. Moreover, even in the LTLf setting, assumptions about the environments are often forms of obligations (Aminof et al. 2025a). For obligation properties, we can work with deterministic weak automata (DWA) (Löding 2001). These automata have a substantially simpler structure than those required for arbitrary temporal formulas, particularly formulas from the higher levels of the Manna-Pnueli hierarchy. Their structural simplicity makes DWA very easy to use: they are closed under Boolean operations using constructions analogous to those of deterministic finite automata (DFA), and after a linear-time preprocessing stage (Löding 2001), they can be minimized using the same algorithm as

DFA. In this setting, the contributions of the present paper are as follows: 1. A technique for constructing symbolically represented DWA from LTLf + obligation properties. 2. A reduction of synthesis for the obligation fragment of LTLf + to the solution of weak games played on DWA. 3. A novel symbolic algorithm for the solving weak games by alternating safety and reachability computations. Together with three existing solution algorithms (the standard algorithms for Büchi and co-Büchi games, and a linear-time algorithm based on SCC decomposition), we obtain four fully symbolic 2E XP T IME synthesis algorithms for LTLf + obligation formulas. 4. A proof-of-concept implementation and experimental evaluation of these algorithms, based on LydiaSyft+ (Hausmann et al. 2025), demonstrating that synthesis for the LTLf + obligation fragment can be solved very efficiently, achieving performance comparable to synthesis for LTLf .

2

Preliminaries

LTL and LTLf . Linear-time Temporal Logic (LTL) specifies temporal properties of infinite traces (Pnueli 1977). We use the standard syntax φ, ψ ::= p | ¬φ | φ ∧ ψ | X φ | φ U ψ,

(p ∈ AP )

where AP is a countable set of atomic propositions. Common abbreviations include φ ∨ ψ = ¬(¬φ ∧ ¬ψ), true = p ∨ ¬p, false = p ∧ ¬p, F φ = true U φ (“eventually”) and Gφ = ¬F¬φ (“always”). Formulas are evaluated over infinite traces τ ∈ (2AP )ω . LTL is expressively equivalent to first-order logic over infinite traces (Kamp 1968). LTL on finite traces (LTLf ) (De Giacomo and Vardi 2013) uses the same syntax but is interpreted over finite traces τ ∈ (2AP )∗ . In this setting, X false holds exactly at the last position of a finite trace. A common abbreviation is the operator X[!]φ = ¬X¬φ (“strong next”), expressing the existence of a next position in the trace that satisfies φ. Given an LTLf formula Φ, let [Φ] = {τ ∈ (2AP )∗ | τ, 0 |= Φ} denote the set of finite traces that satisfy Φ at position 0. LTLf is expressively equivalent to first-order logic over finite traces and to star-free regular expressions, see (De Giacomo and Vardi 2013). Automata on finite traces. A transition system T = (Σ, Q, I, δ) consists of a finite alphabet Σ, a finite set Q of states, a set I ⊆ Q of initial states, and a transition relation δ ⊆ Q × Σ × Q. For q ∈ Q and a ∈ Σ, define δ(q, a) = {q ′ ∈ Q | (q, a, q ′ ) ∈ δ}. The system is deterministic if |I| = 1 and |δ(q, a)| = 1 for all q ∈ Q and a ∈ Σ, and nondeterministic otherwise; in the deterministic case, we write δ(q, a) = q ′ for the unique successor and denote the initial state by ι. A finite automaton A = (T, F ) is a transition system together with a set F ⊆ Q of accepting states. If T is deterministic, A is a deterministic finite automaton (DFA); otherwise it is a nondeterministic finite

automaton (NFA). A run of A on a word w ∈ Σ∗ is a path starting from an initial state whose sequence of transition labels is w; it is accepting if it ends in a state from F . The automaton accepts the language L(A) consisting of all finite words for which an accepting run exists. For each LTLf formula Φ, one can construct an equivalent O(|Φ|) NFA of size 2O(|Φ|) and an equivalent DFA of size 22 represented symbolically (De Giacomo and Vardi 2015). Infinite-duration games on finite graphs. A game arena is a finite directed graph A = (V, E ⊆ V × V ) whose vertex set is partitioned into system nodes Vs and environment nodes Ve . For v ∈ V , define E(v) = {v ′ | (v, v ′ ) ∈ E} and assume E(v) ̸= ∅ for all v. A play is a path in A. A memoryless strategy for the system player is a function σ : Vs → V that assigns to every system node v ∈ Vs a successor σ(v) ∈ E(v). A play v1 v2 . . . is compatible with a σ if whenever vi ∈ Vs , we have vi+1 = σ(vi ). An objective is a set of infinite plays; a play is winning for the system player if belongs to the objective. We consider Büchi and co-Büchi objectives specified by sets F ⊆ V : Büchi objectives require visiting F infinitely often, whereas co-Büchi objective require visiting V \ F finitely often. Strategies and winning plays for the environment player are defined dually. A strategy for a player wins a node v if every compatible play starting at v is winning for that player. Büchi and co-Büchi games are positionally determined: every node is won by exactly one player, and memoryless (positional) strategies suffice. Solving a game amounts to computing winning regions together with witnessing strategies. Reactive synthesis and games. Assume that the set AP of atomic propositions is partitioned into system actions X and environment actions Y . A (synthesis) strategy is a function σ : (2Y )∗ → 2X . An outcome of σ is an infinite word (x1 ∪ y1 )(x2 ∪ y2 ) . . . ∈ (2AP )ω such that xi+1 = σ(y1 y2 . . . yi ) for all i ≥ 0. Thus, synthesis strategies encode transducers. The synthesis problem for a temporal formula Ψ asks whether there exists a synthesis strategy σ such that every outcome of σ satisfies Ψ, and if so, to construct one. A deterministic transition system T = (2AP , Q, ι, δ) induces a game arena AT = (Q ∪ Q × 2X ∪ Q × 2X × 2Y , E) in which the system owns nodes in Q and the environment owns all other nodes. Transitions are defined by E(q) = {q} × 2X , E(q, x) = {(q, x)} × 2Y , and E(q, x, y) = {δ(q, x ∪ y)}. Plays of the form q1 (q1 , x1 )(q1 , x1 , y1 )q2 (q2 , x2 )(q2 , x2 , y2 ) . . . induce runs q1 q2 . . . of T on the word (x1 ∪ y1 )(x2 ∪ y2 ) . . .. Hence, the synthesis problem reduces to translating the specification into a deterministic transition system and solving the induced game with an appropriate objective.

3

Specification of Obligation Properties

In their seminal work, Manna and Pnueli introduced a hierarchy of ω-regular languages (Manna and Pnueli 1990). We apply this hierarchy to LTL-definable properties, i.e.,

properties definable in first-order logic over infinite sequences. The hierarchy is based on four fundamental classes of infinite-trace properties obtained from finite-trace properties via trace quantification. Safety properties require that a finite-trace property holds for all prefixes, whereas guarantee properties require the existence of a prefix satisfying the finite-trace property. Recurrence properties require that the finite-trace property holds on infinitely many prefixes, and persistence properties require it to hold on all but finitely many prefixes. Obligation properties are Boolean combinations of safety and guarantee properties, and reactivity properties are Boolean combinations of recurrence and persistence properties. In this work, we focus on obligation properties. These properties naturally capture specifications that combine invariants with eventual goals and therefore arise frequently in planning, control, and reactive synthesis. The recently proposed logic LTLf + (Aminof et al. 2025b), which is inspired by the Manna-Pnueli hierarchy, uses LTLf properties to define the finite-trace properties mentioned in the hierarchy description. Namely, it explicitly uses guarantee, safety, recurrence, and persistence properties over LTLf properties, and considers Boolean combinations of them. Formulas of LTLf + over a countable set AP of propositions are generated by the grammar Ψ, Ψ′ ::= ∀Φ | ∃Φ | ∀∃Φ | ∃∀Φ | Ψ ∨ Ψ′ | Ψ ∧ Ψ′ | ¬Ψ where Φ is an LTLf formula over AP . We refer to formulas of the form QΦ as finite-trace components. Recall that [Φ] ⊆ (2AP )∗ denotes the set of finite traces satisfying Φ. Given a set R ⊆ (2AP )∗ of finite traces, let ∃R (∀R) denote the set of infinite traces τ ∈ (2AP )ω such that at least one prefix of τ (respectively, every prefix) belongs to T . Similarly, let ∀∃T (∃∀T ) denote the set of infinite traces for which infinitely many prefixes (respectively, all but finitely many prefixes) belong to T . We evaluate LTLf + formulas Ψ over infinite traces using the extension [Ψ] ⊆ (2AP )ω defined inductively by [Ψ ∨ Ψ′ ] = [Ψ] ∪ [Ψ′ ], [Ψ ∧ Ψ′ ] = [Ψ] ∩ [Ψ′ ], [¬Ψ] = (2AP )ω \ [Ψ], and [QΦ] = Q[Φ] where Q ∈ {∃, ∀, ∀∃, ∃∀}. Theorem 1. (Aminof et al. 2025b) The logics LTLf + and LTL define the same infinite-trace properties, namely those definable in first-order logic over infinite sequences. The obligation fragment of LTLf + is obtained by allowing only safety and guarantee finite-trace components, i.e., by using only the clauses ∃Φ and ∀Φ from the syntax. We refer to formulas in this fragment as obligation formulas. As an example, suppose a domain and a collection of goals are specified by finite-trace LTLf formulas V Φd and Φg1 ,. . . ,Φgk . The obligation formula ∀Φd → ( i≤k ∃Φgi ) states that every infinite trace that remains within the domain eventually satisfies each V goal. Goals can be made conditional using ∀Φd → ( i≤k (∃Φti → ∃Φgi )) where Φti specifies a triggering property for the ith goal. This formula states that whenever a trigger occurs along a trace that stays within the domain, the corresponding goal is eventually achieved (either before or after the trigger occurs). Not every property is expressible as an obligation formula. For

example, the recurrence formula ∀∃(F(a ∧ X false)) states that infinitely many prefixes end with a, equivalently, that a holds infinitely often. Lemma 1. The obligation fragment of LTLf + defines exactly the obligation properties over infinite traces. Remark 1. Alongside LTLf +, (Aminof et al. 2025b) introduces the related and equally expressive logic PPLTL+, in which finite-trace specifications are formulated in Pure Past LTL (PPLTL) rather than in LTLf . We focus our technical developments on the obligation fragment of LTLf +, but emphasize that the synthesis algorithms we propose extend directly to the obligation fragment of PPLTL+. Since PPLTL formulas can be translated into DFA of single-exponential size, the upper bounds in the PPLTL+ counterparts of Corollary 2 and Theorem 2 are singly exponential. The obligation fragment of LTL, obtained by imposing syntactic restrictions on classical LTL formulas, has the same expressive power and thus also characterizes the obligation properties over infinite traces (Chang, Manna, and Pnueli 1992). Definition 1. The synthesis problem for obligation LTLf + asks, given an obligation formula Ψ, whether there exists a strategy σ such that every outcome of σ satisfies Ψ, and if so, to construct one. Lemma 2. Let Φ and Φ′ be LTLf formulas. Then ∀Φ ∧ ∀Φ′ ≡ ∀(Φ ∧ Φ′ )

∃Φ ∨ ∃Φ′ ≡ ∃(Φ ∨ Φ′ )

Moreover, Φ is equi-realizable with the LTLf + formula ∃Φ. Since obligation formulas form a fragment of LTLf +, their synthesis problem can be solved using techniques for the full logic, based on games over deterministic EmersonLei automata (DELA), whose objectives are Boolean combinations of Büchi and co-Büchi conditions (Aminof et al. 2025b; Hausmann et al. 2025). These methods translate individual finite-trace components into Büchi or co-Büchi automata and obtain a DELA by Boolean combination of the individual automata. The resulting game is solved via a nested fixpoint computation derived from the Zielonka tree of the acceptance condition (Hausmann, Lehaut, and Piterman 2024); solving DELA games is known to be PS PACEcomplete. We show that obligation formulas admit a reduction to substantially simpler ω-automata, enabling efficient minimization and linear-time game solving.

4

From Obligations to DWA

In this Section, we transform obligation formulas into deterministic weak automata (DWA) on infinite words. In every run of a DWA, there exists a position from which on only accepting states or only rejecting states are visited. Owing to this structural property, DWA are simpler than Büchi and co-Büchi automata, and, in many respects, similar to DFA. In particular, DWA are closed under conjunction and disjunction and can be minimized efficiently using a variant of Hopcroft’s DFA minimization algorithm. Each finite-trace component QΦ of an obligation formula corresponds to a DWA: the finite-trace formula Φ can be

transformed to a DFA AΦ that accepts exactly the finite traces that satisfy Φ. The automaton for QΦ then processes infinite traces τ and checks whether AΦ accepts some prefix of τ (if Q = ∃), or all prefixes of τ (if Q = ∀). This is achieved by turning accepting (respectively, rejecting) states in AΦ into absorbing sinks. An infinite run of the resulting automaton AQΦ is accepting iff it visits an accepting state infinitely often, which in turn is the case iff from some position onward only accepting states are visited. As DWA are closed under conjunction and disjunction, we can construct DWA for full obligation formulas, which are Boolean combinations of safety and guarantee finitetrace components. Weak Büchi automata. We consider standard automata on infinite traces. A Büchi automaton A = (T, F ) is a transition system T = (Σ, Q, ι, δ) together with a set F of accepting states. A run of T on an infinite word w = a1 a2 . . . ∈ Σω is an infinite sequence π = q1 q2 . . . ∈ Qω of states such that q1 = ι and qi+1 ∈ δ(qi , ai ) for all i ≥ 1. The automaton recognizes the (ω-regular) language L(A) of all words w ∈ Σω for which there exists a run that visits states in F infinitely often. Dually, a co-Büchi automaton recognizes the language of all words admitting a run that visits rejecting states only finitely often. A strongly connected component (SCC) of a transition system T = (Σ, Q, ι, δ) is a maximal set S ⊆ Q of states such that every state in S is reachable from every other state in S. The SCC decomposition of Q can be computed in time O(|Q| + |δ|). Reachability induces a partial order on SCCs; a bottom SCC is a minimal element of this order. A state is recurrent if it can reach itself via a non-empty path, and transient otherwise. An automaton (T, F ) is weak if every SCC S is either entirely accepting (S ⊆ F ) or entirely rejecting (S ∩ F = ∅) (Löding 2001).1 For weak automata, Büchi and co-Büchi acceptance coincide: every infinite run that visits an accepting state infinitely often must eventually remain within an accepting SCC. Hence we simply refer to deterministic weak Büchi automata as deterministic weak automata (DWA). Closure properties of DWA. To translate obligation formulas into ω-automata, we require closure under intersection and union. Given deterministic transition systems T1 = (Σ, Q1 , ι1 , δ1 ) and T2 = (Σ, Q2 , ι2 , δ2 ), their product is the transition system T1 ⊗ T2 = (Σ, Q1 × Q2 , (ι1 , ι2 ), δ⊗ ) where δ⊗ ((q1 , q2 ), a) = (δ1 (q1 , a), δ2 (q2 , a)). Lemma 3. The set of languages recognizable by DWA is closed under union, intersection, and complement. Proof. (Sketch) Complementation is obtained by swapping accepting and rejecting states. Union and intersection are realized via the product construction with accepting sets 1 This definition is different from, though equivalent to, the one in Section 9.1.5 of (Hofmann and Lange 2025).

F1 × F2 (intersection) and (Q1 × F2 ) ∪ (F1 × Q2 ) (union). All constructions preserve weakness. DWA minimization. For every DWA A, there exists a unique minimal equivalent DWA that can be computed in time O(n log n), where n is the number of states (Löding 2001). DFA minimization using the Hopcroft algorithm can be applied once the automaton is brought into a suitable normal form. This form can be obtained in linear time by marking transient states accepting or rejecting according to their rank. Intuitively, the rank of a state q is the maximum number of alternations between accepting and rejecting recurrent states along runs starting from q. States with different ranks are not equivalent, as higher ranks induce additional accepted or rejected words. Transient states are marked accepting iff their rank is even, allowing Hopcroft’s algorithm to merge them with maximally ranked successors. Formally, define rank(S) for SCCs S inductively. Bottom accepting and rejecting SCCs have rank 0 and 1, respectively. For a non-bottom SCC S, let l(S) be the maximum rank among its successors in the SCC decomposition. If S is transient, set rank(S) = l(S). If S is recurrent, set rank(S) = l(S) + 1 when parity disagrees with acceptance, and rank(S) = l(S) otherwise. The rank of a state is the rank of its SCC and can be computed in time O(|A|). Hence, recurrent states have even rank iff they are accepting. Given a DWA A = (T, F ) with state set Q, define F ′ = {q ∈ Q | rank(q) is even} and put A′ = (T, F ′ ); this does not change the marking of recurrent states. Applying Hopcroft minimization to A′ yields Amin . Lemma 4. (Löding 2001) Amin is the minimal DWA equivalent to A. Corollary 1. Deterministic weak automata with n states can be minimized in time O(n log n). From obligation formulas to DWA. Recall that obligation formulas are Boolean combinations of components QΦ, where Φ is a finite-trace formula and Q ∈ {∃, ∀} a guarantee or safety trace quantifier. We first translate individual components into equivalent ω-automata. Given an LTLf formula Φ over AP , let AΦ = (TΦ , F ) with TΦ = (2AP , Q, ι, δ) denote an equivalent DFA of size O(|φ|) 22 , represented symbolically. Assume ι ∈ / F when Q = ∃ and ι ∈ F when Q = ∀. Let TΦ+ = (2AP , Q, ι, δ + ) and TΦ− = (2AP , Q, ι, δ − ) be obtained from TΦ by turning accepting (respectively, rejecting) states into absorbing sinks: define δ + (q, a) = q if q ∈ F and δ + (q, a) = δ(q, a) otherwise, and δ − (q, a) = q if q ∈ / F and δ − (q, a) = δ(q, a) otherwise. Lemma 5. Let Φ be an LTLf formula and Q ∈ {∃, ∀}. Then there exists a DWA AQΦ equivalent to QΦ such that – if Q = ∃, then AQΦ = (TΦ+ , FΦ ); – if Q = ∀, then AQΦ = (TΦ− , FΦ ). Proof. (Sketch) Let AΦ = (TΦ , FΦ ) be a DFA for Φ. If Q = ∃, an infinite trace satisfies ∃Φ iff some finite prefix is

accepted by AΦ ; making accepting states absorbing in TΦ+ yields a DWA that accepts exactly those runs that eventually remain in FΦ . If Q = ∀, a trace satisfies ∀Φ iff every prefix is accepted; making rejecting states absorbing in TΦ− ensures that leaving F is permanent, so acceptance coincides with staying in FΦ forever. In both constructions, SCCs do not mix accepting and rejecting states due to the absorbing sinks, hence the automata are weak. This leads to the following transformation from obligation LTLf + formulas to weak automata. Corollary 2. Every obligation LTLf + formula Ψ can be O(|Ψ|) translated into an equivalent DWA of size 22 . Proof. Translate each component QΦ using Lemma 5 and combine the resulting automata according to the Boolean structure of Ψ via the closure constructions of Lemma 3. The automata produced during this construction may be minimized at any stage using Corollary 1. Structural properties of the constructed DWA. The automata constructed for a given obligation formula Ψ via Corollary 2 have a particular internal structure. Accepting states in the individual automata for guarantee finite trace components are turned into accepting sinks. These sink states can be merged, leading to individual automata that have just a single accepting (sink) state and in which all other states are rejecting. Dually, the individual automata for safety components can be assumed to have just a single rejecting sink state. In both cases, it is not possible to leave the sink state, once it has been reached. After composing the individual automata using the constructions from Lemma 3, the resulting DWA is partitioned according to acceptance/non-acceptance of the individual automata. Let there be k finite trace components. Then every set σ ⊆ {1, . . . , k} identifies a region in the composed automaton where component automata are in accepting states if and only if their index is contained in σ. Formally, let QΨ denote the state set of the composed DWA. Then every state in QΨ is of the shape (q1 , . . . , qk ) where qi is a state in AQi Φi . Put Qσ = {(q1 , . . . , qk ) ∈ Q | qi ∈ FΦi iff i ∈ σ}. Then the sets Qσ for σ ⊆ {1, . . . , k} form a partition of QΨ . Since all states in a single such set agree on acceptance of the individual component automata, we have that each Qσ is either fully accepting (Qσ ⊆ FΨ ) or fully rejecting (Qσ ∩ FΨ = ∅), depending on whether σ corresponds to a satisfying valuation of the Boolean formula structure of Ψ. Furthermore, for all i such that Qi = ∃ and i ∈ σ, or Qi = ∀ and i ∈ / σ, all states in Qσ have the same state as ith component – it is the sink state of the automaton AQi Φi . Since it is not possible to leave sink states in individual automata, there is, for every strongly connected component S in AΨ , some σ ⊆ {1, . . . , k} such that S ⊆ Qσ . Also, for all σ, σ ′ ⊆ {1, . . . , k} such that σ ̸= σ ′ , Qσ may be reachable from Qσ′ or vice versa, but not both. Hence, reachability partially orders the sets Qσ , arranging them in a DAG structure.

This does not provide a full SCC decomposition of AΨ since a single set Qσ may consist of several SCCs, which, however, are either all fully accepting or all fully rejecting.

5

Synthesis via DWA

We show how the synthesis problem for obligation LTLf + can be reduced to the solution of games over deterministic weak automata (DWA). Our procedure builds on Lemma 5 and Corollary 2. We introduce infinite-duration games over graphs, present the reduction to DWA games, and discuss several symbolic algorithms for solving such games. In particular, we recall the classical solutions via Büchi games and co-Büchi games and propose a novel symbolic algorithm that iteratively solves safety and reachability computations. These algorithms all have quadratic runtime. Finally, we show that the novel algorithm can be made linear by restricting its fixpoint computations to individual SCCs of the game graph; the resulting algorithm resembles the one described in (Amram et al. 2021). Formally, a DWA (or weak) game is a Büchi game G = (A, F ) that is induced by a DWA. Hence every SCC of A is either contained in F or does not intersect with F . The objective of the system player is to visit F infinitely often (equivalently, to eventually remain within F forever). Synthesis as DWA games. We reduce the reactive synthesis problem for the obligation fragment of LTLf + to the solution of DWA games. Consider an input obligation formula Ψ given in positive normal form, expressed as a positive Boolean formula over k components Qi Φi , where Qi ∈ {∃, ∀} and each Φi is an LTLf formula. The synthesis algorithm transforms Ψ into an equivalent DWA (according to Corollary 2) and then solves the DWA game induced by this automaton. Step 1. Convert each component Qi Φi into an equivalent DWA AQi Φi according to Lemma 5: Transform Φi into the DFA (TΦi , FΦi ), where TΦi = (2AP , QΦi , ιΦi , δΦi ). If Qi = ∀, put AQi Φi = (TΦ−i , FΦi ); if Qi = ∃, put AQi Φi = (TΦ+i , FΦi ). Step 2. Compose the automata AQi Φi according to the Boolean structure of Ψ (repeatedly using Lemma 3): Construct the DWA AΨ = (TΨ , FΨ ) inductively as follows. TΨi ∧Ψj = TΨi ∨Ψj = TΦi ⊗ TΦj

FΨi ∧Ψj = FΨi × FΨj

FΨi ∨Ψj = FΨi × QΦj ∪ QΦi × FΨj At any stage, the (partially) composed DWA can be minimized according to Corollary 1. Step 3. Solve the DWA game induced by AΨ . If the system player wins from the initial state (ι1 , . . . , ιk ) of TΨ , extract a witnessing strategy.

Theorem 2. The synthesis problem for the obligation fragment of LTLf + can be decided symbolically via DWA games in 2E XP T IME. More precisely, consider an input formula Ψ of size n. The constructed DWA game over AΨ has size at most n′ = n 2 2 . Notably, this bound depends neither on the number of finite-trace components in Ψ nor on its Boolean structure, but only on the overall size of Ψ. By Lemma 8 below, the DWA game can be solved symbolically in time O(n′ ). Therefore, the worst-case time complexity for synthesizing obligation properties matches that of reactive synthesis for LTLf. Remark 2. All steps in the described synthesis algorithm admit symbolic implementations. Remark 3. For a realizable specification Ψ, the corresponding transducer is obtained by extracting a memoryless winning strategy for the system player in the DWA game induced by AΨ (see, e.g., the proof of Lemma 8). Solution of DWA Games. We now present several symbolic algorithms for solving DWA games. Since DWA games can be viewed as both Büchi and co-Büchi games with a particular structure, they can be solved using standard algorithms for these classes. In the worst case, however, this is unnecessarily expensive, as the best known algorithms for (co-)Büchi games have quadratic runtime in the arena size. Nevertheless, we briefly recall the classical nested fixpoint algorithms. Next, we propose an apparently novel algorithm that solves DWA games via iterative safety and reachability computations, thereby avoiding the computation of nested fixpoints. Although its worst-case runtime is again quadratic, the algorithm may perform better in practice because the intermediately computed winning regions grow monotonically. Finally, we recall a specialized algorithm for DWA games that decomposes the arena into SCCs and solves the resulting DAG, applying safety and reachability computations to single SCCs in a bottom-up manner, thereby achieving linear worst-case runtime. We begin by defining monotone operators for the symbolic computation of one-step strategies in a given game arena A = (V, E): ♢W = {v ∈ V | E(v) ∩ W ̸= ∅}, □W = {v ∈ V | E(v) ⊆ W }, CPres (W ) = (Vs ∩ ♢W ) ∪ (Ve ∩ □W ), CPree (W ) = (Vs ∩ □W ) ∪ (Ve ∩ ♢W ), for W ⊆ V . Here, ♢ computes the set of nodes with an outgoing edge to the argument set, while □ computes the set of nodes whose outgoing edges all lead to the argument set. Consequently, the controllable predecessor operators CPres and CPree compute the nodes from which the system and environment, respectively, have a one-step strategy to reach the argument set. A symbolic operation is the evaluation of an expression of the form W1 ∩ W2 , W1 ∪ W2 , or ¬W1 for symbolic sets

W1 , W2 (encoded, e.g., by BDDs). We measure time complexity by the number of symbolic operations. Under this measure, computing CPres (W ) or CPree (W ) requires symbolic time O(1). Let f : 2V → 2V be a monotone function. Its extremal (least and greatest) fixpoints are defined as µX. f (X) = {Z ⊆ V | f (Z) ⊆ Z} = f |V | (∅) νX. f (X) = {Z ⊆ V | Z ⊆ f (Z)} = f |V | (V ) where f i+1 (Z) = f (f i (Z)) for i ≥ 0 and f 0 (Z) = Z. Hence, a single extremal fixpoint over V can be computed in symbolic time O(|V |), assuming that f can be evaluated in constant symbolic time. We recall standard fixpoint constructions for games, and associated results. Define Reach(W, T ) = µX.T ∪ (W ∩ CPres (X)), Safe(W, T ) = νX.T ∪ (W ∩ CPres (X)), Büchi(T ) = νX.µY.(T ∩ CPres (X)) ∪ CPres (Y ), co-Büchi(T ) = µX.νY.(F ∩ CPres (Y )) ∪ CPres (X). Here, Reach(W, T ) computes the system player’s winning region in a game over W ∪ T with the objective to eventually reach T , while Safe(W, T ) computes the winning region with the objective to either remain in W forever or eventually reach T . Both sets can be computed in symbolic time O(|W |). Lemma 6. Let A be an arena and F a set of game nodes. Then Büchi(F ) is the winning region of the system player in the Büchi game G = (A, F ), while co-Büchi(F ) is the winning region of the system player in the co-Büchi game G = (A, F ). Corollary 3. Büchi games and co-Büchi games with n nodes can be solved in symbolic time O(n2 ). Alternating safety and reachability. We now consider Algorithm 1, which solves DWA games without computing nested fixpoints. Although the runtime remains quadratic, the algorithm decouples the least and greatest fixpoint computations used in (co-)Büchi solutions. The algorithm maintains a growing sequence of winning regions Wi , starting from W0 = ∅. In iteration i, it solves: – a game over F ∪ W2i with the objective to either stay in F forever or eventually reach W2i , and – a reachability game over V with target set W2i+1 . The corresponding fixpoints are W2i+1 = Safe(F, W2i ) W2i+2 = Reach(V, W2i+1 )

(line 3) (line 4)

Thus, S OLVE S AFE R EACH(V, F ) computes the set of nodes from which the system player has a strategy to eventually stay within an accepting SCC forever. We observe that W2i ⊆ W2i+1 ⊆ W2(i+1) for all i. Consequently, the fixpoint computations in later iterations operate on larger target sets (W2i and W2i+1 , respectively) and therefore terminate more quickly.

Algorithm 1: S OLVE S AFE R EACH(V,F) i = 0; W0 = ∅; W−2 = V while W2i ̸= W2(i−1) do 3 W2i+1 = Safe(F, W2i ) 4 W2i+2 = Reach(V, W2i+1 ) 5 i=i+1 6 return W ; 1

Lemma 8. Algorithm 2 solves weak games with n nodes in symbolic time O(n) and yields memoryless winning strategies for the system player.

2

Algorithm 2: S OLVE W EAK SCC(V ,F ,SCCs) 1 W =∅ 2 while SCCs ̸= ∅ do 3 B = bottomSCCs(SCCs) 4 SCCs = SCCs \ B 5 for SCC ∈ B do 6 if SCC ⊆ F then 7 X = Safe(SCC, W) 8 else // SCC ∩ F = ∅ 9 X = Reach(SCC, W) 10 W =W ∪X 11

return W

Lemma 7. Algorithm 1 solves weak games with n nodes, k accepting nodes and l SCCs in symbolic time O(n + kl) ∈ O(n2 ), and yields memoryless winning strategies for the system player. Proof. Correctness follows directly from the construction of the algorithm. The total number of symbolic operations required to compute all sets Reach(V, Wj ) is linear in n, since each game node is added to the winning region at most once. Furthermore, at most l computations of Safe(F, Wj ) are needed; each such computation can be implemented in symbolic time O(k), where k = |F |. A winning strategy is obtained by playing, at each game node v, according to the memoryless winning strategy for the game associated with Wj , where j is the smallest index such that v ∈ Wj .

Linear solution of weak games. Algorithm 1 can be made linear by parameterizing it with an SCC decomposition of the game arena and restricting fixpoint computations to individual SCCs. This results in Algorithm 2, which is similar to the algorithm proposed in (Amram et al. 2021). It takes a game together with its SCC decomposition as input and solves the DAG of SCCs in a bottom-up fashion by repeatedly processing all bottom SCCs and removing them from the DAG. The algorithm assumes a function BOTTOM SCC S that returns the current minimal SCCs. The winning region computed so far is stored in the set W . Each bottom SCC is handled as follows. If the SCC is accepting, the algorithm solves a game over the union of the SCC and W with the objective to either remain within the SCC forever or eventually reach W . If the SCC is rejecting, the objective is just to eventually reach W .

Proof. (Sketch) The algorithm computes precisely the set of nodes for which the system player has a strategy to eventually stay in some accepting SCC forever. Regarding time complexity, graphs with n vertices can be decomposed into their SCCs in symbolic time O(n) (Larsen et al. 2023). For each strongly connected component SCC, Algorithm 2 computes exactly one of the sets Reach(SCC, W ) or Safe(SCC, W ), each of which can be obtained in symbolic time O(|SCC|). Since the sizes of all SCCs sum to n, the overall runtime is linear. A memoryless strategy is constructed by always following the memoryless safety or reachability strategy for the current SCC.

6

Implementation

We implemented all the algorithms mentioned above by extending the LTLf + synthesis tool LydiaSyft+ (Hausmann et al. 2025). We first describe the implementation of the game arena construction and then detail the implementation of the gamesolving algorithms. Given an obligation LTLf + formula Ψ, each finite-trace component QΦ is converted into a DWA by translating the LTLf formula Φ into a DFA using MONA’s explicit representation (Klarlund, Møller, and Schwartzbach 2002), which then is treated as a DWA. Subsequently, the composition constructions described in Section 4 are applied along the Boolean structure of Ψ. We implemented DWA minimization in an explicit representation, applying Löding’s pre-processing step (Löding 2001), followed by DFA minimization using MONA. We consider two modes for obtaining the automata: • Component-wise minimization + symbolic product: Each component DWA is minimized individually, after which the product is constructed symbolically. This approach results in n minimization calls for n components. • Incremental explicit products + threshold-based switching: Intermediate products are kept explicit and are minimized as long as the number of states remains below a fixed threshold τ (we use τ = 256). Once the threshold is exceeded, we switch to a symbolic representation for subsequent products. To further control the sizes of product automata, we compute products in a balanced manner. At the end of the arena construction, both variants yield symbolic games played over DWA. These games are solved as follows. Direct fixpoint computation algorithms. We implemented the classical fixpoint computations for the symbolic solution of Büchi and co-Büchi games, as we well as the novel Algorithm 1 (referred to as “SafeReach” below). These algorithms integrate seamlessly into the LydiaSyft+ infrastructure, as they compute fixpoints directly over the BDD representation of the game arena.

102

runtime (s)

101

100

10−1

10−2

10−3 2

3

4

5

6

7

8

9

pattern size SCC [m] SCC

SafeReach [m] SafeReach

Büchi [m] Büchi

co-Büchi [m] co-Büchi

EL

Figure 1: Runtime of solvers on the counter pattern ψ

SCC-based solution algorithm. Although Algorithm 2 is theoretically more efficient, implementing linear-time SCC decomposition is not straightforward with the automaton representation used by LydiaSyft+. Existing linear-time algorithms assume a monolithic, fully symbolic encoding of the transition relation with primed successor variables (i.e., transitions encoded as a function T (x, x′ )). In contrast, LydiaSyft+ employs a partitioned encoding that facilitates pre-image computation but makes post-image computation more difficult. In our implementation of SCC decomposition, we follow the established FwdBwd approach, using an implementation similar to (Amram et al. 2021). Specifically, we first convert the transition relation to the primed encoding and then compute the path relation required for SCC decomposition via transitive closure. We also considered implementing the fully symbolic Chain algorithm (Larsen et al. 2023). However, this algorithm optimizes only the SCC computation itself. This does not address the overhead of constructing the monolithic transition relation. Since this construction constitutes the dominant bottleneck in our setting, we do not expect the Chain algorithm to significantly improve scalability.

7

Experiments

We conduct experiments on a range of formula patterns to study the scalability of the proposed algorithms. The evaluation is intended as a proof of concept and therefore does not rely on extensive computational resources. Overall, our results demonstrate that the obligation fragment can be solved with effectivity comparable to standard LTLf synthesis. All experiments were carried out on an M4 MacBook Air with 16GB RAM of which 12GB were allocated to the virtual experiments, using a time limit of 10 minutes per benchmark. When discussing experiment results, we refer to the four synthesis algorithms detailed above by “Büchi”, “coBüchi”, “SafeReach”, and “SCC”. Versions that employ incremental minimization are marked with “[m]” and plotted using solid lines (dashed lines are used to plot the runtime for algorithms that build the component-wise symbolic product of minimized automata). We additionally compare our methods with the LydiaSyft+ implementation of synthesis for full LTLf + based on a reduction to EmersonLei games (denoted “EL” in the plots); this algorithm does not support incremental minimization. Finally, we compare against the LydiaSyft+ implementation of LTLf synthesis

(denoted by “LTLf”), where possible. To ensure a fair comparison, we disabled one-step realizability checks using Z3, as these trivially solve the instance. We begin by adapting the counter benchmark commonly used in LTLf and LTLf + synthesis, which specifies a binary counter with n bits b0 , . . . , bn−1 with the overall system objective to reach the maximal counter value, expressed as a guarantee property. The original LTLf + formulation (Hausmann et al. 2025) does not belong to the obligation fragment, as it employs a recurrence property to require that the counter is incremented infinitely often. We modify this specification by incorporating the increment requirement into the LTLf formula for the domain. More specifically, we require that the counter is incremented at every step (φalw ), resulting in the following realizable specification in which the system controls the variable add: ψ = ∀(φinit ∧ φinc ∧ φalw ∧ φtrans ) ⊃ ∃φgoal φinit = ¬c0 ∧ · · · ∧ ¬cn−1 ∧ ¬b0 ∧ · · · ∧ ¬bn−1 φinc = G(add ⊃ (X(c0 ) ∧ X(X(c0 )) ∧ X(X(X(c0 ))))) φalw = GF(add ∧ X false)  ((¬ci ∧ ¬bi ) → X(¬bi ∧ ¬ci+1 ))∧    ((¬c ∧ b ) → X(b ∧ ¬c ))∧ i i i i+1 φtrans = G  ((c ∧ ¬b ) → X(b ∧ ¬c i i i i+1 ))∧   ((ci ∧ bi ) → X(¬bi ∧ ci+1 )) φgoal = F (b0 ∧ · · · ∧ bn−1 ∧ X false) Figure 1 shows the runtimes of the various implementations on this benchmark series. In this case, DFA construction accounts for the majority of the runtime, while solving the resulting game is comparatively fast. Consequently, the overall runtime is dominated by the construction of the LTLf component automata, leading to nearly identical performance across all algorithms. Minimization does not significantly reduce the number of states in this benchmark. This appears to be due primarily to the minimization threshold being set to 256: once the automaton for the LTLf domain exceeds this size, minimization is no longer performed. Increasing the DWA minimization threshold is unlikely to yield significant performance gains, as DFA construction already constitutes the principal cost in this example. To evaluate synthesis for basic Boolean combinations of finite-trace components, we consider several formula patterns obtained by combining LTLf formulas of the form φi = F((ei ∨ ai ) ∧ X false) with different boolean operators and trace quantifiers. The environment controls variables ei and the system controls variables ai . In consequence, all formulas in this experiment are realizable. We omit patterns in which the number of finite-trace components can be reduced using Lemma 2. V

i ∃i ∧ ∀ :

∃φ1 ∧ · · · ∧ ∃φn−1 ∧ ∀φn

V

i ∃i ∧ ∃ :

∃φ1 ∧ · · · ∧ ∃φn

W

i ∀i ∨ ∀ :

∀φ1 ∨ · · · ∨ ∀φn

W

i ∀i ∨ ∃ :

∀φ1 ∨ · · · ∨ ∀φn−1 ∨ ∃φn

The ∃ pattern V introduced in (Hausmann et al. 2025) corresponds to the i ∃i ∧ ∃ pattern. We refer to the number of conjuncts or disjuncts as the pattern size.

103

2

102

101

101

runtime (s)

10

runtime (s)

103

100

100

10−1

10−1

10−2

10−2

10

−3

10−3 5

10

15

20

5

10

15

pattern size SCC [m] SCC

SafeReach [m] SafeReach

Büchi [m] Büchi

V

i ∃i ∧ ∀

(a)

SCC [m] SCC

103

2

102

101

101

100

10−1

10−2

10−2

10

−3

Büchi [m] Büchi

V

co-Büchi [m] co-Büchi

25

EL

LTLf

i ∃i ∧ ∃

100

−1

10

SafeReach [m] SafeReach

(b)

runtime (s)

runtime (s)

EL

103

10

20

pattern size co-Büchi [m] co-Büchi

10−3 5

10

15

20

5

10

15

pattern size SCC [m] SCC

SafeReach [m] SafeReach

Büchi [m] Büchi

W

i ∀i ∨ ∀

(c)

20

pattern size co-Büchi [m] co-Büchi

EL

SCC [m] SCC

SafeReach [m] SafeReach

Büchi [m] Büchi

W

i ∀i ∨ ∃

(d)

co-Büchi [m] co-Büchi

EL

Figure 2: Runtime of solvers for conjunction and disjunction patterns

Figure 2 shows the runtime of the algorithms on these benchmarks for growing pattern sizes. In most of these examples, we observe a clear separation between the SCC, EL, and Büchi-based algorithms, both in terms of runtime and the number of instances solved. With the exception of the SCC-based implementation, our new methods perform similar to the existing algorithms. We attribute the comparatively good performance of the EL-based solver for experiments on conjunctions of guarantuee properties (Figures 2(a) and 2(b)) to the fact that the EL solver constructs and solves generalized Büchi games in these experiments. Using this approach, the EL solver decomposes the overall objective into several subobjectives that can be solved independently. An overall solution is obtained by composing the solutions for the subobjectives. This apparently can lead to advantages over the Büchi-based algorithms which solve games with a single monolithic objective, which is simpler but may require more iterations until a fixpoint is obtained. Because the patterns in this experiment are designed to be irreducible under the simplification rules from Lemma 2, it is not surprising that minimization in most cases does not substantially V reduce the number of states. The only exception is the i ∃i ∧ ∀ pattern, where minimization decreases the state count by up to 50%, but does not reduce the bit count of the BDD representation. We attribute the comparatively weak performance of the SCC-based algorithm primarily to implementation effects, in particular the automata representation used in LydiaSyft+, which is not well suited for efficient SCC computation. In instances where the SCC solver fails to pro-

duce a result within the allotted time, the construction of the monolithic transition relation typically fails because the BDD grows too large. Notably, minimization has mixed W effects on the SCC algorithm: in some cases (e.g., the ∀i ∨∀ pattern) it improves performance, while in others (e.g., the V ∃ ∧ ∃ pattern) it degrades it. This likely reflects a tradei i off between the reduced state space, which can improve efficiency, and the loss of the partitioned symbolic structure of the automata caused by minimization, which can make subsequent V operations more expensive. TheV i ∃i ∧∃ pattern is equi-realizable with the LTLf formula 1≤i≤n (ai ∨ ei ), enabling a direct comparison with LTLf synthesis tools. In Figure 2b we plot the runtime of the LTLf synthesizer included in LydiaSyft+. We observe that both the EL-based approach and our novel algorithms require less time and solve more instances. We believe that the improved performance of our implementations in this benchmark stems from their compositional treatment of the automata. To validate this hypothesis, we conduct V additional experiments using our solvers on formulas ∃( 1≤i≤n F((ai ∨ ei ) ∧ X false)). This results in performance comparable to standard LTLf synthesis, suggesting that a compositional approach to LTLf synthesis (Bansal et al. 2020) could achieve similar results on these benchmarks. Overall, the results in Figure 2b are particularly significant, as they show that synthesis for the LTLf + obligation fragment, despite operating over infinite traces, achieves performance comparable to that of LTLf synthesis on finite traces. Finally, we construct a family of benchmark formulas with a more complex Boolean structure. We consider the

102

runtime (s)

101

100

10−1

10−2

10−3 2

4

6

8

10

12

14

16

pattern size SCC [m] SCC

SafeReach [m] SafeReach

Büchi [m] Büchi

co-Büchi [m] co-Büchi

EL

Figure 3: Runtime of solvers on the implication pattern

V implication pattern ψj = i≤j ((∃F ai ) ⊃ ∃(F ei )) which states that for every i ≤ j, whenever ai holds at some point along a trace, ei must also hold at some point (possibly even before ai ). The environment controls the variables ai , while the system controls the variables ei , making the overall specification realizable. Figure 3 shows the runtimes for this experiment. In this setting, the SCC algorithm benefits from minimization, which reduces the BDD representation by four bits for the larger instances and by two to three bits for pattern sizes up to 14. Nevertheless, its performance remains inferior to that of the EL algorithm, which itself is outperformed significantly by our Büchi-based approaches. For the Büchi algorithms, minimization appears to have only limited impact. Although the arena size reduces by roughly 99% on the larger instances, this results in a reduction of only about 12% in the BDD bit count, which likely explains the modest effect on overall runtime.

8

Discussion

We show that synthesis for obligation properties in LTLf + reduces to solving games over automata on infinite words with weak acceptance conditions (DWA). Leveraging the simplicity of DWA automata and games, we propose reactive synthesis algorithms with the same asymptotic complexity as LTLf synthesis. We implement and evaluate these algorithms on benchmark formulas, comparing them to each other, to a full LTLf + solver based on reduction to Emerson–Lei games, and, where applicable, to an LTLf synthesis tool. Results show performance comparable to LTLf synthesis, extending effective synthesis from finite traces to infinite-trace obligation properties. For future work, we plan to implement the SCC-based algorithm using an automaton representation akin to SPOT’s MTBDD-based approach (Duret-Lutz et al. 2025). We also conjecture that our efficient methods can be adapted to handle recurrence and persistence properties, but leave this for future investigation.

References Aminof, B.; De Giacomo, G.; Di Stasio, A.; Francon, H.; Rubin, S.; and Zhu, S. 2025a. LTLf synthesis under environment specifications for reachability and safety properties. Inf. Comput. 303:105255. Aminof, B.; De Giacomo, G.; Rubin, S.; and Vardi, M. Y.

2025b. LTLf+ and PPLTL+: Extending LTLf and PPLTL to infinite traces. In IJCAI. Amram, G.; Bansal, S.; Fried, D.; Tabajara, L. M.; Vardi, M. Y.; and Weiss, G. 2021. Adapting behaviors via reactive synthesis. In CAV. Bacchus, F., and Kabanza, F. 1998. Planning for temporally extended goals. Ann. Math. Artif. Intell. 22(1-2):5–27. Bacchus, F., and Kabanza, F. 2000. Using temporal logics to express search control knowledge for planning. Artif. Intell. 116(1-2):123–191. Baier, J. A., and McIlraith, S. A. 2006. Planning with firstorder temporally extended goals using heuristic search. In AAAI. Baier, J. A.; Fritz, C.; and McIlraith, S. A. 2007. Exploiting procedural domain control knowledge in state-of-the-art planners. In ICAPS. Bansal, S.; Li, Y.; Tabajara, L. M.; and Vardi, M. Y. 2020. Hybrid compositional reasoning for reactive synthesis from finite-horizon specifications. In AAAI. Calvanese, D.; De Giacomo, G.; and Vardi, M. Y. 2002. Reasoning about actions and planning in LTL action theories. In KR. Camacho, A.; Bienvenu, M.; and McIlraith, S. A. 2019. Towards a unified view of AI planning and reactive synthesis. In ICAPS. Chang, E. Y.; Manna, Z.; and Pnueli, A. 1992. Characterization of temporal property classes. In ICALP. Cimatti, A.; Pistore, M.; Roveri, M.; and Traverso, P. 2003. Weak, strong, and strong cyclic planning via symbolic model checking. Artif. Intell. 1–2(147). De Giacomo, G., and Rubin, S. 2018. Automata-theoretic foundations of fond planning for LTLf /LDLf goals. In IJCAI. De Giacomo, G., and Vardi, M. Y. 1999. Automata-theoretic approach to planning for temporally extended goals. In ECP. De Giacomo, G., and Vardi, M. Y. 2013. Linear temporal logic and linear dynamic logic on finite traces. In IJCAI. De Giacomo, G., and Vardi, M. Y. 2015. Synthesis for LTL and LDL on finite traces. In IJCAI. De Giacomo, G.; Di Stasio, A.; Fuggitti, F.; and Rubin, S. 2020. Pure-past linear temporal and dynamic logic on finite traces. In IJCAI. Duret-Lutz, A.; Zhu, S.; Piterman, N.; Giacomo, G. D.; and Vardi, M. Y. 2025. Engineering an LTLf synthesis tool. In CIAA. Dwyer, M. B.; Avrunin, G. S.; and Corbett, J. C. 1998. Property specification patterns for finite-state verification. In FMSP. Ehlers, R.; Lafortune, S.; Tripakis, S.; and Vardi, M. Y. 2017. Supervisory control and reactive synthesis: a comparative introduction. Discret. Event Dyn. Syst. 27(2):209–260. Finkbeiner, B. 2016. Synthesis of reactive systems. Dependable Softw. Syst. Eng. 45:72–98.

Gerevini, A.; Haslum, P.; Long, D.; Saetti, A.; and Dimopoulos, Y. 2009. Deterministic planning in the fifth international planning competition: PDDL3 and experimental evaluation of the planners. Artif. Intell. 173(5-6):619–668. Hausmann, D.; Zhu, S.; Parretti, G.; Weinhuber, C.; Giacomo, G. D.; and Piterman, N. 2025. Emerson-Lei and Manna-Pnueli games for LTLf+ and PPLTL+ synthesis. In KR. Hausmann, D.; Lehaut, M.; and Piterman, N. 2024. Symbolic solution of Emerson-Lei games for reactive synthesis. In FoSSaCS. Hofmann, M., and Lange, M. 2025. Alternating Büchi Automata. Berlin, Heidelberg: Springer Berlin Heidelberg. 209–239. Kamp, J. A. W. 1968. Tense Logic and the Theory of Linear Order. Los Angeles, CA, USA: University of California. Klarlund, N.; Møller, A.; and Schwartzbach, M. I. 2002. MONA implementation secrets. Int. J. Found. Comput. Sci. 13(4):571–586. Larsen, C. A.; Schmidt, S. M.; Steensgaard, J.; Jakobsen, A. B.; van de Pol, J.; and Pavlogiannis, A. 2023. A truly symbolic linear-time algorithm for SCC decomposition. In TACAS. Lichtenstein, O.; Pnueli, A.; and Zuck, L. D. 1985. The glory of the past. In Logic of Programs, 196–218. Löding, C. 2001. Efficient minimization of deterministic weak omega-automata. Inf. Process. Lett. 79(3):105–109. Manna, Z., and Pnueli, A. 1990. A hierarchy of temporal properties. In PODC. Manna, Z., and Pnueli, A. 1992. The temporal logic of reactive and concurrent systems - specification. Springer. Manna, Z., and Pnueli, A. 1995. Temporal verification of reactive systems - safety. Springer. Manna, Z., and Pnueli, A. 2010. Temporal verification of reactive systems: Response. In Essays in Memory of Amir Pnueli. Piterman, N., and Pnueli, A. 2018. Temporal logic and fair discrete systems. In Handbook of Model Checking. Springer. 27–73. Piterman, N.; Pnueli, A.; and Sa’ar, Y. 2006. Synthesis of reactive(1) designs. In VMCAI. Pnueli, A., and Rosner, R. 1989. On the synthesis of a reactive module. In POPL. Pnueli, A. 1977. The temporal logic of programs. In FOCS. Somenzi, F., and Bloem, R. 2000. Efficient Büchi automata for LTL formulae. In CAV.

Supplement to “Preliminaries” Syntax and Semantics of LTL. Linear-time Temporal Logic (LTL) (Pnueli 1977) allows to express temporal properties of infinite traces. The set of LTL formulas over the set AP of atomic propositions is given by the following grammar. φ, ψ ::= p | ¬φ | φ ∧ ψ | Xφ | φUψ

(p ∈ AP )

We make use of common abbreviations such as φ ∨ ψ = ¬(¬φ ∧ ¬ψ), true = p ∨ ¬p, false = ¬true, Fφ = trueUφ (“eventually”) and Gφ = ¬F¬φ (“always”). LTL formulas are evaluated over infinite traces τ ∈ (2AP )ω of sets of atomic propositions. Satisfaction of LTL formulas by infinite traces is defined inductively as follows, referring to the ith element in τ by τi . τ, i |= p τ, i |= ¬φ τ, i |= φ ∧ ψ τ, i |= Xφ τ, i |= φUψ

iff p ∈ τi iff τ, i ̸|= φ iff τ, i |= φ and τ, i |= ψ iff τ, i + 1 |= φ iff ∃j ≥ i. τ, j |= ψ and ∀i ≤ j ′ < j.τ, j ′ |= φ.

Given an LTL formula φ, we let [φ] = {τ ∈ (2AP )ω | τ, 0 |= φ} denote the set of infinite traces that satisfy φ at the start. Syntax and Semantics of LTLf . The syntax of LTL on finite traces (LTLf ) (De Giacomo and Vardi 2013) is the same as the syntax of LTL given above. However, LTLf formulas are evaluated over finite traces τ ∈ (2AP )∗ rather than over infinite ones. A common abbreviation is the operator Xφ = ¬X[!]¬φ (“weak next”), expressing that if there is a next position in the trace, then it satisfies φ. The satisfaction of LTLf formulas by finite traces is defined inductively as follows, where |τ | denotes the length of a finite trace τ . τ, i |= p τ, i |= ¬φ τ, i |= φ ∧ ψ τ, i |= X[!]φ τ, i |= φUψ

iff p ∈ τi iff τ, i ̸|= φ iff τ, i |= φ and τ, i |= ψ iff i + 1 < |τ | and τ, i + 1 |= φ iff ∃i ≤ j < |τ |. τ, j |= ψ and ∀i ≤ j ′ < j.τ, j ′ |= φ.

The subtle (but consequential) difference to standard LTL semantics is the requirement that i + 1 < |τ | (resp. j < |τ |) in the last two clauses; that is, for all φ, X[!]φ is not satisfied at the end of a finite trace, and in order for φUψ to be satisfied in a finite trace, ψ is required to be satisfied before the trace ends. The formula last = ¬X[!] true is satisfied exactly at the last position of a finite trace. Given an LTLf formula φ, we let [φ] = {τ ∈ (2AP )∗ | τ, 0 |= φ} denote the set of finite traces that satisfy φ at the start.

Syntax and Semantics of PPLTL. Pure past LTL (PPLTL) (De Giacomo et al. 2020) allows to express temporal properties of finite traces by means of statements that refer to the past. The set of PPLTL formulas over the set AP of atomic propositions is given by the following grammar. φ, ψ ::= p | ¬φ | φ ∧ ψ | Y[!]φ | φSψ

(p ∈ AP )

Here, Y[!] (“yesterday”) and S (“since”) are the past operators; they are past analogues of the temporal operators X[!] and U. Common abbreviations include Oφ = true S φ (“at least once in the past”) and Hφ = ¬O¬φ (“historically”). The satisfaction of PPLTL formulas by finite traces is defined inductively as follows. τ, i |= p τ, i |= ¬φ τ, i |= φ ∧ ψ τ, i |= Y[!]φ τ, i |= φ S ψ

iff p ∈ τi iff τ, i ̸|= φ iff τ, i |= φ and τ, i |= ψ iff i > 0 and τ, i − 1 |= φ iff ∃i ≥ j ≥ 0. τ, j |= ψ and ∀i ≥ j ′ > j.τ, j ′ |= φ.

We observe that for all φ, Y[!]φ is not satisfied at the start of a finite trace, and in order for φ S ψ to be satisfied at position i in a finite trace, ψ has to be satisfied somewhere in the first i + 1 positions of the trace. The formula first = Y false (where Y = ¬Y[!]¬ denotes “weak yesterday”) is satisfied exactly at the first position of a finite trace. Given a PPLTL formula φ, we let [φ] = {τ ∈ (2AP )∗ | τ, |τ | − 1 |= φ} denote the set of finite traces that satisfy φ at the end, that is, at position |τ | − 1.

Supplement to “Specification of Obligation Properties” Proof of Lemma 2, restated for convenience. Lemma 2. Let Φ and Φ′ be LTLf formulas. Then ∀Φ ∧ ∀Φ′ ≡ ∀(Φ ∧ Φ′ )

∃Φ ∨ ∃Φ′ ≡ ∃(Φ ∨ Φ′ )

Moreover, Φ is equi-realizable with the LTLf + formula ∃Φ. Proof. We have [∀Φ ∧ ∀Φ′ ] = [∀Φ] ∩ [∀Φ′ ] = ∀[Φ] ∩ ∀[Φ′ ] = ∀([Φ] ∩ [Φ′ ]) = ∀[Φ ∧ Φ′ ] = [∀(Φ ∧ Φ′ )], where the third equality holds since, given an infinite trace τ and sets T, T ′ of finite traces, all prefixes of τ are contained in T and all prefixes of τ are contained in T ′ iff all prefixes of τ are contained in T and in T ′ . The proof of ∃Φ ∨ ∃Φ′ ≡ ∃(Φ ∨ Φ′ ) is analogous. To see that the LTLf formula Φ and the LTLf + formula ∃Φ are equi-realizable, let π be a finite trace that satisfies Φ. Then for any infinite extension τ of π, we have that π is a prefix of τ so that τ satisfies ∃Φ. For the converse direction, let τ be an infinite trace that satisfies ∃Φ. Then there is a prefix π of τ that is contained in [Φ]. Hence π satisfies Φ.

Supplement to “From Obligations to DWA” Full proof of Lemma 3, restated for convenience. Lemma 3. The set of languages recognizable by DWA is closed under union, intersection, and complement. Proof. Let A1 = (T1 , F1 ) and A2 = (T2 , F2 ) be weak automata with transition systems T1 = (Σ, Q1 , I1 , δ1 ) and T2 = (Σ, Q2 , I2 , δ2 ). We claim that: – A(1∧2) = (T1 ⊗T2 , F1 ×F2 ) is s.t. L(A(1∧2) ) = L(A1 )∩ L(A2 ); – A(1∨2) = (T1 ⊗T2 , F1 ×Q2 ∪Q1 ×F2 ) is s.t. L(A(1∨2) ) = L(A1 ) ∪ L(A2 ); – A(¬1) = (T1 , Q1 \ F1 ) is s.t. L(A(¬1) ) = Σω \ L(A1 ). – A(1∧2) , A(1∨2) , and A(¬1) are weak automata. Let w ∈ Σω be a word and let π1 = q1 q2 . . ., π2 = q1′ q2′ . . . and π1 × π2 = (q1 , q1′ )(q2 , q2′ ) . . . be the runs of T1 , T2 and T1 ⊗ T2 on w, respectively. The first claim follows since Inf(π1 × π2 ) ∩ F1 × F2 ̸= ∅ if and only if Inf(π1 )∩F1 ̸= ∅ and Inf(π2 )∩F2 ̸= ∅. For the second claim, we point out that Inf(π1 × π2 ) ∩ (F1 × Q2 ∪ Q1 × F2 ) ̸= ∅ if and only if Inf(π1 ) ∩ F1 ̸= ∅ or Inf(π2 ) ∩ F2 ̸= ∅. For the third claim, we have Inf(π1 )∩(Q1 \F1 ) ̸= ∅ if and only if Inf(π1 ) ∩ F1 = ∅ by weakness of A1 , that is, since every strongly connected component is either fully accepting or fully rejecting so that either Inf(π1 ) ⊆ F1 or Inf(π1 ) ⊆ Q1 \ F1 . It remains to show that (T1 ⊗T2 , F1 ×F2 ), (T1 ⊗T2 , F1 × Q2 ∪ Q1 × F2 ) and (T1 , Q1 \ F1 ) are weak automata. This is obvious for (T1 , Q1 \ F1 ). For the other two cases, we make the following observation about strongly connected components in the product transition system T1 ⊗ T2 . Let (q1 , q2 ) and (q1′ , q2′ ) be two states that belong to the same strongly connected component in T1 ⊗ T2 , that is, let there be a loop through (q1′ , q2′ ) and (q1 , q2 ). Then it follows from the definition of T1 ⊗ T2 that there is a loop through q1 and q1′ in T1 and a loop through q2 and q2′ in T2 . In other words, q1 and q1′ belong to the same strongly connected component in T1 , and q2 and q2′ belong the same strongly connected component in T2 . By weakness of T1 and T2 , we then have q1 ∈ F1 iff q1′ ∈ F1 and q2 ∈ F2 iff q2′ ∈ F2 . To see that (T1 ⊗ T2 , F1 × F2 ) is a weak automaton, consider two states (q1 , q2 ) and (q1′ , q2′ ) that belong to the same strongly connected component in T1 ⊗ T2 . From the above argumentation, we have (q1 , q2 ) ∈ F1 × F2 iff q1 ∈ F1 and q2 ∈ F2 iff q1′ ∈ F1 and q2′ ∈ F2 iff (q1′ , q2′ ) ∈ F1 × F2 , as required. To see that (T1 ⊗T2 , F1 ×Q2 ∪Q1 ×F2 ) is a weak automaton, consider two states (q1 , q2 ) and (q1′ , q2′ ) that belong to the same strongly connected component in T1 ⊗ T2 . Again, we have (q1 , q2 ) ∈ F1 ×Q2 ∪Q1 ×F2 iff q1 ∈ F1 or q2 ∈ F2 iff q1′ ∈ F1 or q2′ ∈ F2 iff (q1′ , q2′ ) ∈ F1 × Q2 ∪ Q1 × F2 , as required.

Full proof of Lemma 5, restated for convenience. Lemma 5. Let Φ be an LTLf formula and Q ∈ {∃, ∀}. Then there exists a DWA AQΦ equivalent to QΦ such that – if Q = ∃, then AQΦ = (TΦ+ , FΦ ); – if Q = ∀, then AQΦ = (TΦ− , FΦ ). Proof. – Q = ∃: Let τ ∈ (2AP )ω be an infinite trace. Then we have τ ∈ [∃Φ] iff there is some finite prefix of τ that is contained in [Φ]. This in turn is (by equivalence of Φ and AΦ ) the case iff there is some finite prefix of τ that is contained in L(AΦ ), which is the case iff the run of AQΦ = (TΦ , F ) on τ eventually visits a state from F iff τ ∈ L(AQΦ ). The last equivalence holds since all accepting states in TΦ+ are sinks so that a run of TΦ+ on an infinite word eventually visits F iff it eventually stays in F forever. – Q = ∀: Let τ ∈ (2AP )ω be an infinite trace. Then we have τ ∈ [∀Φ] iff all finite prefixes of τ are contained in [Φ]. This in turn is (by equivalence of Φ and AΦ ) the case iff all finite prefixes of τ are contained in L(AΦ ), which is the case iff the run of AQΦ = (TΦ , F ) on τ does not visit a state that is not contained in F iff τ ∈ L(AQΦ ). The last equivalence holds since all rejecting states in TΦ− are sinks so that a run of TΦ− on an infinite word does not visit a state that is not contained in F iff it eventually stays in F forever. To see that (TΦ+ , F ) is a weak automaton, observe that any strongly connected component in TΦ+ either consists of a single accepting (sink) state or exclusively of rejecting states; this is the case since in TΦ+ it is not possible to reach a rejecting state from an accepting state. The argument showing the weakness of (TΦ− , F ) is dual.

Supplement to “Synthesis via DWA” Proof of Theorem 2, restated for convenience. Theorem 2. The synthesis problem for the obligation fragment of LTLf + can be decided symbolically via DWA games in 2E XP T IME. Proof. By Lemmas 3 and 5, the DWA AΨ is equivalent to Ψ. Thus the system player wins the game induced by AΨ if and only if there is a (synthesis) strategy σ such that every outcome of σ satisfies Ψ. By Lemma 8, winning regions and strategies in the induced game can be computed in symbolic O(|Ψ|) time O(|QΨ |), where |QΨ | ∈ 22 . Symbolic algorithms for Büchi and co-Büchi games. For completeness, we include pseudo-code for the solution algorithms for Büchi games (Algorithm 3) and co-Büchi games (Algorithm 4). The algorithms compute nested least and greatest fixpoints. Full proof of Lemma 8, restated for convenience. Lemma 8. Algorithm 2 solves weak games with n nodes in symbolic time O(n) and yields memoryless winning strategies for the system player.

Algorithm 3: S OLVE B ÜCHI(V, F ) X = F ; X′ = V ′ 2 while X ̸= X do ′ 3 X=X 4 target = F ∩ Cpres (X) 5 Y = V ;Y ′ = ∅ 6 while Y ̸= Y ′ do 7 Y =Y′ 8 Y ′ = target ∪ Cpres (Y ) 9 X′ = Y 10 return X; 1

Algorithm 4: S OLVE C O -B ÜCHI(V, F ) X = V ; X′ = ∅ ′ 2 while X ̸= X do ′ 3 X=X 4 target = Cpres (X) 5 Y = ∅; Y ′ = V 6 while Y ̸= Y ′ do 7 Y =Y′ 8 Y ′ = target ∪ (F ∩ Cpres (Y )) 9 X′ = Y 10 return X; 1

Proof. For one direction of the proof, we use the data computed by the algorithm to construct a memoryless system player strategy that wins all game nodes from the computed set W . For each SCC S, the algorithm computes a memoryless strategy σS for the system player. Let v ∈ W and let S = SCC(v) denote the SCC of v. If S is rejecting, then σS ensures that every play starting at v eventually leaves S to a node w ∈ W that belongs to a lower SCC. If S is accepting, then σS ensures that every play starting at v either stays within S forever, or eventually leaves S to a node w ∈ W that belongs to a lower SCC. We define the memoryless strategy σ for the overall game to always play according to the strategy for the current SCC. Formally, put σ(v) = σSCC(v) (v) for each game node v ∈ Vs . It follows that σ wins every node in W . For the converse direction, let v be a game node that is won by the environment player and let σ be an environment strategy such that every play starting at v and following σ eventually stays forever within a rejecting SCC in A. We show that v ∈ / W . The proof proceeds by induction on the number l of different SCCs that are reachable from v. If l = 1, then there is no way to leave SCC(v), and SCC(v) is rejecting by assumption. Hence the algorithm treats SCC(v) in the first iteration of the loop (lines 2–10), using lines 8–9. We have v ∈ / Reach(SCC(v), ∅) so that v ∈ / W , as required. If l > 1, then we distinguish cases. If SCC(v) is accepting, then the environment has, by assumption, a strategy that ensures that every play starting at v eventually leaves SCC(v) by reaching a node w belonging to a lower SCC. Every such node w is won by the envi-

ronment and, by the inductive hypothesis, not contained in W . The algorithm treats the accepting SCC(v) using lines 6-7. We have v ∈ / Safe(SCC(v), W ) so that v ∈ / W , as required. If SCC(v) is rejecting, then the environment has a strategy that ensures that every play starting at v either stays in SCC(v) forever or eventually leaves the SCC(v) to a node w belonging to a lower SCC. Every such node w is won by the environment and, by the inductive hypothesis, not contained in W . Again, the algorithm treats SCC(v) using lines 8-9 and we have v ∈ / Reach(SCC(v), W ) so that v∈ / W , as required. Regarding time complexity, graphs with n vertices can be decomposed into their SCCs in symbolic time O(n) (Larsen et al. 2023). For each strongly connected component SCC, Algorithm 2 computes exactly one of the sets Reach(SCC, W ) or Safe(SCC, W ), each of which can be obtained in symbolic time O(|SCC|). Since the sizes of all SCCs sum to n, the overall runtime is linear. A memoryless strategy is constructed by always following the memoryless safety or reachability strategy for the current SCC.