Paper deep dive
Symbolic Synthesis for LTLf+ Obligations
Giuseppe De Giacomo, Christian Hagemeier, Daniel Hausmann, Nir Piterman
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 96%
Last extracted: 6/21/2026, 11:40:46 AM
Summary
The paper presents a method for the symbolic synthesis of LTLf+ obligation properties, which are extensions of LTLf to infinite traces. The authors demonstrate that obligation properties (positive Boolean combinations of safety and guarantee properties) can be efficiently translated into symbolically represented Deterministic Weak Automata (DWA). These DWAs inherit the algorithmic advantages of Deterministic Finite Automata (DFA), such as Boolean closure and polynomial-time minimization. The research shows that synthesis for this fragment is highly efficient, solvable in linear time once the DWA is constructed, and provides a novel symbolic algorithm for solving the resulting weak games. Experimental results using the LydiaSyft+ implementation show performance comparable to LTLf synthesis.
Entities (7)
Relation Signals (4)
LTLF → extends → LTLF
confidence 100% · LTLf+, the extension of LTLf to infinite traces.
LTLf+ obligation properties → translatesto → Deterministic Weak Automata
confidence 100% · they admit a translation into symbolically represented deterministic weak automata (DWA)
LydiaSyft+ → usedforevaluationof → LTLf+ synthesis algorithms
confidence 100% · experimental evaluation of these algorithms, based on LydiaSyft+
DWA → inheritsfeaturesfrom → DFA
confidence 90% · DWA inherit many of the attractive algorithmic features of DFA
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:We study synthesis for obligation properties expressed in LTLfp, 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 LTLfp 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 LTLfp obligation properties can be performed with virtually the same effectiveness as LTLf synthesis.
Tags
Links
- Source: https://arxiv.org/abs/2604.18532v1
- Canonical: https://arxiv.org/abs/2604.18532v1
Trouble viewing inline? Open PDF directly →
Full Text
77,398 characters extracted from source content.
Expand or collapse full text
Symbolic Synthesis for LTLf+ Obligations Giuseppe De Giacomo1 Christian Hagemeier1 Daniel Hausmann2 Nir Piterman3 1University of Oxford, UK 2University of Liverpool, UK 3University of Gothenburg and Chalmers University of Technology, Sweden @liverpool.ac.uk, christian.hagemeier,giuseppe.degiacomo@cs.ox.ac.uk, piterman@chalmers.se 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) (?) and its finite-trace variants are commonly used in computer science and artificial intelligence, e.g., in planning for temporally extended goals and declarative control knowledge (?; ?; ?; ?; ?; ?; ?). 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 (?; ?; ?). It is closely related to strong planning for temporally extended goals in fully observable nondeterministic domains (?; ?; ?; ?; ?; ?; ?; ?). Significant advances in reactive synthesis have been achieved using the GR(1) fragment of LTL (?), and by restricting attention to finite traces using LTLf (?). 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+ (?). 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 so-called Manna-Pnueli (or safety-progress) hierarchy of temporal formulas. This hierarchy was originally introduced in (?) and subsequently developed in detail by Manna and Pnueli in (?) and (?; ?; ?); see also the survey (?). 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. (?), 25 are obligation properties. Similarly, Somenzi & Bloem’s compilation of 25 LTL formulas “found in the literature” (?) contains 13 obligation properties. Moreover, even in the LTLf setting, assumptions about the environments are often forms of obligations (?). For obligation properties, we can work with deterministic weak automata (DWA) (?). 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 (?), 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 2ExpTime synthesis algorithms for LTLf+ obligation formulas. 4. A proof-of-concept implementation and experimental evaluation of these algorithms, based on + LydiaSyft+ (?), 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 (?). We use the standard syntax φ,ψ::=p∣¬φ∣φ∧ψ∣φ∣φψ, ,ψ::=p ψ X\, \, U\,ψ, (p∈APp∈ AP) where APAP is a countable set of atomic propositions. Common abbreviations include φ∨ψ=¬(¬φ∧¬ψ) ψ= ( ψ), =p∨¬p true=p p, =p∧¬p false=p p, φ=φ F\, = true\, U\, (“eventually”) and φ=¬¬φ G = F (“always”). Formulas are evaluated over infinite traces τ∈(2AP)ωτ∈(2^AP)^ω. LTL is expressively equivalent to first-order logic over infinite traces (?). LTL on finite traces (LTLf) (?) uses the same syntax but is interpreted over finite traces τ∈(2AP)∗τ∈(2^AP)^*. 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⊧Φ[ ]=\τ∈(2^AP)^* τ,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 (?). Automata on finite traces. A transition system T=(Σ,Q,I,δ)T=( ,Q,I,δ) consists of a finite alphabet Σ , a finite set Q of states, a set I⊆QI Q of initial states, and a transition relation δ⊆Q×Σ×Qδ Q× × Q. For q∈Qq∈ Q and a∈Σa∈ , define δ(q,a)=q′∈Q∣(q,a,q′)∈δ(q,a)=\q ∈ Q (q,a,q )∈δ\. The system is deterministic if |I|=1|I|=1 and |δ(q,a)|=1|δ(q,a)|=1 for all q∈Qq∈ Q and a∈Σa∈ , and nondeterministic otherwise; in the deterministic case, we write δ(q,a)=q′δ(q,a)=q for the unique successor and denote the initial state by ι . A finite automaton =(T,F)A=(T,F) is a transition system together with a set F⊆QF 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∈Σ∗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()L(A) consisting of all finite words for which an accepting run exists. For each LTLf formula Φ , one can construct an equivalent NFA of size 2(|Φ|)2^O(| |) and an equivalent DFA of size 22(|Φ|)2^2^O(| |) represented symbolically (?). Infinite-duration games on finite graphs. A game arena is a finite directed graph A=(V,E⊆V×V)A=(V,E V× V) whose vertex set is partitioned into system nodes VsV_s and environment nodes VeV_e. For v∈Vv∈ V, define E(v)=v′∣(v,v′)∈EE(v)=\v (v,v )∈ E\ and assume E(v)≠∅E(v)≠ for all v. A play is a path in A. A memoryless strategy for the system player is a function σ:Vs→Vσ:V_s→ V that assigns to every system node v∈Vsv∈ V_s a successor σ(v)∈E(v)σ(v)∈ E(v). A play v1v2…v_1v_2… is compatible with a σ if whenever vi∈Vsv_i∈ V_s, we have vi+1=σ(vi)v_i+1=σ(v_i). 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⊆VF V: Büchi objectives require visiting F infinitely often, whereas co-Büchi objective require visiting V∖FV 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 APAP of atomic propositions is partitioned into system actions X and environment actions Y. A (synthesis) strategy is a function σ:(2Y)∗→2Xσ:(2^Y)^*→ 2^X. An outcome of σ is an infinite word (x1∪y1)(x2∪y2)…∈(2AP)ω(x_1∪ y_1)(x_2∪ y_2)…∈(2^AP)^ω such that xi+1=σ(y1y2…yi)x_i+1=σ(y_1y_2… y_i) for all i≥0i≥ 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=(2,Q,ι,δ)T=(2 AP,Q, ,δ) induces a game arena AT=(Q∪Q×2X∪Q×2X×2Y,E)A_T=(Q∪ Q× 2^X∪ Q× 2^X× 2^Y,E) in which the system owns nodes in Q and the environment owns all other nodes. Transitions are defined by E(q)=q×2XE(q)=\q\× 2^X, E(q,x)=(q,x)×2YE(q,x)=\(q,x)\× 2^Y, and E(q,x,y)=δ(q,x∪y)E(q,x,y)=\δ(q,x∪ y)\. Plays of the form q1(q1,x1)(q1,x1,y1)q2(q2,x2)(q2,x2,y2)…q_1(q_1,x_1)(q_1,x_1,y_1)q_2(q_2,x_2)(q_2,x_2,y_2)… induce runs q1q2…q_1q_2… of T on the word (x1∪y1)(x2∪y2)…(x_1∪ y_1)(x_2∪ y_2)…. 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 (?). 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+ (?), 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 APAP of propositions are generated by the grammar Ψ,Ψ′::=∀Φ∣∃Φ∣∀∃Φ∣∃∀Φ∣Ψ∨Ψ′∣Ψ∧Ψ′∣¬Ψ , ::=∀ ∃ ∀∃ ∃∀ where Φ is an LTLf formula over APAP. We refer to formulas of the form ℚΦQ as finite-trace components. Recall that [Φ]⊆(2AP)∗[ ] (2^AP)^* denotes the set of finite traces satisfying Φ . Given a set R⊆(2AP)∗R (2^AP)^* of finite traces, let ∃R∃ R (∀R∀ R) denote the set of infinite traces τ∈(2AP)ωτ∈(2^AP)^ω such that at least one prefix of τ (respectively, every prefix) belongs to T. Similarly, let ∀∃T∀∃ T (∃∀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)ω[ ] (2^AP)^ω defined inductively by [Ψ∨Ψ′]=[Ψ]∪[Ψ′][ ]=[ ]∪[ ], [Ψ∧Ψ′]=[Ψ]∩[Ψ′][ ]=[ ]∩[ ], [¬Ψ]=(2AP)ω∖[Ψ][ ]=(2^AP)^ω [ ], and [ℚΦ]=ℚ[Φ][Q ]=Q[ ] where ℚ∈∃,∀,∀∃,∃∀Q∈\∃,∀,∀∃,∃∀\. Theorem 1. (?) 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 Φd _d and Φg1 _g_1,…,Φgk _g_k. The obligation formula ∀Φd→(⋀i≤k∃Φgi)∀ _d→( _i≤ k∃ _g_i) states that every infinite trace that remains within the domain eventually satisfies each goal. Goals can be made conditional using ∀Φd→(⋀i≤k(∃Φti→∃Φgi))∀ _d→( _i≤ k(∃ _t_i→∃ _g_i)) where Φti _t_i specifies a triggering property for the iith 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 ∀∃((a∧))∀∃( 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+, (?) 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 (?). 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 Emerson-Lei automata (DELA), whose objectives are Boolean combinations of Büchi and co-Büchi conditions (?; ?). 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 (?); solving DELA games is known to be PSpace-complete. 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 ℚΦA_Q 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 finite-trace components. Weak Büchi automata. We consider standard automata on infinite traces. A Büchi automaton =(T,F)A=(T,F) is a transition system T=(Σ,Q,ι,δ)T=( ,Q, ,δ) together with a set F of accepting states. A run of T on an infinite word w=a1a2…∈Σωw=a_1a_2…∈ ^ω is an infinite sequence π=q1q2…∈Qωπ=q_1q_2…∈ Q^ω of states such that q1=ιq_1= and qi+1∈δ(qi,ai)q_i+1∈δ(q_i,a_i) for all i≥1i≥ 1. The automaton recognizes the (ω-regular) language L()L(A) of all words w∈Σω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,ι,δ)T=( ,Q, ,δ) is a maximal set S⊆QS 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 (|Q|+|δ|)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)(T,F) is weak if every SCC S is either entirely accepting (S⊆FS F) or entirely rejecting (S∩F=∅S∩ F= ) (?).111This definition is different from, though equivalent to, the one in Section 9.1.5 of (?). 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)T_1=( ,Q_1, _1, _1) and T2=(Σ,Q2,ι2,δ2)T_2=( ,Q_2, _2, _2), their product is the transition system T1⊗T2=(Σ,Q1×Q2,(ι1,ι2),δ⊗)T_1 T_2=( ,Q_1× Q_2,( _1, _2), _ ) where δ⊗((q1,q2),a)=(δ1(q1,a),δ2(q2,a)) _ ((q_1,q_2),a)=( _1(q_1,a), _2(q_2,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 F1×F2F_1× F_2 (intersection) and (Q1×F2)∪(F1×Q2)(Q_1× F_2)∪(F_1× Q_2) (union). All constructions preserve weakness. ∎ DWA minimization. For every DWA A, there exists a unique minimal equivalent DWA that can be computed in time (nlogn)O(n n), where n is the number of states (?). 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 (S) rank(S) for SCCs S inductively. Bottom accepting and rejecting SCCs have rank 0 and 11, respectively. For a non-bottom SCC S, let l(S)l(S) be the maximum rank among its successors in the SCC decomposition. If S is transient, set (S)=l(S) rank(S)=l(S). If S is recurrent, set (S)=l(S)+1 rank(S)=l(S)+1 when parity disagrees with acceptance, and (S)=l(S) 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 =(T,F)A=(T,F) with state set Q, define F′=q∈Q∣(q) is evenF =\q∈ Q rank(q) is even\ and put ′=(T,F′)A =(T,F ); this does not change the marking of recurrent states. Applying Hopcroft minimization to ′A yields minA_ . Lemma 4. (?) minA_ is the minimal DWA equivalent to A. Corollary 1. Deterministic weak automata with n states can be minimized in time (nlogn)O(n 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 APAP, let Φ=(TΦ,F)A_ =(T_ ,F) with TΦ=(2AP,Q,ι,δ)T_ =(2^AP,Q, ,δ) denote an equivalent DFA of size 22(|φ|)2^2^O(| |), represented symbolically. Assume ι∉F ∉ F when ℚ=∃Q=∃ and ι∈F ∈ F when ℚ=∀Q=∀. Let TΦ+=(2AP,Q,ι,δ+)T^+_ =(2^AP,Q, ,δ^+) and TΦ−=(2AP,Q,ι,δ−)T^-_ =(2^AP,Q, ,δ^-) be obtained from TΦT_ by turning accepting (respectively, rejecting) states into absorbing sinks: define δ+(q,a)=qδ^+(q,a)=q if q∈Fq∈ F and δ+(q,a)=δ(q,a)δ^+(q,a)=δ(q,a) otherwise, and δ−(q,a)=qδ^-(q,a)=q if q∉Fq∉ F and δ−(q,a)=δ(q,a)δ^-(q,a)=δ(q,a) otherwise. Lemma 5. Let Φ be an LTLf formula and ℚ∈∃,∀Q∈\∃,∀\. Then there exists a DWA ℚΦA_Q equivalent to ℚΦQ such that – if ℚ=∃Q=∃, then ℚΦ=(TΦ+,FΦ)A_Q =(T^+_ ,F_ ); – if ℚ=∀Q=∀, then ℚΦ=(TΦ−,FΦ)A_Q =(T^-_ ,F_ ). Proof. (Sketch) Let Φ=(TΦ,FΦ)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Φ+T^+_ yields a DWA that accepts exactly those runs that eventually remain in FΦF_ . If ℚ=∀Q=∀, a trace satisfies ∀Φ∀ iff every prefix is accepted; making rejecting states absorbing in TΦ−T^-_ ensures that leaving F is permanent, so acceptance coincides with staying in FΦ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 translated into an equivalent DWA of size 22(|Ψ|)2^2^O(| |). 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σ \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ΨQ_ denote the state set of the composed DWA. Then every state in QΨQ_ is of the shape (q1,…,qk)(q_1,…,q_k) where qiq_i is a state in ℚiΦiA_Q_i _i. Put Qσ=(q1,…,qk)∈Q∣qi∈FΦi iff i∈σQ_σ=\(q_1,…,q_k)∈ Q q_i∈ F_ _i iff i∈σ\. Then the sets QσQ_σ for σ⊆1,…,kσ \1,…,k\ form a partition of QΨQ_ . Since all states in a single such set agree on acceptance of the individual component automata, we have that each QσQ_σ is either fully accepting (Qσ⊆FΨQ_σ F_ ) or fully rejecting (Qσ∩FΨ=∅Q_σ∩ F_ = ), depending on whether σ corresponds to a satisfying valuation of the Boolean formula structure of Ψ . Furthermore, for all i such that ℚi=∃Q_i=∃ and i∈σi∈σ, or ℚi=∀Q_i=∀ and i∉σi∉σ, all states in QσQ_σ have the same state as iith component – it is the sink state of the automaton ℚiΦiA_Q_i _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σ \1,…,k\ such that S⊆QσS Q_σ. Also, for all σ,σ′⊆1,…,kσ,σ \1,…,k\ such that σ≠σ′σ≠σ , QσQ_σ may be reachable from Qσ′Q_σ or vice versa, but not both. Hence, reachability partially orders the sets QσQ_σ, arranging them in a DAG structure. This does not provide a full SCC decomposition of ΨA_ since a single set Qσ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 (?). Formally, a DWA (or weak) game is a Büchi game G=(A,F)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 ℚiΦiQ_i _i, where ℚi∈∃,∀Q_i∈\∃,∀\ and each Φi _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 ℚiΦiQ_i _i into an equivalent DWA ℚiΦiA_Q_i _i according to Lemma 5: Transform Φi _i into the DFA (TΦi,FΦi)(T_ _i,F_ _i), where TΦi=(2AP,QΦi,ιΦi,δΦi)T_ _i=(2^AP,Q_ _i, _ _i, _ _i). If ℚi=∀Q_i=∀, put ℚiΦi=(TΦi−,FΦi)A_Q_i _i=(T^-_ _i,F_ _i); if ℚi=∃Q_i=∃, put ℚiΦi=(TΦi+,FΦi)A_Q_i _i=(T^+_ _i,F_ _i). Step 2. Compose the automata ℚiΦiA_Q_i _i according to the Boolean structure of Ψ (repeatedly using Lemma 3): Construct the DWA Ψ=(TΨ,FΨ)A_ =(T_ ,F_ ) inductively as follows. TΨi∧Ψj T_ _i _j =TΨi∨Ψj=TΦi⊗TΦj =T_ _i _j=T_ _i T_ _j FΨi∧Ψj F_ _i _j =FΨi×FΨj =F_ _i× F_ _j FΨi∨Ψj F_ _i _j =FΨi×QΦj∪QΦi×FΨ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)( _1,…, _k) of TΨT_ , extract a witnessing strategy. Theorem 2. The synthesis problem for the obligation fragment of LTLf+ can be decided symbolically via DWA games in 2ExpTime. More precisely, consider an input formula Ψ of size n. The constructed DWA game over ΨA_ has size at most n′=22n =2^2^n. 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 (n′)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)A=(V,E): ◇W W =v∈V∣E(v)∩W≠∅, =\v∈ V E(v)∩ W≠ \, □W W =v∈V∣E(v)⊆W, =\v∈ V E(v) W\, s(W) CPre_s(W) =(Vs∩◇W)∪(Ve∩□W), =(V_s∩ W)∪(V_e∩ W), e(W) CPre_e(W) =(Vs∩□W)∪(Ve∩◇W), =(V_s∩ W)∪(V_e∩ W), for W⊆VW 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 s CPre_s and e CPre_e 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∩W2W_1∩ W_2, W1∪W2W_1∪ W_2, or ¬W1 W_1 for symbolic sets W1,W2W_1,W_2 (encoded, e.g., by BDDs). We measure time complexity by the number of symbolic operations. Under this measure, computing s(W) CPre_s(W) or e(W) CPre_e(W) requires symbolic time (1)O(1). Let f:2V→2Vf:2^V→ 2^V be a monotone function. Its extremal (least and greatest) fixpoints are defined as μX.f(X) μ X.\,f(X) =Z⊆V∣f(Z)⊆Z=f|V|(∅) =\Z V f(Z) Z\=f^|V|( ) νX.f(X) ν X.\,f(X) =Z⊆V∣Z⊆f(Z)=f|V|(V) =\Z V Z f(Z)\=f^|V|(V) where fi+1(Z)=f(fi(Z))f^i+1(Z)=f(f^i(Z)) for i≥0i≥ 0 and f0(Z)=Zf^0(Z)=Z. Hence, a single extremal fixpoint over V can be computed in symbolic time (|V|)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) (W,T) =μX.T∪(W∩s(X)), =μ X.T∪(W∩ CPre_s(X)), Safe(W,T) (W,T) =νX.T∪(W∩s(X)), =ν X.T∪(W∩ CPre_s(X)), Büchi(T) \"uchi(T) =νX.μY.(T∩s(X))∪s(Y), =ν X.μ Y.(T∩ CPre_s(X))∪ CPre_s(Y), co-Büchi(T) -B\"uchi(T) =μX.νY.(F∩s(Y))∪s(X). =μ X.ν Y.(F∩ CPre_s(Y))∪ CPre_s(X). Here, Reach(W,T)Reach(W,T) computes the system player’s winning region in a game over W∪TW∪ T with the objective to eventually reach T, while Safe(W,T)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 (|W|)O(|W|). Lemma 6. Let A be an arena and F a set of game nodes. Then Büchi(F)B\"uchi(F) is the winning region of the system player in the Büchi game G=(A,F)G=(A,F), while co-Büchi(F)co -B\"uchi(F) is the winning region of the system player in the co-Büchi game G=(A,F)G=(A,F). Corollary 3. Büchi games and co-Büchi games with n nodes can be solved in symbolic time (n2)O(n^2). 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 WiW_i, starting from W0=∅W_0= . In iteration i, it solves: – a game over F∪W2iF∪ W_2i with the objective to either stay in F forever or eventually reach W2iW_2i, and – a reachability game over V with target set W2i+1W_2i+1. The corresponding fixpoints are W2i+1 W_2i+1 =Safe(F,W2i) =Safe(F,W_2i) (line 3) W2i+2 W_2i+2 =Reach(V,W2i+1) =Reach(V,W_2i+1) (line 4) Thus, SolveSafeReach(V,F) SolveSafeReach(V,F) computes the set of nodes from which the system player has a strategy to eventually stay within an accepting SCC forever. 1i=0i=0; W0=∅W_0= ; W−2=VW_-2=V 2 while W2i≠W2(i−1)W_2i≠ W_2(i-1) do 3 W2i+1=Safe(F,W2i)W_2i+1= Safe(F,W_2i) 4 W2i+2=Reach(V,W2i+1)W_2i+2= Reach(V,W_2i+1) 5 i=i+1i=i+1 6 7return W; Algorithm 1 SolveSafeReach( SolveSafeReach(V,F)) We observe that W2i⊆W2i+1⊆W2(i+1)W_2i W_2i+1 W_2(i+1) for all i. Consequently, the fixpoint computations in later iterations operate on larger target sets (W2iW_2i and W2i+1W_2i+1, respectively) and therefore terminate more quickly. Lemma 7. Algorithm 1 solves weak games with n nodes, k accepting nodes and l SCCs in symbolic time (n+kl)∈(n2)O(n+kl) (n^2), 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)Reach(V,W_j) 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)Safe(F,W_j) are needed; each such computation can be implemented in symbolic time (k)O(k), where k=|F|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 WjW_j, where j is the smallest index such that v∈Wjv∈ W_j. ∎ 1W=∅W= 2 while SCCs≠∅SCCs≠ do 3 B=bottomSCCs(SCCs)B= bottomSCCs(SCCs) 4 SCCs=SCCs∖BSCCs=SCCs B 5 for SCC∈BSCC∈ B do 6 if SCC⊆FSCC F then 7 X=Safe(X= Safe(SCC, W)) 8 9 else // SCC∩F=∅SCC∩ F= 10 X=Reach(X= Reach(SCC, W)) 11 W=W∪XW=W∪ X 12 13 return W Algorithm 2 SolveWeakSCC(V,F,SCCsSCCs) 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 (?). 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 bottomSCCs 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. Lemma 8. Algorithm 2 solves weak games with n nodes in symbolic time (n)O(n) and yields memoryless winning strategies for the system player. 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 (n)O(n) (?). For each strongly connected component SCCSCC, Algorithm 2 computes exactly one of the sets Reach(SCC,WSCC,W) or Safe(SCC,WSCC,W), each of which can be obtained in symbolic time (|SCC|)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+ (?). We first describe the implementation of the game arena construction and then detail the implementation of the game-solving 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 (?), 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 (?), 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τ=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. 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′)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 (?). 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 (?). 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. Figure 1: Runtime of solvers on the counter pattern ψ (a) ⋀i∃i∧∀ _i _i ∀ (b) ⋀i∃i∧∃ _i _i ∃ (c) ⋁i∀i∨∀ _i _i ∀ (d) ⋁i∀i∨∃ _i _i ∃ Figure 2: Runtime of solvers for conjunction and disjunction patterns 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”, “co-Bü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 Emerson-Lei 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−1b_0,…,b_n-1 with the overall system objective to reach the maximal counter value, expressed as a guarantee property. The original LTLf+ formulation (?) 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 _alw), resulting in the following realizable specification in which the system controls the variable addadd: ψ ψ =∀(φinit∧φinc∧φalw∧φtrans)⊃∃φgoal =∀( _init _inc _alw _trans)⊃∃ _goal φinit _init =¬c0∧⋯∧¬cn−1∧¬b0∧⋯∧¬bn−1 = c_0 … c_n-1 b_0 … b_n-1 φinc _inc =(add⊃((c0)∧((c0))∧(((c0))))) = G(add⊃( X(c_0) X( X(c_0)) X( X( X(c_0))))) φalw _alw =(add∧) = G F(add X\, false) φtrans _trans =((¬ci∧¬bi)→(¬bi∧¬ci+1))∧((¬ci∧bi)→(bi∧¬ci+1))∧((ci∧¬bi)→(bi∧¬ci+1))∧((ci∧bi)→(¬bi∧ci+1)) = G \ aligned (( c_i b_i)&→ X( b_i c_i+1)) \\ (( c_i b_i)&→ X(b_i c_i+1)) \\ ((c_i b_i)&→ X(b_i c_i+1)) \\ ((c_i b_i)&→ X( b_i c_i+1)) aligned . φgoal _goal =(b0∧⋯∧bn−1∧) = F (b_0 … b_n-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=((ei∨ai)∧) _i= F((e_i a_i) X\, false) with different boolean operators and trace quantifiers. The environment controls variables eie_i and the system controls variables aia_i. 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. ⋀i∃i∧∀ _i _i ∀ :∃φ1∧⋯∧∃φn−1∧∀φn : ∃ _1 … ∃ _n-1 ∀ _n ⋀i∃i∧∃ _i _i ∃ :∃φ1∧⋯∧∃φn : ∃ _1 … ∃ _n ⋁i∀i∨∀ _i _i ∀ :∀φ1∨⋯∨∀φn : ∀ _1 … ∀ _n ⋁i∀i∨∃ _i _i ∃ :∀φ1∨⋯∨∀φn−1∨∃φn : ∀ _1 … ∀ _n-1 ∃ _n The ∃ pattern introduced in (?) corresponds to the ⋀i∃i∧∃ _i _i ∃ pattern. We refer to the number of conjuncts or disjuncts as the pattern size. 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 reduce the number of states. The only exception is the ⋀i∃i∧∀ _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 produce 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 effects on the SCC algorithm: in some cases (e.g., the ⋁∀i∨∀ _i ∀ pattern) it improves performance, while in others (e.g., the ⋀i∃i∧∃ _i _i ∃ pattern) it degrades it. This likely reflects a trade-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 operations more expensive. The ⋀i∃i∧∃ _i _i ∃ pattern is equi-realizable with the LTLf formula ⋀1≤i≤n(ai∨ei) _1≤ i≤ n(a_i e_i), enabling a direct comparison with LTLf synthesis tools. In Figure 2(b) 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 additional experiments using our solvers on formulas ∃(⋀1≤i≤n((∨)∧))∃( _1≤ i≤ n F((a_i e_i) X~ false)). This results in performance comparable to standard LTLf synthesis, suggesting that a compositional approach to LTLf synthesis (?) could achieve similar results on these benchmarks. Overall, the results in Figure 2(b) 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 implication pattern ψj=⋀i≤j((∃ai)⊃∃(ei)) _j= _i≤ j((∃ F\,a_i)⊃∃( F\,e_i)) which states that for every i≤ji≤ j, whenever aia_i holds at some point along a trace, eie_i must also hold at some point (possibly even before aia_i). The environment controls the variables aia_i, while the system controls the variables eie_i, 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. Figure 3: Runtime of solvers on the implication pattern 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 (?). We also conjecture that our efficient methods can be adapted to handle recurrence and persistence properties, but leave this for future investigation. References Supplement to “Preliminaries” Syntax and Semantics of LTL. Linear-time Temporal Logic (LTL) (?) allows to express temporal properties of infinite traces. The set of LTL formulas over the set APAP of atomic propositions is given by the following grammar. φ,ψ::=p∣¬φ∣φ∧ψ∣φ∣φψ ,ψ::=p ψ X Uψ (p∈APp∈ AP) We make use of common abbreviations such as φ∨ψ=¬(¬φ∧¬ψ) ψ= ( ψ), =p∨¬p true=p p, =¬ false= true, φ=φ F = true U (“eventually”) and φ=¬¬φ G = F (“always”). LTL formulas are evaluated over infinite traces τ∈(2AP)ωτ∈(2^AP)^ω of sets of atomic propositions. Satisfaction of LTL formulas by infinite traces is defined inductively as follows, referring to the iith element in τ by τi _i. τ,i τ,i ⊧p p iff p∈τi p∈ _i τ,i τ,i ⊧¬φ iff τ,i⊧̸φ τ,i τ,i τ,i ⊧φ∧ψ ψ iff τ,i⊧φ and τ,i⊧ψ τ,i and τ,i ψ τ,i τ,i ⊧φ X iff τ,i+1⊧φ τ,i+1 τ,i τ,i ⊧φψ Uψ iff ∃j≥i.τ,j⊧ψ and ∃ j≥ i.\,τ,j ψ and ∀i≤j′<j.τ,j′⊧φ. ∀ i≤ j <j.τ,j . Given an LTL formula φ , we let [φ]=τ∈(2AP)ω∣τ,0⊧φ[ ]=\τ∈(2^AP)^ω τ,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) (?) is the same as the syntax of LTL given above. However, LTLf formulas are evaluated over finite traces τ∈(2AP)∗τ∈(2^AP)^* 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 τ,i ⊧p p iff p∈τi p∈ _i τ,i τ,i ⊧¬φ iff τ,i⊧̸φ τ,i τ,i τ,i ⊧φ∧ψ ψ iff τ,i⊧φ and τ,i⊧ψ τ,i and τ,i ψ τ,i τ,i ⊧[!]φ X[!] iff i+1<|τ| and τ,i+1⊧φ i+1<|τ| and τ,i+1 τ,i τ,i ⊧φψ Uψ iff ∃i≤j<|τ|.τ,j⊧ψ and ∃ i≤ j<|τ|.\,τ,j ψ and ∀i≤j′<j.τ,j′⊧φ. ∀ i≤ j <j.τ,j . The subtle (but consequential) difference to standard LTL semantics is the requirement that i+1<|τ|i+1<|τ| (resp. j<|τ|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⊧φ[ ]=\τ∈(2^AP)^* τ,0 \ denote the set of finite traces that satisfy φ at the start. Syntax and Semantics of PPLTL. Pure past LTL (PPLTL) (?) 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 APAP of atomic propositions is given by the following grammar. φ,ψ::=p∣¬φ∣φ∧ψ∣[!]φ∣φψ ,ψ::=p ψ Y[!] Sψ (p∈APp∈ 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 τ,i ⊧p p iff p∈τi p∈ _i τ,i τ,i ⊧¬φ iff τ,i⊧̸φ τ,i τ,i τ,i ⊧φ∧ψ ψ iff τ,i⊧φ and τ,i⊧ψ τ,i and τ,i ψ τ,i τ,i ⊧[!]φ Y[!] iff i>0 and τ,i−1⊧φ i>0 and τ,i-1 τ,i τ,i ⊧φψ \, S\,ψ iff ∃i≥j≥0.τ,j⊧ψ and ∃ i≥ j≥ 0.\,τ,j ψ and ∀i≥j′>j.τ,j′⊧φ. ∀ 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+1i+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⊧φ[ ]=\τ∈(2^AP)^* τ,|τ|-1 \ denote the set of finite traces that satisfy φ at the end, that is, at position |τ|−1|τ|-1. Supplement to “Specification of Obligation Properties” Proof of Lemma 2, restated for convenience. See 2 Proof. We have [∀Φ∧∀Φ′] [∀ ∀ ] =[∀Φ]∩[∀Φ′]=∀[Φ]∩∀[Φ′] =[∀ ]∩[∀ ]=∀[ ]∩∀[ ] =∀([Φ]∩[Φ′])=∀[Φ∧Φ′]=[∀(Φ∧Φ′)], =∀([ ]∩[ ])=∀[ ]=[∀( )], where the third equality holds since, given an infinite trace τ and sets T,T′T,T of finite traces, all prefixes of τ are contained in T and all prefixes of τ are contained in T′T iff all prefixes of τ are contained in T and in T′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. See 3 Proof. Let 1=(T1,F1)A_1=(T_1,F_1) and 2=(T2,F2)A_2=(T_2,F_2) be weak automata with transition systems T1=(Σ,Q1,I1,δ1)T_1=( ,Q_1,I_1, _1) and T2=(Σ,Q2,I2,δ2)T_2=( ,Q_2,I_2, _2). We claim that: – (1∧2)=(T1⊗T2,F1×F2)A_(1 2)=(T_1 T_2,F_1× F_2) is s.t. L((1∧2))=L(1)∩L(2)L(A_(1 2))=L(A_1)∩ L(A_2); – (1∨2)=(T1⊗T2,F1×Q2∪Q1×F2)A_(1 2)=(T_1 T_2,F_1× Q_2∪ Q_1× F_2) is s.t. L((1∨2))=L(1)∪L(2)L(A_(1 2))=L(A_1)∪ L(A_2); – (¬1)=(T1,Q1∖F1)A_( 1)=(T_1,Q_1 F_1) is s.t. L((¬1))=Σω∖L(1)L(A_( 1))= ^ω L(A_1). – (1∧2)A_(1 2), (1∨2)A_(1 2), and (¬1)A_( 1) are weak automata. Let w∈Σωw∈ ^ω be a word and let π1=q1q2… _1=q_1q_2…, π2=q1′q2′… _2=q _1q _2… and π1×π2=(q1,q1′)(q2,q2′)… _1× _2=(q_1,q _1)(q_2,q _2)… be the runs of T1T_1, T2T_2 and T1⊗T2T_1 T_2 on w, respectively. The first claim follows since (π1×π2)∩F1×F2≠∅ Inf( _1× _2)∩ F_1× F_2≠ if and only if (π1)∩F1≠∅ Inf( _1)∩ F_1≠ and (π2)∩F2≠∅ Inf( _2)∩ F_2≠ . For the second claim, we point out that (π1×π2)∩(F1×Q2∪Q1×F2)≠∅ Inf( _1× _2)∩(F_1× Q_2∪ Q_1× F_2)≠ if and only if (π1)∩F1≠∅ Inf( _1)∩ F_1≠ or (π2)∩F2≠∅ Inf( _2)∩ F_2≠ . For the third claim, we have (π1)∩(Q1∖F1)≠∅ Inf( _1)∩(Q_1 F_1)≠ if and only if (π1)∩F1=∅ Inf( _1)∩ F_1= by weakness of 1A_1, that is, since every strongly connected component is either fully accepting or fully rejecting so that either (π1)⊆F1 Inf( _1) F_1 or (π1)⊆Q1∖F1 Inf( _1) Q_1 F_1. It remains to show that (T1⊗T2,F1×F2)(T_1 T_2,F_1× F_2), (T1⊗T2,F1×Q2∪Q1×F2)(T_1 T_2,F_1× Q_2∪ Q_1× F_2) and (T1,Q1∖F1)(T_1,Q_1 F_1) are weak automata. This is obvious for (T1,Q1∖F1)(T_1,Q_1 F_1). For the other two cases, we make the following observation about strongly connected components in the product transition system T1⊗T2T_1 T_2. Let (q1,q2)(q_1,q_2) and (q1′,q2′)(q _1,q _2) be two states that belong to the same strongly connected component in T1⊗T2T_1 T_2, that is, let there be a loop through (q1′,q2′)(q _1,q _2) and (q1,q2)(q_1,q_2). Then it follows from the definition of T1⊗T2T_1 T_2 that there is a loop through q1q_1 and q1′q _1 in T1T_1 and a loop through q2q_2 and q2′q _2 in T2T_2. In other words, q1q_1 and q1′q _1 belong to the same strongly connected component in T1T_1, and q2q_2 and q2′q _2 belong the same strongly connected component in T2T_2. By weakness of T1T_1 and T2T_2, we then have q1∈F1q_1∈ F_1 iff q1′∈F1q _1∈ F_1 and q2∈F2q_2∈ F_2 iff q2′∈F2q _2∈ F_2. To see that (T1⊗T2,F1×F2)(T_1 T_2,F_1× F_2) is a weak automaton, consider two states (q1,q2)(q_1,q_2) and (q1′,q2′)(q _1,q _2) that belong to the same strongly connected component in T1⊗T2T_1 T_2. From the above argumentation, we have (q1,q2)∈F1×F2(q_1,q_2)∈ F_1× F_2 iff q1∈F1q_1∈ F_1 and q2∈F2q_2∈ F_2 iff q1′∈F1q _1∈ F_1 and q2′∈F2q _2∈ F_2 iff (q1′,q2′)∈F1×F2(q _1,q _2)∈ F_1× F_2, as required. To see that (T1⊗T2,F1×Q2∪Q1×F2)(T_1 T_2,F_1× Q_2∪ Q_1× F_2) is a weak automaton, consider two states (q1,q2)(q_1,q_2) and (q1′,q2′)(q _1,q _2) that belong to the same strongly connected component in T1⊗T2T_1 T_2. Again, we have (q1,q2)∈F1×Q2∪Q1×F2(q_1,q_2)∈ F_1× Q_2∪ Q_1× F_2 iff q1∈F1q_1∈ F_1 or q2∈F2q_2∈ F_2 iff q1′∈F1q _1∈ F_1 or q2′∈F2q _2∈ F_2 iff (q1′,q2′)∈F1×Q2∪Q1×F2(q _1,q _2)∈ F_1× Q_2∪ Q_1× F_2, as required. ∎ Full proof of Lemma 5, restated for convenience. See 5 Proof. – ℚ=∃Q=∃: Let τ∈(2AP)ωτ∈(2^AP)^ω 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(Φ)L(A_ ), which is the case iff the run of ℚΦ=(TΦ,F)A_Q =(T_ ,F) on τ eventually visits a state from F iff τ∈L(ℚΦ)τ∈ L(A_Q ). The last equivalence holds since all accepting states in TΦ+T^+_ are sinks so that a run of TΦ+T^+_ on an infinite word eventually visits F iff it eventually stays in F forever. – ℚ=∀Q=∀: Let τ∈(2AP)ωτ∈(2^AP)^ω 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(Φ)L(A_ ), which is the case iff the run of ℚΦ=(TΦ,F)A_Q =(T_ ,F) on τ does not visit a state that is not contained in F iff τ∈L(ℚΦ)τ∈ L(A_Q ). The last equivalence holds since all rejecting states in TΦ−T^-_ are sinks so that a run of TΦ−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)(T^+_ ,F) is a weak automaton, observe that any strongly connected component in TΦ+T^+_ either consists of a single accepting (sink) state or exclusively of rejecting states; this is the case since in TΦ+T^+_ it is not possible to reach a rejecting state from an accepting state. The argument showing the weakness of (TΦ−,F)(T^-_ ,F) is dual. ∎ Supplement to “Synthesis via DWA” Proof of Theorem 2, restated for convenience. See 2 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 time (|QΨ|)O(|Q_ |), where |QΨ|∈22(|Ψ|)|Q_ |∈ 2^2^O(| |). ∎ 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. 1X=FX=F; X′=VX =V 2 while X≠X′X≠ X do 3 X=X′X=X 4 =F∩s(X) target=F∩ Cpre_s(X) 5 Y=VY=V; Y′=∅Y = 6 while Y≠Y′Y≠ Y do 7 Y=Y′Y=Y 8 Y′=∪s(Y)Y = target∪ Cpre_s(Y) 9 10 X′=YX =Y 11 return X; Algorithm 3 SolveBüchi(V,F) SolveB\"uchi(V,F) 1X=VX=V; X′=∅X = 2 while X≠X′X≠ X do 3 X=X′X=X 4 =s(X) target= Cpre_s(X) 5 Y=∅Y= ; Y′=VY =V 6 while Y≠Y′Y≠ Y do 7 Y=Y′Y=Y 8 Y′=∪(F∩s(Y))Y = target∪(F∩ Cpre_s(Y)) 9 10 X′=YX =Y 11 return X; Algorithm 4 SolveCo-Büchi(V,F) SolveCo-B\"uchi(V,F) Full proof of Lemma 8, restated for convenience. See 8 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 _S for the system player. Let v∈Wv∈ W and let S=SCC(v)S=SCC(v) denote the SCC of v. If S is rejecting, then σS _S ensures that every play starting at v eventually leaves S to a node w∈Ww∈ W that belongs to a lower SCC. If S is accepting, then σS _S ensures that every play starting at v either stays within S forever, or eventually leaves S to a node w∈Ww∈ 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)σ(v)= _SCC(v)(v) for each game node v∈Vsv∈ V_s. 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∉Wv∉ W. The proof proceeds by induction on the number l of different SCCs that are reachable from v. If l=1l=1, then there is no way to leave SCC(v)SCC(v), and SCC(v)SCC(v) is rejecting by assumption. Hence the algorithm treats SCC(v)SCC(v) in the first iteration of the loop (lines 2–10), using lines 8–9. We have v∉Reach(SCC(v),∅)v (SCC(v), ) so that v∉Wv∉ W, as required. If l>1l>1, then we distinguish cases. If SCC(v)SCC(v) is accepting, then the environment has, by assumption, a strategy that ensures that every play starting at v eventually leaves SCC(v)SCC(v) by reaching 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. The algorithm treats the accepting SCC(v)SCC(v) using lines 6-7. We have v∉Safe(SCC(v),W)v (SCC(v),W) so that v∉Wv∉ W, as required. If SCC(v)SCC(v) is rejecting, then the environment has a strategy that ensures that every play starting at v either stays in SCC(v)SCC(v) forever or eventually leaves the SCC(v)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)SCC(v) using lines 8-9 and we have v∉Reach(SCC(v),W)v (SCC(v),W) so that v∉Wv∉ W, as required. Regarding time complexity, graphs with n vertices can be decomposed into their SCCs in symbolic time (n)O(n) (?). For each strongly connected component SCCSCC, Algorithm 2 computes exactly one of the sets Reach(SCC,WSCC,W) or Safe(SCC,WSCC,W), each of which can be obtained in symbolic time (|SCC|)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. ∎