Practical "Paritizing" of Emerson-Lei Automata Florian Renkin^)©, Alexandre Duret-Lutz©, and Adrien PommelletC LRDE, EPITA, Le Kremlin-Bicetre, France {frenkin,adl,adrien}@lrde.epita.fr Abstract. We introduce a new algorithm that takes a Transition-based Emerson-Lei Automaton (TELA), that is, an ^-automaton whose acceptance condition is an arbitrary Boolean formula on sets of transitions to be seen infinitely or finitely often, and converts it into a Transition-based Parity Automaton (TPA). To reduce the size of the output TPA, the algorithm combines and optimizes two procedures based on a latest appearance record principle, and introduces a partial degeneralization. Our motivation is to use this algorithm to improve our LTL synthesis tool, where producing deterministic parity automata is an intermediate step. 1 Introduction Let us consider the transformation of o;-automata with arbitrary Emerson-Lei acceptance into o;-automata with parity acceptance. Our inputs are Transition-based Emerson-Lei Automata (TELA), i.e., automata whose edges are labeled with integer marks like ©, ©, and whose acceptance condition is a positive Boolean formula over terms such as Fin(O) or 'nf (©) that specifies which marks should be seen infinitely or finitely often in accepting runs. Our algorithm processes a TELA with any such acceptance condition, and outputs a TELA whose acceptance can be interpreted as a parity max odd (resp. even) condition, i.e., the largest mark seen infinitely often along a run has to be odd (resp. even). Figure 1 on page 9 and Fig. 3 on page 10 show an example of input and output. While non-deterministic Biichi automata are the simplest o;-automata able to represent all o;-regular languages, deterministic Biichi automata are less expressive; as a consequence, applications that require determinism usually switch to more complex acceptance conditions like Rabin, Streett, or parity. Parity can be regarded as the simplest of the three, in the sense that any parity automaton can be converted into a Rabin or a Streett automaton without changing its transition structure. Parity acceptance is especially popular among game solvers, as parity games can be solved with memoryless strategies and arise in many problems. Our motivation comes from one such problem: reactive synthesis from LTL specifications, i.e., building an I/O transducer whose input and output signals satisfy an LTL specification ip [4]. The high-level approach taken by our ltlsynt tool [20], or even by the SyntComp'19 winner Strix [18], is to transform the LTL © Springer Nature Switzerland AG 2020 D. V. Hung and O. Sokolsky (Eds.): ATVA 2020, LNCS 12302, pp. 127-143, 2020. https://doi.org/10.1007/978-3-030-59152-6_7 Check for updates 128 F. Renkin et al. formula into a deterministic transition-based parity automaton (DTPA), interpret the DTPA as a parity game by splitting the alphabet on inputs and outputs, then solve the game and use any winning strategy to synthesize a transducer. Let us zoom on the first step: transforming an LTL formula into a DTPA. One of the many methods to transform an LTL formula into a DTPA is to first convert the LTL formula into a non-deterministic Biichi automaton, and then determinize this automaton using some variant of Safra's construction to obtain a DTPA [22,23]. This is the current approach of ltlsynt [20]. However, since the introduction of the HOA format [2] allowing the representation of TELA, we have seen the development of several tools for converting LTL formulas into TELA: for instance delag [21], ltl2da and ltl2na (all three part of newer versions of Owl [13]), ltl3tela [19], or Spot's ltl2tgba -G (see Sect. 5), all trying to reduce the size of their output by using acceptance formulas more closely related to the input LTL formulas. An alternative way to transform an LTL formula into a DTPA is therefore to first transform the LTL formula into a deterministic TELA, and then "paritize" the result. This paper focuses on such a paritization procedure. Note that our construction preserves the deterministic nature of its input but also works on non-deterministic automata. Our procedure adapts for TELA, optimizes, and combines a few existing transformation procedures. For instance there exists a procedure called SAR (state appearance record) [16,17] that converts a state-based Muller automaton into a state-based parity automaton, and a similar but more specialized procedure called IAR (index appearance record) [16,17] for transforming a Rabin or Streett automaton into a parity automaton. These two procedures are based on a latest appearance record (LAR), i.e., a structure that keeps track of the latest occurring state or the latest occurring unsatisfied Rabin/Streett pair (the term LAR is sometimes used to describe SAR [10]). We describe the adaptation of these two procedures in Sect. 3. In the context of a TELA, we introduce a simplified SAR called CAR (color appearance record) that only tracks colors, and the IAR algorithm has already been adapted by Kfetinsky et al. [15]. A third transformation, also described in Sect. 3, can be used as a preprocessing before the previous procedures: this is a partial degeneralization, i.e. an extension of the classical degeneralization procedure [1,11] that will replace any sub-formula of the form /\i Inf(m^) (resp. \J{ Fin(raj)) by a single Inf(raj) (resp. Fin(raj)) in the acceptance condition. In Sect. 4 we present our "paritization" procedure that combines the above procedures with some additional optimizations. Essentially the automaton is processed one strongly-connected component (SCC) at a time, and for each SCC the acceptance condition is simplified before choosing the most appropriate transformation to parity. This paritization procedure is implemented in Spot 2.9. In Sect. 5 we show how the combination of all the improvements outperforms the straightforward CAR algorithm in practice. Practical "Paritizing" of Emerson-Lei Automata 129 2 Transition-Based Emerson-Lei Automata Emerson-Lei Automata were denned [8] and named [24] in the 80s, and provide a way to describe a Muller acceptance condition using a positive Boolean formula over sets of states that must be visited finitely or infinitely often. Below we define the transition-based version of those automata, as used in the Hanoi Omega-Automata Format [2]. Instead of working directly with sets of transitions, we label transitions by multiple colored marks, as can be seen in Figs. 1, 2 and 3. Let M = {0,..., n— 1} be a finite set of n contiguous integers called the set of marks or colors, from now on also written M = {©,©,...} in our examples. We define the set C(M) of acceptance formulas according to the following grammar, where m stands for any mark in M: a :: = T | _L | Inf (ra) | Fin(m) | (a A a) | (a V a) Acceptance formulas are interpreted over subsets of M. For N C M we define the satisfaction relation N |= a according to the following semantics: AT |= T N \= Inf (m) iff m e N N \= ax A a2 iff N |= ax and N |= a2 N ty= _L N \= Fin(m) iff m N N \= ax V a2 iff N |= ax or N |= a2 Intuitively, an Emerson-Lei automaton is an o;-automaton labeled by marks and whose acceptance condition is expressed as a positive Boolean formula on sets of marks that occur infinitely often or finitely often in a run. More formally: Definition 1 (Transition-based Emerson-Lei Automata). A transition-based Emerson-Lei automaton (TELA) is a tuple A = (Q,M,E,S,qo,a) where Q is a finite set of states, M is a finite set of marks, E is a finite input alphabet, 5 C Q x E x 2M x Q is a finite set of transitions, qo G Q is an initial state, and a £ C(M) is an acceptance formula. £ A Given a transition d = (qi,£, A, q2) £ 5, we write d = q± ——> q2. A run r of A l- A- is an infinite sequence of transitions r = [si l> s9i>o in 5U such that sq = qo and Vi > 0, = Si+i. Since Q is finite, for any run r, there exists a position £ ■ A ■ jr > 0 such that for each i > jr, the transition Si l> occurs infinitely often in r. Let Rep(r) = Ui>j ^ be the set of colors repeated infinitely often in r. A run r is accepting if Rep(r) |= a, and we then say that A accepts the word (£i)i>o ^ ^ ■ The language J??(A) is the set of words accepted by A. Two TELA are equivalent if they have the same language. By extension, the language of a state q G Q is the language of the automaton using q as initial state. Example 1. In the automaton of Fig. 1, the run r that repeats infinitely the two transitions —>(o)^g^rw{T) has Rep(r) = {©,©,0} • Since Rep(r) satisfies the acceptance condition (written below the automaton) r is an accepting run. A TELA's acceptance formula can be used to express many classical uj-automata acceptance conditions, as shown in Table 1. Note that colors may 130 F. Renkin et al. Table 1. Shape of classical acceptance formulas. The variables m,mo,mi,... stand for any acceptance marks in M = {0,1,. ..} to allow multiple occurrences. Buchi Inf (m) generalized Buchi co-Buchi Fin(m) generalized co-Buchi \/t Fin (mi) Rabin \Ji (Fin(m2i) A lnf(m2i+i)) Rabin-like Vi (Fin(m2i) A lnf(m2i+i)) V V,' 'nf(mj) V Vfc Fin(mfc) Streett /\i (lnf(m2i) V Fin(m2i+i)) Streett-like /\i (lnf(m2i) V Fin(m2i+i)) A A, 'nf(mj) A /\k Fin(mfc) parity max even lnf(2fc) V (Fin(2fc - 1) A (lnf(2fc - 2) V (Fin(2fc - 3) A .. .))) parity max odd Inf(2fc + 1) V (Fin(2fc) A (lnf(2fc - 1) V (Fin(2fc - 2) A .. .))) appear more than once in most formulas; for instance (Fin(O) A lnf(©)) V (Fin(O) A Inf (©)) is a Rabin acceptance formula. The only unusual formulas of Table 1 are the Rabin-like and Streett-like conditions. A Rabin-like formula Vi (Fin(ra2i) A Inf(m2i+i)) VVj Inf(m^) V Vfc Fin(mfc) can be converted into the Rabin formula \Ji{y\r\{m2i) Alnf(m2i+i)) V Vj(Fin(a) A Inf(mj)) V Vfc(Fin(mfc) A I nf (6)) by introducing two new marks a and b such that a occurs nowhere in the automaton and b occurs everywhere. Therefore, without loss of generality, we may describe algorithms over Rabin automata, but in practice we implement those over Rabin-like acceptance conditions. When discussing Rabin acceptance, it is common to mention the number of Rabin pairs, i.e., the number of disjuncts in the formula; we use the same vocabulary for Rabin-like, even if some of the pairs only have one term. Dually, the number of pairs in a Streett-like formula is the number of conjuncts. Remark 1. Formula Fin(0) A Inf(O) can be seen as Rabin with one pair, or a Streett-like with two pairs. Similarly, a generalized Buchi is also Streett-like. Remark 2. Any sub-formula of the form Vi 'nf(mi) (resp. f\{ Fin(raj)) can be replaced by a single lnf(a) (resp. Fin(a)) by introducing a mark a on all transitions where any rrii occurred. Thus, any parity automaton can be rewritten as Rabin-like or Streett-like without adding or removing any transition: to produce a Rabin-like (resp. Streett-like) acceptance, rewrite the parity acceptance formula in disjunctive normal form (resp. CNF) and then replace each term of the form /\i Fin(raj) (resp. Vi ^(mi)) by a single Fin (resp. Inf). Definition 2 (Strongly Connected Component). Let us consider a TELA A= (Q, M, E,S,qo,a). A strongly connected component (SCC) is a non-empty set of states S C Q such that any ordered pair of distinct states of S can be connected by a sequence of transitions of 5. We note A\s = (S,M,U,5',q'0,a) a sub-automaton induced by S, where 5' = 5 Pi (S x E x 2M x S), and q'0 G S is an arbitrary state of S. An SCC S is said accepting if ££{A\s) ^ 0- Practical "Paritizing" of Emerson-Lei Automata 131 3 Specialized Transformations We describe three algorithms that transform the acceptance condition of a TELA. The first two output an equivalent TELA with parity acceptance: CAR (Sect. 3.1) works for any input, while IAR (Sect. 3.2) is specialized for Rabin-like or Streett-like inputs. The third algorithm is a partial degeneralization (Sect. 3.3): it takes an automaton with any acceptance formula a, and produces an automaton where any generalized Biichi (resp. generalized co-Biichi) subformula of a have been replaced by a Biichi (resp. co-Biichi) formula. Optimizations common to these algorithms are listed in Sect. 3.4. 3.1 Color Appearance Record Consider a set of marks M = {0,1,..., n— 1} and a TELA A = (Q, M, U, 5, qo, a). Let II(M) be the set of permutations of M. We can represent a permutation a £ II(M) by a table (a(0), a(l),..., a(n - 1)). The Color Appearance Record (CAR) algorithm pairs such permutations of colors with states of the input automaton in order to keep track of the history of colors visited in the corresponding run of A, in the order they were last seen. Output states are therefore elements of QCAR = Q x LT(M). We update histories with a function U : II(M) x M —> 77\M) x 2M, such that U(a,c) = ((c,a(0),a(l),...,a(i-l),a(i + l),...,a(n-l)),{a(0),a(l),...,a(i)}) where i = a~x (c) is the position of color c in a. In other words, IA(a, c) moves c to the front of a by rotating the first i + 1 elements: it returns the new permutation and the set of rotated elements. This update function can be generalized to a set of colors recursively as follows: U(a, 0) = (a, 0) U(a, {c} U C) = (p, R U S) where (vr, 7?) = U(a, C) and (p, S) = U(ir, c) That is to say, U(a, C) moves the colors in C to the front of a and also returns set of colors corresponding to the updated prefix. The order in which colors in C are moved to the front of a is unspecified and may affect the size of the output automaton (see Sect. 3.4). Let M' = {0,..., 2n+l} be the output marks. We define the transition relation SCAR Q QCAR x e x 2M' x gCAR ag follows: eS, (tt,R) =U(a,C), c = 2\R\ + [R\£a] where [7? ^ a] is a shorthand for 0 if 7? |= a and for 1 if 7? ^ a. Theorem 1. For any TELA A = (Q, M, U, 5, qo, a) over the marks M = {0, ...,n- 1}, there exists an equivalent TELA A' = (QCAR, M', U, SCAR, (q0, 7To),c/) where a' is a parity max even formula over 2n + 1 colors. The initial permutation can be any ttq G LT(M). 132 F. Renkin et al. The proof is similar to that of the state appearance record algorithm [16], but we track colors instead of states. The intuition is that any cycle r' of A' corresponds to a cycle r of A. If the union of the colors visited by r is R, then all the states in r' necessarily have all colors of R to the front of their history, there will be at least one transition t of r' for which the number of colors rotated by IA is \R\, and for all the other transitions this number will be lesser or equal. Therefore, the color 2|i?| + [R \/= a] selected for this transition t will be the highest of Rep(r') and will cause r' to be accepting iff r is accepting. Note that this construction may produce |Q| x nl states in the worst case. Example 2. The CAR arrow at the top-right of Fig. 2 shows an application of CAR on a small example. Let us ignore the fact that there is no initial state in these "automata" and focus on how transitions of the output (above the arrow) are built from the transitions of the input (below). Assuming we want to build the successors of the output state (li, (0, 2,1)), we look for all successors of input state li. One option is (li)~©*"(0i)- We compute the history U((0, 2,1), {©}) of the destination state by moving © to the front of the current history, yielding (2,0,1). The destination state is therefore (0i, (2,0,1)). Two colors R = {©,©} have been moved in the history by this transition, and since R |= a the transitions is labeled by color 2 x \R \ +0 = 0. Another successor is the loop (Ti^G). In this case, color © , already at the front of the history, is moved onto itself, so the output is a loop. Since R = {©} a , that loop is labeled by 2 x \R\ + 1 = ©. 3.2 Index Appearance Record While CAR can be used to transform Rabin or Streett automata into parity automata, there exists an algorithm more suitable for these subclasses of TELA. Let A = (Q, M, E,5,qo,a) be a TELA with a Rabin acceptance condition a = Viei (Fin(pi) A Inf(r^)). We call (pi,ri) a Rabin pair, where pi is the prohibited color, and ri the required color. We define the set of index appearance records as the set n(T) of permutations of Rabin pair indices. The output states QlAR = Q x 11(1) are equipped with such a record to track the history of indices of the Rabin pairs (pi,ri) in the order the colors pi were last seen. We update those IAR using a function U. : IJ(X) xl^ n(T), such that U{a,i) = (i,a(0),a(l),...,a(j-l),a(j + l),...,a(|X|-l)) where j = a~1(i) is the position of the index % in a. In other words, U(a, i) moves % to the front of a by rotating the first j + 1 elements. This update function can be generalized to a set of indices recursively with U(a, 0) = a and U(a, {i} U I) = U(U(a, When processing a transition labeled by colors C C M, we need to update the history for all indices P(C) = {i G X | pi G C} of a prohibited color. This construction builds an automaton with parity max odd acceptance over the color M' = {0,1,..., \X\ +2} . The transitions 5IAR C QIAR x E x 2M' x QIAR of the output automaton can be defined as: Practical "Paritizing" of Emerson-Lei Automata 133 q q' e 5, 7T = U(a, P(C)), m = M(a,C), c = 2m + 1 + [m > 0 A Pa(m) € C] where M(a, C) = max({-±} U {i e {0,1, \I\ - 1} | pa^ e C V ra^ e C}) is the rightmost index of a corresponding to a pair with a color in C, or — ^ if no such index exists. Theorem 2 ([15]). For any TELA A = (Q, M, U, 5, qo, a) over the marks M = {0,..., n — 1} and such that a is a Rabin condition, there exists an equivalent TELA A; = (QIAR, M', E, 5IAR, (go, no), ot') where a' is a parity max odd acceptance formula over 2n + 2 colors. The initial permutation tiq can be chosen arbitrarily. A dual construction transforms Streett into parity max even. For proof, we refer the reader to Loding [16] (for state-based acceptance) and to Kfetinsky et al. [15] (who adapted it to TELA). For the intuition behind the definition of c in <5IAR, imagine a transition (q, a) ~-> (q'',7T) on a cycle r' of A', and a matching transition q ——> q' from A. Assume the corresponding cycle r of the input automaton visits all colors in C = Rep(r). Because they are on the cycle r', the IARs a, tt, and the others on that cycle have all their indices P(C) to the left of the permutation. When we scan the IAR a from the right to the left to find the maximal index m = A4(a, C) corresponding to a pair matching C, three situations can occur: (1) If m > 0 and pa(m) £ Cj we know that we are in the left part, and that all Rabin pairs of indices 0 and pa(m) ^ C? it may be the case that m is in the right part of the IAR, meaning that the Rabin pair of index a(m) is satisfied. We label the transition with c = 2m+ 1 to indicate acceptance, but this might be canceled by a another transition emitting a higher even value if pa(i) appears elsewhere on this cycle. (3) Finally m = — \ occurs when C = 0, in this case the transition is labeled by c = 0 as no pair is satisfied. This procedure generates an automaton with |Q| x \T\\ states in the worst case, but unless colors occur multiple times in a, we usually have \T\ < n/2, making IAR preferable to CAR. Example 3. The arrow IAR in Fig. 2 shows an example of IAR at work on a Rabin automaton with two pairs. The output transition (2(01 ))-Q»(2 (10)) , corresponds to a loop labeled by C = {©,©} in the input. Since © is prohibited in Rabin pair 1, index 1 has to move to the front of the history. Furthermore, the rightmost index of (01) with a color in C is also m = 1 and corresponds to Pi = © G C , this justifies that the output transition is labeled by 2m+l+l = ©• 3.3 Partial Degeneralization We now define the partial degeneralization of a TELA A according to some subset D of its colors. Our intent is to modify A in such a way that we can 134 F. Renkin et al. replace any sub-formula of the form /\deD Inf(rf) in its acceptance condition a by a single lnf(e) for some new color e. Similarly any sub-formula of the form V'deD Fin(cZ) will be replaced by Fin(e). We denote such a substitution of sub-formulas by Oi[/\deD Inf(cf) <— \nf(e)][\fdeD Fin(rf) <— Fin(e)]. The construction ensures that the runs of the output that see all colors of D infinitely often also see e infinitely often. To do that, we consider an ordering of {do,di,... d\o\-i} of D, and equip each state of the output automaton by a level in L = {0,1,... \D\ — 1}. We jump from level i to level i + 1 whenever we use a transition labeled by df, thus, we reach a level i only after having met the i first colors of D. We jump down to level 0 when a transition t leaving a state at level \D\ — 1 is labeled by d\n\_i\ moreover, since any cycle going through t will have seen all colors in D, we can add the new color e to t. An optimization, commonly done in degeneralization procedures [1,11], is that transition labeled by multiple consecutive colors of D may skip several levels. Let us define this skipping of levels more formally as a function S : L x 2M —>■ L x 2^eJ" that takes a level i and a set C of colors seen by some transition, and returns the new level j and a subset that is either 0 or {e} to indicate whether the new color should be added to the output transition. W,0) = {*\ , _ where \(j-\D\,{e}) ifj^l j = max(fc g {M+l, • • .,i+\D\}\{di, d(i+i) mod .. .,d(k+\D\-i) mod Q C). Theorem 3. Let A = (Q, M, E, 5, q0, a) be a TELA, and let C C M be a set of marks. Let D = {do, rfi, • • •, rf|c|-i} ^e some ordering of the colors of C, and let L = {0,1,..., \C\} be a set of levels. A is equivalent to its partial degeneralization according to C, defined by automaton A' = (Q', M', E, 5', (q0, i0), a') where Q' = Q x L, M' = M U {e} for some new colore ^ M, a' = a[f\deD\nf(d) <— Inf (e)] [\/deD Fin(rf) <— Fin(e)]7 and 5' = [(gi,i) (q2,j) | qi q2 g S, S(i, C Pi M) = (j, C \ M) j. The initial level can be any iq g L. First, note that this procedure does not remove any color from the automaton. This is because even though subformulas of the form /\deD Inf(rf) are removed from a, other parts of a, preserved in a', may still use colors in D. Of course, colors that do not appear in a' may be removed from the automaton as a subsequent step, and this is done in our implementation. Moreover, because the algorithm keeps all used colors, the construction is valid for any subset D C M, even one that does not correspond to a conjunction of Inf or disjunction of Fin in a. In such the construction enlarges the automaton without changing its acceptance condition. Finally, in the case where a is a generalized Biichi condition over the marks M, and D = M, then the resulting a' will be lnf(e), and removing all the now useless original colors will have the same effect as a classical degeneralization. In this sense, the degeneralization is a special case of the partial degeneralization. Practical "Paritizing" of Emerson-Lei Automata 135 Similarly, this procedure can also be seen as a generalization of the transformation of generalized-Rabin automata into Rabin automata [12]. Example 4- In Fig- 2, the arrow PD{13} denotes the application of a partial degeneralization according to the set M = {©, ©}. This allows to rewrite acceptance's sub-formula Fin(O) V Fin(©) as Fin(0) with a new color. Output states (q, i) are written as qi for brevity. The ordering of colors is do = ©, d\ = ©. SCC\ SCC2 SCC3 (lnf(0)AFin(O))V ((Inf(O)Vlnf(O)) A Fin(O) A (Fin(©)VFin(©))) Fig. 1. Some arbitrary input TELA, to be paritized. For readability, letters are not displayed. 3.4 Optimizations We now describe several optimizations for the aforementioned constructions. Jump to Bottom: The choice of the initial permutation ttq in the CAR, in the IAR, or of the initial level Iq in the partial degeneralization is arbitrary. With a bad selection of those values, a cycle can be turned into a lasso. For instance, if we consider the input automaton -applying CAR with ttq = (0,1) produces an automaton with the following structure: —»[x(01)]-»-(?/(01)]^[x(10)], whereas ttq = (1,0) would yield —»[x(10))^(?/(01)]. Instead of guessing the correct initialization, we simply use the fact that two states (q, a) and (q, tt) recognize the same language: after the algorithm's execution, we redirect any transition leading to a state (q, a) to the copy (q, tt) that lies in the bottommost SCC (in some topological ordering of the SCCs). The initial state is changed similarly. The input and output automata should have then the same number of SCCs. This optimization applies to CAR, IAR, partial degeneralization, or combinations of those. E.g., if partial degeneralization is used before CAR or IAR, leading to states of the form ((q,i),a), the search for an equivalent state in the bottom SCC needs only consider q, and can simplify both constructions at once. A similar simplification was initially proposed in the context of IAR for simplifying one SCC at a time [15]. Heuristics used in degeneralization algorithms to select initial level upon entering a new SCC [1] are then unnecessary. 136 F. Renkin et al. <201)V©->i0o (102)17© Ii (201)VcHli (021)13) parity max even ] CAR (lnf(0)AFin(O)) V ((lnf(0)Vlnf(O)) A Fin(O) A (Fin(O)VFin(O))) (lnf(©)AFin(0)) ((lnf( l)Vlnf(0))A Fin(O) A Fin(G)) V SCCi S+P IAR 2(01) 2(10) lnf(©)AFin(0)) V (Inf(O)Vlnf(O)) A Fin(O)) 3(01) parity max odd (lnf(©)AFin(0)) V (lnf( )AFin(©)) Rabin pair 0 Rabin pair 1 S+P Q-V renumber Q-s/ sees — xíb> — lnf(©)AFin(0) Fin(0)Alnf(0) (parity max even) Fig. 2. Intermediate steps of the construction, handling the SCCs in different ways. These steps are explained at various places through Sects. 3 and 4. CAR of SCd, adjusted for max odd IAR of SCC2 2(10)] SCC3, adjusted for max odd Fin((6))A(lnf(0)V(Fin(G)A(lnf(©)V(Fin(0)A(lnf(O)VFin(O)))))) (parity max odd) Fig. 3. Paritization of the automaton of Fig. 1, combining the transformed SCCs of Fig. 2 after adjustment to a common acceptance condition. Practical "Paritizing" of Emerson-Lei Automata 137 History Reuse: When processing an input transition labeled with multiple colors, the insertion order of those colors (resp. Rabin pair indices) in front of the history during an update of the CAR (resp. IAR) is arbitrary. Kfetinsky et al. [15] suggested to check previously built states for one with a compatible trail of the history, in order to avoid creating new states. While implementing this optimization, we noticed that sometimes we can find multiple compatible states: heuristically selecting the most recently created one (as opposed to the oldest one) produces fewer states on average in our benchmark. It seems to create tighter loops and larger "lasso prefixes" that can later be removed by the jump to bottom optimization. Such history reuse can also be done a posteriori once a candidate automaton has been built, to select better connections. Heuristic Selection of Move Order: When an input transition is labeled with multiple colors, but no compatible destination state already exists to apply the previous optimization, we select the order in which colors are moved to the front of the history using a heuristic. Colors that are common to all incoming transitions of the destination states are moved last, so they end up at the beginning of the history. For instance in the CAR construction of Fig. 2, this is how the order (102) is chosen as destination history for transition (0i^-©©©>(0c^: O is common to all edges going to Oo, so we want it at the front of the history. SCC-aware Algorithms: These algorithms benefit from considering the SCCs of the original automaton. For CAR and IAR, the histories attached can be restricted to the colors present in the SCC [15]. The partial degeneralization needs not modify SCCs that do not contain all the colors C to degeneralize. Heuristic Ordering of Colors to Degeneralize: Our implementation of the partial degeneralization tries to guess, for each SCC, an appropriate ordering of the color to degeneralize: this is done by maintaining the order as a list of equivalence classes of colors, and refining this order as new transitions are processed. For instance if we degeneralize for the colors C = {©, ©, ©, ©} , the initial order will be ({©, ©, @, ©}) , then if the first transition we visit has colors {©, ©} the new order will be refined to ({©,©}, {©,©}) and we jump to level 2 as we have now seen the first equivalence class of size 2. Propagation of Colors: To favor the grouping of colors in the dynamic ordering of the partial degeneralization, and in the history reuse optimization of IAR and CAR, we propagate colors as much as possible in SCCs. Ignoring transitions that are self-loops or that do not have both extremities in the same SCC, colors common to all incoming transitions of a state can be copied to all outgoing transitions and vice-versa. E.g., @i^_^@;^^(£)5© is seen as the equivalent (^)^S^(yy^. ' . ^(zj^. , showing that cycles with © always have ©. The next section goes one step further in SCC-awareness, by actually simplifying the acceptance condition for each SCC according to the colors present. The paritization strategy to apply (CAR, IAR, identity, ...) can then be chosen independently for each SCC. 138 F. Renkin et al. 4 Paritization with Multiple Strategies We now describe our paritization algorithm taking as input a TELA A: (1) Enumerate the SCCs Si of A. For each Si, perform the following operations: (a) Consider the sub-automaton A\s,r (b) Simplify its acceptance condition by removing unused colors (Fin(i) becomes T, and lnf(i) becomes _L for any color % unused in A\Si), or dually, colors that appear everywhere. Colors that always appear together can be replaced by a single color, and disjunctions of Inf or conjunctions of Fin can be reduced as discussed in Remark 2. (c) Propagate colors in the SCC (Sect. 3.4). (d) If the simplified acceptance condition contains conjunctions of Inf or disjunctions of Fin, apply the partial degeneralization construction (maybe multiple times) for all those terms, and remove unused colors. Since this incurs a blowup of the state-space that is linear (maybe multiple times) in the number of colors removed, it generally helps the CAR construction which has a worst case factorial blowup in the number of colors. Also, after this step, the acceptance condition might match more specialized algorithms in the next step. Jump to step lb as the acceptance changed. (e) Transform the automaton A\st into a parity max automaton Ri using the first applicable procedure from the following list: - If Jzf(*4.|,s.) is empty [3], strip all colors and set the acceptance condition to _L, which is a corner case for parity max even formula. (For parity max acceptances, transitions without color can be interpreted as having color —1.); - Do nothing if the acceptance is already a parity max formula; - If the acceptance has the shape Inf(mo) V (Fin(mi) A (Inf(m2) V ...)) of a parity max, renumber the colors mo, mi,... in decreasing order to get a parity max formula; - Adjust the condition to lnf(®) and the labeling of the transitions if this is a deterministic Rabin-like automaton that is Biichi-type (this requires a transition-based adaptation of an algorithm by Krishnan et al. [14]); note that lnf(©) is also a parity max even formula. - Dually, adjust the condition to Fin(©) if this is a deterministic Streett-like automaton that is co-Biichi-type, since Fin(O) is also a parity max odd formula. - If the automaton is Rabin-like or Streett-like, apply IAR to obtain a parity max automaton. When the acceptance formula can be interpreted as both Rabin-like or Streett-like we use the interpretation with the fewest number of pairs (cf. Remark 1). - Otherwise, apply CAR to obtain a parity max automaton. (2) Now that each automaton A\s,t nas been converted into an automaton Ri whose parity acceptance is either max odd or max even, adjust those acceptance conditions by incrementing or decrementing the colors of some Ri so that they can all use the same acceptance, and stitch all Ri together to form Practical "Paritizing" of Emerson-Lei Automata 139 the final automaton R. For any transition of A that goes from state q in SCC i to state q' in SCC j, R should have a transition for each copy of q in Ri and going to one copy of q' in Rj. Similarly, the initial state of R should be any copy of the initial state of A. (3) As a final cleanup, the number of colors of R can be reduced by computing the Rabin-index of the automaton [5]. Figures 1, 2 and 3 show this algorithm at work on a small example with three SCCs. Figure 3 shows the result of step 2. Executing step 3 would reduce the number of colors to 2 (or to 3 if uncolored transitions are disallowed). We now comment the details of Fig. 2. The notation S+P refers to the Simplification of the acceptance condition (step lb) and the Propagation of colors in the SCC (step lc). On SCCi, step lb replaces 0 by © , because these always occur together, and step lc adds © on the transition from 1 to 0. After partial degeneralization, the sub-formula Fin(©) A Fin(O) can be fused into a single Fin(©) (see Remark 2) by simply replacing © by © in the automaton, and after that the marks on the transitions before and after state Oo are propagated by step lc. The resulting automaton is neither Rabin-like nor Streett-like, so it is transformed to parity using CAR; however the history of the states only have 3 colors to track instead of the original 5. In SCC2, Fin(©) and lnf(©) can be replaced respectively by T and _L because © and © are not used. The acceptance condition is therefore reduced to the Rabin acceptance condition displayed, and IAR can be used instead of CAR. (Using CAR would build at least 4 states.) Finally .SCCVs acceptance conditions reduces to Inf (©) A Fin(©) . Renumbering the colors to Fin(O) A lnf(©) gives us a parity max odd acceptance. To stitch all these results together, as in Fig. 3, we adjust all automata to use parity max odd: in SCC\ this can be done for instance by decrementing all colors and in SCCs by incrementing them (handling any missing color as —1). Our implementation uses an additional optimization that we call the parity prefix detection. If the acceptance formula has the shape Inf(rao) V (Fin(rai) A (Inf(ra2) V (.../?))), i.e., it starts like a parity max formula but does not have the right shape because of j3, we can apply CAR or IAR using only (3 while preserving the color mo, mi, m,2,... of the parity prefix, and later renumber all colors so the formula becomes parity max. This limits the colors that CAR and IAR have to track, so it reduces the number of states in the worst case. 5 Experimental Evaluation The simple CAR described in Sect. 3.1, without the optimizations of Sect. 3.4 was implemented in Spot 2.8 [7] as a function to_parity(). It can be used by Spot's ltlsynt tool with option —algo=lar; in that case the LTL specification (p passed to ltlsynt is converted to a deterministic TELA Av with arbitrary acceptance and then transformed into a parity automaton with to_parity () before the rest of the LTL synthesis procedure is performed. The TELA Av built internally by ltlsynt can be obtained using Spot's ltl2tgba -G -D command: the construction is similar to the delag tool [21] and 140 F. Renkin et al. regards the original formula as a Boolean combination of LTL sub-formulas fi, translating each ipi to a deterministic TELA Aipi (by combining classical LTL-to-generalized-Biichi translation [6] with specialized constructions for subclasses of LTL [9], or a Safra-based procedure [23]), and combining those results using synchronized products to obtain a TELA whose acceptance condition is the Boolean combination of the acceptance conditions of all the Atpi. In Spot 2.9, to_parity() was changed to implement Sect. 4 and the optimizations of Sect. 3.4. We are therefore in position to compare the improvements brought by those changes on the transformation of Av to V^.1 We evaluate the improvements on two sets of automata: syntcomp contains automata generated with ltl2tgba -G -D from LTL formulas from the sequential TLSF track of SyntComp'2017. Among those automata, we have removed those that already had a parity acceptance (usually Biichi acceptance). The remaining set contains 32 automata with a generalized-Biichi condition, and 84 with a condition that mixes Fin and Inf terms (only 1 of these can be considered Rabin-like or Streett-like). The average number of accepting SCCs is 1.9 (min. 1, med. 1, max. 4). The average number of states is 46 (min. 1, med. 13, max. 986). randltl contains 273 automata built similarly, from random LTL formulas. Furthermore, we have ensured that no automaton has parity acceptance, and all of them use at least 5 colors (med. 5, avg. 5.2, max. 9). The average number of accepting SCCs is 1.7 (min. 1, med. 1, max. 5). The average number of states is 5.8 (min. 1, med. 4, max. 41). Only 13 of these automata have a Rabin-like or Streett-like acceptance condition. The improvement of our new paritization based on multiple strategies over our old unoptimized CAR implementation is shown on Fig. 4. Table 2 selectively disables some optimizations to evaluate their effect on the number of output states. Configuration "all — x" means that optimization x is disabled. Rabin to Biichi is the detection of Rabin-like (or Streett-like) automata that are Biichi (or co-Biichi) realizable at step le. Parity prefix is the optimization mentioned at the very end of Sect. 4. Simplify acc, propagate colors, and partial degen correspond respectively to steps lb and lc, and Id. Partial degeneralization appears to be the most important optimization, because in addition to reducing the number of colors, it may help to use IAR or even simpler construction. The propagation of colors, which allows more flexibility in the selection of histories, is the second best optimization. Hist, reuse corresponds to the history reuse described in Sect. 3.4. all — reuse latest has history reuse enabled, but uses the oldest compatible state instead of the latest—hence our heuristic of using the latest compatible state. Finally Unoptimized CAR is a straightforward implementation of CAR given for comparison. To assert the effect of the improved paritization on ltlsynt, we ran the entire SyntCompT7 benchmark (including formulas omitted before) with a timeout of 100 seconds, and counted the number of cases solved by different configurations 1 To reproduce these results, see https://www.lrde.epita.fr/~frenkin/atva20/. Practical "Paritizing" of Emerson-Lei Automata 141 03 ■si w ' o o in O d o randltl syntcomp ft 03 S-l o o I 100 10000 1000000 unoptimized CAR (states) Fig. 4. Comparison of the new multi-strategy paritization (Sect. 4) against the unoptimized CAR (Sect. 3.1) Table 2. Effect of disabling different optimizations on the arithmetic and geometric means of the number of states on both benchmarks configuration amean gmean all 48.71 14.43 all — Rabin to Buchi 48.72 14.45 all — parity prefix 48.97 14.54 all — simplify acc 49.32 15.07 all — hist, reuse 51.01 15.18 all — reuse latest 51.05 15.29 all — propagate colors 55.69 16.91 all — partial degen 2165.50 20.20 unoptimized CAR 5375.02 45.16 Table 3. Number of SyntComp47 cases solved by ltlsynt under different configurations, with a timeout of 100 s. PAR-2 (penalized average runtime) sums the time of all successful instances, plus twice the timeout for unsuccessful ones. option approach to paritization # solved PAR-2 —algo=lar.old LTL to determ. TELA, then CAR of Sect. 3.1 175 7262 s —algo=sd LTL to Büchi, then split input/output variables, then Safra-based determinization [20] 177 6879 s —algo=ds LTL to Büchi, then Safra-based determinization, then split input/output variables [20] 180 6671 s —algo=lar LTL to determ. TELA, then approach of Sect. 4 185 6296 s of ltlsynt, as reported in Table 3. We can see that improving CAR with all the tricks of Sect. 4 allowed the ltlsynt's LAR-based approach to perform better than ltlsynt's Safra-based approaches. 6 Conclusion We have presented a procedure that converts any TELA into a transition-based parity automaton. Our algorithm combines algorithms that are transition-based adaptations or generalizations of known procedures (e.g., CAR is a adaption of the classical SAR and partial degeneration extends the standard generalization technique), thus this paper can also be read as a partial survey of acceptance condition transformations presented under a unified framework. The CAR construction, which is the general case for our paritization algorithm, produces smaller automata than the classical SAR, as it tracks colors instead of states, and uses transition-based acceptance. We further improved 142 F. Renkin et al. this construction by applying more specialized algorithms in each SCC (IAR [15], detection of Biichi-realizable SCCs [14], detection of empty SCCs [3], detection of parity) after simplifying their acceptance. The proposed partial degeneralization procedure is used as a preprocessing step to reduce conjunctions of Inf or disjunction of Fin in the acceptance condition, and to reduce the number of colors that CAR and IAR have to track. Since partial degeneralization only causes a linear blowup in the number of colors removed, it generally helps the CAR construction whose worst case scenario incurs a factorial blowup in the number of colors. Furthermore, after partial degeneralization, the acceptance condition may match more specialized algorithms. The implementation of the described paritization procedure is publicly available in Spot 2.9. While our motivation stems from one approach to produce deterministic parity automata used in Spot, this paritization also works with non-deterministic automata: it preserves the determinism of the input. Acknowledgment. The unoptimized CAR definition of Sect. 3.1 was first implemented in Spot by Maximilien Colange. References 1. Babiak, T., Badie, T., Duret-Lutz, A., Křetínský, M., Strejček, J.: Compositional approach to suspension and other improvements to LTL translation. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 81-98. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39176-7_6 2. Babiak, T., et al.: The hanoi omega-automata format. In: Kroening, D., Pásáreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 479-486. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_31 3. Baier, C, Blahoudek, F., Duret-Lutz, A., Klein, J., Múller, D., Strejček, J.: Generic emptiness check for fun and profit. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 445-461. Springer, Cham (2019). https://doi. org/10.1007/978-3-030-31784-3.26 4. Bloem, R., Chatterjee, K., Jobstmann, B.: Graph Games and reactive synthesis. Handbook of Model Checking, pp. 921-962. Springer, Cham (2018). https://doi. org/10.1007/978-3-319-10575-8.27 5. Carton, O., Maceiras, R.: Computing the Rabin index of a parity automaton. Informatique théorique et applications 33(6), 495-505 (1999) 6. Duret-Lutz, A.: LTL translation improvements in Spot 1.0. Int. J. Critical Comput. Based Syst. 5(1/2), 31-54 (2014) 7. Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0 — A framework for LTL and _>automata manipulation. In: Artho, C, Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122-129. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46520-3_8 8. Emerson, E.A., Lei, C.-L.: Modalities for model checking: branching time logic strikes back. Sci. Comput. Program. 8(3), 275-306 (1987) 9. Esparza, J., Křetínský, J., Sickert, S.: One theorem to rule them all: a unified translation of LTL into o>automata. In: LICS 2018, pp. 384-393. ACM (2018) Practical "Paritizing" of Emerson-Lei Automata 143 10. Farwer, B.: ^-Automata, LNCS 2500, chap. 1, pp. 3-20. Springer, Heidelberg (2001) 11. Gastin, P., Oddoux, D.: Fast LTL to Biichi automata translation. In: CAV 2001, LNCS 2102, pp. 53-65. Springer, Cham (2001) 12. Kfetmsky, J., Esparza, J.: Deterministic automata for the (F,G)-Fragment of LTL. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 7-22. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_7 13. Kfetmsky, J., Meggendorfer, T., Sickert, S.: Owl: a library for w-words, automata, and LTL. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 543-550. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-01090-4_34 14. Krishnan, S.C., Puri, A., Brayton, R.K.: Deterministic ^-automata vis-a-vis deterministic Biichi automata. In: ISAAC 1994, LNCS 834, pp. 378-386. Springer, Cham (1994) 15. Kfetmsky, J., Meggendorfer, T., Waldmann, C, Weininger, M.: Index appearance record for transforming rabin automata into parity automata. In: Legay, A., Mar-garia, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 443-460. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54577-5_26 16. Loding, C: Methods for the transformation of ^-automata: complexity and connection to second order logic. Diploma thesis, Institue of Computer Science and Applied Mathematics (1998) 17. Loding, C: Optimal bounds for transformations of automata. In: Rangan, CP., Raman, V., Ramanujam, R. (eds.) FSTTCS 1999. LNCS, vol. 1738, pp. 97-109. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-46691-6_8 18. Luttenberger, M., Meyer, P.J., Sickert, S.: Practical synthesis of reactive systems from LTL specifications via parity games. Acta Informatica, 57, 3—36 (2020). Originally published on 21 November 2019 19. Major, J., Blahoudek, F., Strejcek, J., Sasarakova, M., Zboncakova, T.: Itl3tela: LTL to small deterministic or nondeterministic Emerson-Lei automata. In: ATVA 2019, LNCS 11781, pp. 357-365. Springer, Cham (2019) 20. Michaud, T., Colange, M.: Reactive synthesis from LTL specification with Spot. In: SYNT 2018 (2018). http://www.lrde.epita.fr/dload/papers/michaud.18.synt.pdf 21. Miiller, D., Sickert, S.: LTL to deterministic Emerson-Lei automata. In: GandALF 2017, vol. 256 of EPTCS, pp. 180-194 (2017) 22. Piterman, N.: From nondeterministic biichi and streett automata to deterministic parity automata. Logical Methods Comput. Sci. 3(3), 1057-1065 (2007) 23. Redziejowski, R.: An improved construction of deterministic omega-automaton using derivatives. Fundamenta Informaticae 119(3-4), 393-406 (2012) 24. Safra, S., Vardi, M.Y.: On ^-automata and temporal logic. In: STOC 1989, pp. 127-137. ACM (1989)