Determinization and Limit-Determinization of Emerson-Lei Automata

Abstract

We study the problem of determinizing $\omega$-automata whose acceptance condition is defined on the transitions using Boolean formulas, also known as transition-based Emerson-Lei automata (TELA). The standard approach to determinize TELA first constructs an equivalent generalized Büchi automaton (GBA), which is later determinized. We introduce three new ways of translating TELA to GBA. Furthermore, we give a new determinization construction which determinizes several GBA separately and combines them using a product construction. An experimental evaluation shows that the product approach is competitive when compared with state-of-the-art determinization procedures. We also study limit-determinization of TELA and show that this can be done with a single-exponential blow-up, in contrast to the known double-exponential lower-bound for determinization. Finally, one version of the limit-determinization procedure yields good-for-MDP automata which can be used for quantitative probabilistic model checking.

This work was funded by DFG grant 389792660 as part of TRR 248, the Cluster of Excellence EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence Strategy), DFG-projects BA-1679/11-1 and BA-1679/12-1, and the Research Training Group QuantLA (GRK 1763).

1 Introduction

Automata on infinite words, also called $\omega$-automata, play a fundamental role in the fields of verification and synthesis of reactive systems [11, 32, 35, 39]. They can be used both to represent properties of systems and the systems themselves. For logical specification languages such as linear temporal logic (LTL), many verification systems, such as Spin [4] or Prism [25], use logic-to-automata translations internally to verify a given system against the specification.

A major research question in this area has been, and still is, the question of whether and how $\omega$-automata can be determinized efficiently [26, 31, 33, 36, 37]. The first single-exponential and asymptotically optimal determinization for Büchi automata was presented in [36]. Deterministic automata are important from a practical point of view as classical automata-based solutions to reactive synthesis and probabilistic verification use deterministic automata [32, 39].

The high complexity of determinization and most logic-to-automata translations have raised the question of more succinct representations of $\omega$-automata. Using generalized acceptance conditions (e.g. generalized Büchi [12] or generalized Rabin [8, 10]) and transition-based [18], rather than state-based, conditions are common techniques in this direction. An even more general approach has led to the HOA-format [1], which represents the acceptance condition as a positive Boolean formula over standard Büchi (${{\text {Inf}}}$) and co-Büchi (${{\text {Fin}}}$) conditions, also called Emerson-Lei conditions [16, 35]. Together with a vast body of work on heuristics and dedicated procedures this standardized format has led to practically usable and mature tools and libraries such as Spot [14] and Owl [24] which support a wide range of operations on $\omega$-automata. Special classes of nondeterministic automata with some of the desired properties of deterministic automata have also been studied. The classes of good-for-MDP [20] and good-for-games [23] automata can be used for quantitative probabilistic model checking of Markov decision processes [19, 38], while limit-deterministic Büchi automata can be used for qualitative model-checking [11]. Dedicated translations from LTL directly to deterministic and limit-deterministic automata have been considered in [17].

This paper considers determinization and limit-determinization of TELA. In contrast to limit-determinization, the theoretical complexity of determinization is well understood (a tight, double-exponential, bound was given in [35, 36]). However, it has not been studied yet from a practical point of view.

Contribution. We propose three new translations from TELA to GBA (Sect. 3) and give an example in which they perform exponentially better than state-of-the-art implementations. We introduce a new determinization procedure for TELA based on a product construction (Sect. 4). Our experiments show that it often outperforms the approaches based on determinizing a single GBA (Sect. 6). A simple adaptation of the product construction produces limit-deterministic TELA of single-exponential size (in contrast to the double-exponential worst-case complexity of full determinization, Sect. 5.1). We show that deciding $\mathbf {Pr}^{\max }_{\mathcal {M}}(\mathcal {L}(\mathcal {A})) > 0$ is NP-complete for limit-deterministic TELA $\mathcal {A}$, and in P if the acceptance of $\mathcal {A}$ is fin-less (Proposition 5.9). Finally, we show how to limit-determinize TELA based on the breakpoint-construction. A version of this procedure yields good-for-MDP Büchi automata (Definition 5.6). Thereby $\mathbf {Pr}^{\max }_{\mathcal {M}}(\mathcal {L}(\mathcal {A}))$ is computable in single-exponential time for arbitrary MDP $\mathcal {M}$ and TELA $\mathcal {A}$ (Theorem 5.15).

Related Work. The upper-bound for TELA-determinization [35, 36] relies on a translation to GBA which first transforms the acceptance formula into disjunctive normal form (DNF). We build on this idea. Another way of translating TELA to GBA was described in [13]. Translations from LTL to TELA have been proposed in [7, 27, 30], and all of them use product constructions to combine automata for subformulas. The emptiness-check for $\omega$-automata under different types of acceptance conditions has been studied in [2, 8, 10, 15], where [2] covers the general case of Emerson-Lei conditions and also considers qualitative probabilistic model checking using deterministic TELA. The generalized Rabin condition from [8, 10] is equivalent to the special DNF that we use and a special case of the hyper-Rabin condition for which the emptiness problem is in P [9, 16]. Probabilistic model checking for deterministic automata under this condition is considered in [10], while [8] is concerned with standard emptiness while allowing nondeterminism. A procedure to transform TELA into parity automata is presented in [34].¹

2 Preliminaries

Automata. A transition-based Emerson-Lei automaton (TELA) $\mathcal {A}$ is a tuple $(Q, \varSigma , \delta , I, \alpha )$, where Q is a finite set of states, $\varSigma$ is a finite alphabet, $\delta \subseteq Q \times \varSigma \times Q$ is the transition relation, $I \subseteq Q$ is the set of initial states and $\alpha$ is a symbolic acceptance condition over $\delta$, which is defined by:

$$\begin{aligned} \alpha {:}{:}= t\!t\mid f\!\!f\mid {{\text {Inf}}}(T) \mid {{\text {Fin}}}(T) \mid (\alpha \vee \alpha ) \mid (\alpha \wedge \alpha ), \text { with } T\subseteq \delta \end{aligned}$$

If $\alpha$ is $t\!t$, $f\!\!f$, ${{\text {Inf}}}(T)$ or ${{\text {Fin}}}(T)$, then it is called atomic. We denote by $\vert \alpha \vert$ the number of atomic conditions contained in $\alpha$, where multiple occurrences of the same atomic condition are counted multiple times. Symbolic acceptance conditions describe sets of transitions $T \subseteq \delta$. Their semantics is defined recursively as follows:

Two acceptance conditions $\alpha$ and $\beta$ are $\delta$-equivalent ($\alpha \equiv _{\delta } \beta$) if for all $T \subseteq \delta$ we have $T \models \alpha \iff T \models \beta$. A run of $\mathcal {A}$ for an infinite word $u = u_0 u_1 \ldots \in \varSigma ^\omega$ is an infinite sequence of transitions $\rho = (q_0, u_0, q_1)(q_1, u_1, q_2)\ldots \in \delta ^\omega$ that starts with an initial state $q_0 \in I$. The set of transitions that appear infinitely often in $\rho$ are denoted by $\inf (\rho )$. A run $\rho$ is accepting ($\rho \models \alpha$) $\mathrm iff$ $\inf (\rho ) \models \alpha$. The language of $\mathcal {A}$, denoted by $\mathcal {L}(\mathcal {A})$, is the set of all words for which there exists an accepting run of $\mathcal {A}$. The sets of infinite words which are the language of some TELA are called $\omega$-regular. A TELA $\mathcal {A}$ is deterministic if the set of initial states contains exactly one state and the transition relation is a function $\delta : Q \times \varSigma \rightarrow Q$. It is complete, if for all $(q,a) \in Q \times \varSigma$: $\delta \cap \{(q,a,q') \mid q' \in Q\} \ne \varnothing$. A Büchi condition is an acceptance condition of the form ${{\text {Inf}}}(T)$ and a generalized Büchi condition is a condition of the form $\bigwedge _{1 \le i \le k} {{\text {Inf}}}(T_i)$. We call the sets $T_i$ appearing in a generalized Büchi condition its acceptance sets. Rabin (resp. Street) conditions are of the form $\bigvee _{1 \le i \le k} ({{\text {Fin}}}(F_i) \wedge {{\text {Inf}}}(T_i))$ (resp. $\bigwedge _{1 \le i \le k} ({{\text {Fin}}}(F_i) \vee {{\text {Inf}}}(T_i))$).

Probabilistic Systems. A labeled Markov decision process (MDP) $\mathcal {M}$ is a tuple $(S,s_0,{\text {Act}},P,\varSigma ,L)$ where S is a finite set of states, $s_0 \in S$ is the initial state, ${\text {Act}}$ is a finite set of actions, $P : S \times {\text {Act}}\times S \rightarrow [0,1]$ defines the transition probabilities with $\sum _{s' \in S} P(s,\alpha ,s') \in \{0,1\}$ for all $(s,\alpha ) \in S \times {\text {Act}}$ and $L : S \rightarrow \varSigma$ is a labeling function of the states into a finite alphabet $\varSigma$. Action $\alpha \in {\text {Act}}$ is enabled in s if $\sum _{s' \in S} P(s,\alpha ,s') = 1$, and ${\text {Act}}(s) = \{\alpha \mid \alpha \text { is enabled in } s\}$. A path of $\mathcal {M}$ is an infinite sequence $s_0 \alpha _0 s_1 \alpha _1 \ldots \in (S \times {\text {Act}})^{\omega }$ such that $P(s_i,\alpha _i,s_{i+1}) > 0$ for all $i \ge 0$. The set of all paths of $\mathcal {M}$ is denoted by ${\text {Paths}}(\mathcal {M})$ and ${\text {Paths}}_{{\text {fin}}}(\mathcal {M})$ denotes the finite paths. Given a path $\pi = s_0 \alpha _0 s_1 \alpha _1 \ldots$, we let $L(\pi ) = L(s_0)L(s_1) \ldots \in \varSigma ^{\omega }$. A Markov chain is an MDP with $|{\text {Act}}(s)| \le 1$ for all states s. A scheduler of $\mathcal {M}$ is a function $\mathfrak {S}: (S\times {\text {Act}})^*\times S \rightarrow {\text {Act}}$ such that $\mathfrak {S}(s_0 \alpha _0 \ldots s_n) \in {\text {Act}}(s_n)$. It induces a Markov chain $\mathcal {M}_{\mathfrak {S}}$ and thereby a probability measure over ${\text {Paths}}(\mathcal {M})$. The probability of a set of paths $\varPi$ starting in $s_0$ under this measure is $\mathrm {Pr}_\mathcal {M}^{\mathfrak {S}}(\varPi )$. For an $\omega$-regular property $\varPhi \subseteq \varSigma ^{\omega }$ we define $\mathbf {Pr}^{\max }_{\mathcal {M}}(\varPhi ) = \sup _{\mathfrak {S}}\mathrm {Pr}_{\mathcal {M}}^{\mathfrak {S}}(\{\pi \mid \pi \in {\text {Paths}}(\mathcal {M}) \text { and } L(\pi ) \in \varPhi \})$. See [3, Chapter 10] for more details.

3 From TELA to Generalized Büchi Automata

3.1 Operations on Emerson-Lei Automata

The first operator takes a TELA and splits it along the top-level disjuncts of the acceptance condition. Let $\mathcal {A} = (Q, \varSigma , \delta , I, \alpha )$ be a TELA where $\alpha = \bigvee _{1 \le i \le m} \alpha _i$ and the $\alpha _i$ are arbitrary acceptance conditions. We define ${\text {split}}(\mathcal {A}) := (\mathcal {A}_1, \ldots , \mathcal {A}_m)$ with $\mathcal {A}_i = (Q, \varSigma , \delta , I, \alpha _i)$ for $1 \le i \le m$, and ${\text {split}}(\mathcal {A})[i] := \mathcal {A}_i$.

Lemma 3.1

It holds that $\mathcal {L}(\mathcal {A}) = \bigcup _{1 \le i \le m} \mathcal {L}\big ({\text {split}}(\mathcal {A})[i]\big )$.

The analogous statement does not hold for conjunction and intersection (cf [21, Fig. 5]). We also need constructions to realize the union of a sequence of automata. This can either be done using the sum (i.e. disjoint union) or the disjunctive product of the state spaces. We define a general sum (simply called sum) operation and one that preserves GBA acceptance (called GBA-specific sum). The disjunctive product construction for TELA is mentioned in [13] and similar constructions are used in [27, 30]. While the sum operations yield smaller automata in general, only the product construction preserves determinism.

Definition 3.2

Let $\mathcal {A}_i = (Q_i, \varSigma , \delta _i, I_i, \alpha _i)$, with $i \in \{0,1\}$, be two complete TELA with disjoint state-spaces. The sum of $\mathcal {A}_0$ and $\mathcal {A}_1$ is defined as follows:

$$\begin{aligned} \mathcal {A}_0 \oplus \mathcal {A}_1 = \big (Q_0 \cup Q_1, \varSigma , \delta _0 \cup \delta _1, I_0 \cup I_1, (\alpha _0 \wedge {{\text {Inf}}}(\delta _0)) \vee (\alpha _1 \wedge {{\text {Inf}}}(\delta _1) \big ) \end{aligned}$$

If $\alpha _i = {{\text {Inf}}}(T_1^i) \wedge \ldots \wedge {{\text {Inf}}}(T_k^i)$, with $i \in \{0,1\}$, (i.e. both automata are GBA), then we can use the GBA-specific sum:

$$\begin{aligned} \mathcal {A}_0 \oplus _{GBA}\mathcal {A}_1 = \big (Q_0 \cup Q_1, \varSigma , \delta _0 \cup \delta _1, I_0 \cup I_1, ({{\text {Inf}}}(T_1^0 \cup T_1^1) \wedge \ldots \wedge {{\text {Inf}}}(T_k^0 \cup T_k^1)) \big ) \end{aligned}$$

The disjunctive product is defined as follows:

$$\begin{aligned} \mathcal {A}_0 \otimes \mathcal {A}_1 = \big (Q_0 \times Q_1, \varSigma , \delta _\otimes , I_0 \times I_1, (\uparrow _{}\!\!(\alpha _0) \vee \uparrow _{}\!\!(\alpha _1))\big ) \end{aligned}$$

with $\delta _\otimes = \big \lbrace \big ((q_0, q_1), a, (q_0', q_1')\big ) \bigm \vert (q_0,a,q_0') \in \delta _0 \text { and } (q_1,a,q_1') \in \delta _1 \big \rbrace$ and ${\uparrow _{}\!\!(\alpha _i)}$ is constructed by replacing every occurring set of transitions T in $\alpha _i$ by $\big \lbrace \big ((q_0, q_1), u, (q_0', q_1') \big ) \in \delta _\otimes \bigm \vert (q_i, u, q_i') \in T \big \rbrace$.

The additional ${{\text {Inf}}}(\delta _0)$ and ${{\text {Inf}}}(\delta _1)$ atoms in the acceptance condition of $\mathcal {A}_0 \oplus \mathcal {A}_1$ are essential (see [21, Fig. 6]). We can apply the GBA-specific sum to any two GBA by adding ${{\text {Inf}}}(\delta _i)$ atoms until the acceptance conditions are of equal length. Many of our constructions will require the acceptance condition of the TELA to be in DNF. We will use the following normal form throughout the paper (also called generalized Rabin in [8, 10]).

Definition 3.3

(DNF for TELA). Let $\mathcal {A} = (Q, \varSigma ,\delta , I,\alpha )$ be a TELA. We say that $\mathcal {A}$ is in DNF if $\alpha$ is of the form $\alpha = \bigvee _{1 \le i \le m} \alpha _i$, with $\alpha _i = {{\text {Fin}}}(T^i_0) \wedge \bigwedge _{1 \le j \le k_i} {{\text {Inf}}}(T^i_j)$ and such that all $k_i \ge 1$.

The reason that a single ${{\text {Fin}}}$ atom in each disjunct is enough is that ${{\text {Fin}}}(T_1) \wedge {{\text {Fin}}}(T_2) \equiv _{\delta } {{\text {Fin}}}(T_1 \cup T_2)$ for all $T_1,T_2,\delta$. Taking $k_i \ge 1$ is also no restriction, as we can always add $\wedge \, {{\text {Inf}}}(\delta )$ to any disjunct. Using standard Boolean operations one can transform a TELA with acceptance $\beta$ into DNF by just translating the acceptance formula into a formula $\alpha$ of the above form, with $|\alpha | \le 2^{|\beta |}$.

Fin-Less Acceptance. To transform a TELA in DNF (see Definition 3.3) into an equivalent one without ${{\text {Fin}}}$-atoms we use the idea of [8, 13]: a main copy of $\mathcal {A}$ is connected to one additional copy for each disjunct $\alpha _i$ of the acceptance condition, in which transitions from $T_0^i$ are removed. The acceptance condition ensures that every accepting run leaves the main copy eventually. Figure 1 shows an example.

Fig. 1.

Example of applying ${\text {removeFin}}$ and ${\text {removeFin}}_{{\text {GBA}}}$ (Definition 3.4) to the automaton on the left. The result is the automaton on the right with acceptance $\alpha '$ (${\text {removeFin}}$), respectively $\alpha ''$ (${\text {removeFin}}_{{\text {GBA}}}$).

Definition 3.4

Let $\mathcal {F}_i = (Q_i, \varSigma , \delta _i, I_i, \phi _i)$, where $Q_i = \{q^{(i)} \mid q \in Q\}$, $\delta _i = \{(q^{(i)},a,{q'^{(i)}}) \mid (q,a,q') \in \delta \setminus T^i_0\}$ and $\phi _i = \bigwedge _{1 \le j \le k_i} {{\text {Inf}}}(U^i_j)$, where $U^i_j = \{(q^{(i)},a,{q'^{(i)}}) \mid (q,a,q') \in T_j^i \setminus T^i_0\}$. Let ${\text {removeFin}}(\mathcal {A}) = (Q', \varSigma , \delta ', I, \alpha ')$ and ${\text {removeFin}}_{{\text {GBA}}}(\mathcal {A}) = (Q', \varSigma , \delta ', I, \alpha '')$, where $Q' = Q \cup \bigcup _{1 \le i \le m} Q_{i}$ and:

• $\delta ' = \delta \cup \bigcup _{1 \le i \le m}\big (\delta _{i} \cup \{(q, a, {q'^{(i)}}) \mid (q, a, q') \in \delta \} \big )$

• $\alpha ' ~\!= \bigvee _{1 \le i \le m} \phi _i$

• $\alpha '' = \bigwedge _{1\le j \le k} {{\text {Inf}}}(U_j^1 \cup \ldots \cup U_j^m)$, with $k = \max _{i} k_i$ and $U_j^i = \delta _i$ if $k_i < j \le k$.

Lemma 3.5

It holds that $\mathcal {L}(\mathcal {A}) = \mathcal {L}({\text {removeFin}}(\mathcal {A})) = \mathcal {L}({\text {removeFin}}_{{\text {GBA}}}(\mathcal {A}))$.

While ${\text {removeFin}}(\mathcal {A})$ is from [8, 13], ${\text {removeFin}}_{{\text {GBA}}}(\mathcal {A})$ is a variant that differs only in the acceptance and always produces GBA. Both consist of $m+1$ copies of $\mathcal {A}$ (with ${{\text {Fin}}}$-transitions removed).

3.2 Construction of Generalized Büchi Automata

Fig. 2.

A class of TELA where generating the CNF leads to $2^n$ many conjuncts.

Construction of Spot. The transformation from TELA to GBA from [13] is implemented in Spot [14]. It transforms the automaton into DNF and then applies (an optimized version of) ${\text {removeFin}}$. The resulting fin-less acceptance condition is translated into conjunctive normal form (CNF). As ${{\text {Inf}}}(T_1) \vee {{\text {Inf}}}(T_2) \equiv _{\delta } {{\text {Inf}}}(T_1 \cup T_2)$ holds for all $\delta$, one can rewrite any fin-less condition in CNF into a conjunction of ${{\text {Inf}}}$-atoms, which is a generalized Büchi condition. When starting with a TELA $\mathcal B$ with acceptance $\beta$ and N states, one gets a GBA with $N \, 2^{O(|\beta |)}$ states and $2^{O(|\beta |)}$ acceptance sets, as the fin-removal may introduce exponentially (in $|\beta |$) many copies, and the CNF may also be exponential in $|\beta |$.

Transforming a fin-less automaton into a GBA by computing the CNF has the advantage of only changing the acceptance condition, and in some cases it produces simple conditions directly. For example, Spot’s TELA to GBA construction transforms a Rabin into a Büchi automaton, and a Streett automaton with m acceptance pairs into a GBA with m accepting sets. However, computing the CNF may also incur an exponential blow-up (Fig. 2 shows such an example).

Copy-Based Approaches. We now describe three approaches (remFin$\rightarrow$split$\alpha$, split$\alpha$ $\rightarrow$remFin and remFin$\rightarrow$rewrite$\alpha$), which construct GBA with at most $|\beta |$ acceptance sets. On the other hand, they generally produce automata with more states. They are based on [35] which first translates copies of $\mathcal {A}$ (corresponding to the disjuncts of the acceptance condition) to GBA, and then takes their sum. However, it is not specified in [35] how exactly ${{\text {Fin}}}$-atoms should be removed (they were concerned only with the theoretical complexity). We define:

With ${\text {removeFin}}$ as defined in Definition 3.4, the approaches remFin$\rightarrow$split$\alpha$ and split$\alpha$ $\rightarrow$remFin produce the same automata (after removing non-accepting SCC’s in remFin$\rightarrow$split$\alpha$), and all three approaches create O(m) copies of $\mathcal {A}$. Our implementation uses an optimized variant of ${\text {removeFin}}$, as provided by Spot, which leads to different results for all three approaches.

4 Determinization

Determinization via Single GBA. The standard way of determinizing TELA is to first construct a GBA, which is then determinized. Dedicated determinization procedures for GBA with N states and K acceptance sets produce deterministic Rabin automata with $2^{O(N (\log N + \log K))}$ states [37]. For a TELA $\mathcal {B}$ with n states and acceptance $\beta$, the above translations yield GBA with $N = n \, 2^{O(|\beta |)}$ and $K = 2^{O(|\beta |)}$ (Spot’s construction) or $N = n \, 2^{O(|\beta |)}$ and $K = O(|\beta |)$ (copy-based approaches). We evaluate the effect of the translations to GBA introduced in the previous chapter in the context of determinization in Sect. 6.

Determinization via a Product Construction. Another way to determinize a TELA $\mathcal {A}$ in DNF is to determinize the automata ${\text {split}}(\mathcal {A})[i]$ one by one and then combining them with the disjunctive product construction of Definition 3.2:

$$\begin{aligned} \bigotimes _{1 \le i \le m} {\text {det}}\big ({\text {removeFin}}({\text {split}}(\mathcal {A})[i])\big ) \end{aligned}$$

where “${\text {det}}$” is any GBA-determinization procedure. Let $\mathcal B$ be a TELA with acceptance $\beta$ and n states, and let $\alpha$ be an equivalent condition in DNF with m disjuncts. Assuming an optimal GBA-determinization procedure, the product combines m automata with $2^{O(n (\log n + \log |\beta |))}$ states and hence has $\big (2^{O(n \, (\log n + \log |\beta |))}\big )^m = 2^{O ( 2^{|\beta |} \cdot n (\log n + \log |\beta |))}$ states.

5 Limit-Deterministic TELA

Limit-determinism has been studied mainly in the context of Büchi automata [11, 38, 39], and we define it here for general TELA.

Definition 5.1

A TELA $\mathcal {A} = (Q,\varSigma ,\delta ,I,\alpha )$ is called limit-deterministic if there exists a partition $Q_N,Q_D$ of Q such that

• 1. $\delta \cap (Q_D \times \varSigma \times Q_N) = \varnothing$,

• 2. for all $(q,a) \in Q_D \times \varSigma$ there exists at most one $q'$ such that $(q,a,q') \in \delta$,

• 3. every accepting run $\rho$ of $\mathcal {A}$ satisfies $\inf (\rho ) \cap (Q_N \times \varSigma \times Q_N) = \varnothing$.

This is a semantic definition and as checking emptiness of deterministic TELA is already coNP-hard, checking whether a TELA is limit-deterministic is also.

Proposition 5.2

Checking limit-determinism for TELA is coNP-complete.

An alternative syntactic definition for TELA in DNF, which implies limit-determinism, is provided in Definition 5.3.

Definition 5.3

A TELA $\mathcal {A} = (Q,\varSigma ,\delta ,\{q_0\},\alpha )$ in DNF, with $\alpha = \bigvee _{1 \le i \le m} \alpha _i$, $\alpha _i = {{\text {Fin}}}(T^i_0) \wedge \bigwedge _{1 \le j \le k_i} {{\text {Inf}}}(T^i_j)$ and $k_i \ge 1$ for all i, is syntactically limit-deterministic if there exists a partition $Q_N,Q_D$ of Q satisfying 1. and 2. of Definition 5.1 and additionally $T^i_j \subseteq Q_D \times \varSigma \times Q_D \text { for all } i \le m \text { and } 1 \le j \le k_i$.

5.1 Limit-Determinization

We first observe that replacing the product by a sum in the product-based determinization above yields limit-deterministic automata of single-exponential size (in contrast to the double-exponential lower-bound for determinization). Let $\mathcal {A}$ be a TELA in DNF with n states and acceptance $\alpha = \bigvee _{1 \le i \le m} \alpha _i$, where $\alpha _i = {{\text {Fin}}}(T^i_0) \wedge \bigwedge _{1 \le j \le k_i} {{\text {Inf}}}(T^i_j)$ (see Definition 3.3), and let $\mathcal {A}_i = {\text {split}}(\mathcal {A})[i]$.

Proposition 5.4

$\bigoplus _{1 \le i \le m} {\text {det}}({\text {removeFin}}(\mathcal {A}_i))$ is limit-deterministic and of size $\sum _{1 \le i \le m} |{\text {det}}(\mathcal {A}_i)| = m \cdot 2^{O(n \, (\log n + \log k))}$, where $k = \max \{k_i \mid 1 \le i \le m\}$.

If “$\det$” is instantiated by a GBA-determinization that produces Rabin automata, then the result is in DNF and syntactically limit-deterministic. Indeed, in this case the only nondeterminism is the choice of the initial state. But “$\det$” can, in principle, also be replaced by any limit-determinization procedure for GBA.

We now extend the limit-determinization constructions of [11] (for Büchi automata) and [5, 6, 19] (for GBA) to Emerson-Lei conditions in DNF. These constructions use an initial component and an accepting breakpoint component [28] for $\mathcal {A}$, which is deterministic. The following construction differs in two ways: there is one accepting component per disjunct of the acceptance condition, and the accepting components are constructed from $\mathcal {A}$ without considering the ${{\text {Fin}}}$-transitions of that disjunct. To define the accepting components we use the subset transition function $\theta$ associated with $\delta$: $\theta (P,a) = \bigcup _{q \in P}\{ q' \mid (q,a,q') \in \delta \}$ for $(P,a) \in 2^Q \times \varSigma$, and additionally we define $\theta |_T(P,a) = \bigcup _{q \in P}\{ q' \mid (q,a,q') \in \delta \cap T \}$. These functions are extended to finite words in the standard way.

Definition 5.5

Let $\theta _i = \theta |_{\delta \setminus T_0^i}$ and define $\mathcal {BP}_{i} = (Q_i,\varSigma ,\delta _i,\{p_0\},{{\text {Inf}}}(\delta ^{{\text {break}}}_i))$ with: $Q_i = \{(R,B,l) \in 2^Q \times 2^Q \times \{0, \ldots , k_i\} \mid B \subseteq R \}$, $p_0 = (I,\varnothing ,0)$ and

$$\begin{aligned} \delta ^{{\text {main}}}_i&= \left\{ ((R_1, B_1, l), a, (R_2, B_2, l)) \mid \begin{array}{l} R_2 = \theta _i (R_1, a), \\ B_2 = \theta _i (B_1, a) \cup \theta _i|_{T_l^i}(R_1, a) \end{array} \right\} \\ \delta ^{{\text {break}}}_i&= \left\{ ((R_1, B_1, l), a, (R_2, \varnothing , l') \mid \begin{array}{l} ((R_1, B_1, l), a, (R_2, B_2, l)) \in \delta ^{{\text {main}}}_i,\\ R_2 = B_2,\\ l' = (l+1) \bmod (k_i+1) \end{array} \right\} \\ \delta _i&= \bigl \{((R_1, B_1, l), a, (R_2, B_2, l)) \in \delta ^{{\text {main}}}_i \mid R_2 \ne B_2 \bigr \} \cup \delta ^{{\text {break}}}_i \end{aligned}$$

In state (R, B, l), intuitively R is the set of states reachable for the prefix word in $\mathcal {A}$ without using transitions from $T_0^i$, while B are the states in R which have seen a transition in $T_l^i$ since the last “breakpoint”. The breakpoint-transitions are $\delta ^{{\text {break}}}_i$, which occur when all states in R have seen an accepting transition since the last breakpoint (namely if $R = B$). The breakpoint construction underapproximates the language of a given GBA, in general.

We define two limit-deterministic Büchi automata (LDBA) $\mathcal {G}^{{\text {LD}}}_{\mathcal {A}}$ and $\mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}$ where $\mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}$ is additionally good-for-MDP (GFM) [20]. This means that $\mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}$ can be used to solve certain quantitative probabilistic model checking problems (see Sect. 5.2). Both use the above breakpoint automata as accepting components. While $\mathcal {G}^{{\text {LD}}}_{\mathcal {A}}$ simply uses a copy of $\mathcal {A}$ as initial component, $\mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}$ uses the deterministic subset-automaton of $\mathcal {A}$ (it resembles the cut-deterministic automata of [5]). Furthermore, to ensure the GFM property, there are more transitions between initial and accepting copies in $\mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}$. The construction of $\mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}$ extends the approach for GBA in [19] (also used for probabilistic model checking) to TELA. We will distinguish elements from sets $Q_i$ for different i from Definition 5.5 by using subscripts (e.g. $(R,P,l)_i$) and assume that these sets are pairwise disjoint.

Definition 5.6

($\mathcal {G}^{{\text {LD}}}_{\mathcal {A}}$ and $\mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}$). Let $Q_{{\text {acc}}} = \bigcup _{1 \le i \le m} Q_i$, $\delta _{{\text {acc}}} = \bigcup _{1 \le i \le m} \delta _i$ and $\alpha _{{\text {acc}}} = {{\text {Inf}}}(\bigcup _{1 \le i \le m} \delta ^{{\text {break}}}_i)$. Define

$$\begin{aligned} \mathcal {G}^{{\text {LD}}}_{\mathcal {A}} = (Q \cup Q_{{\text {acc}}},\varSigma ,\delta ^{{\text {LD}}},I,\alpha ') \; \text { and } \; \mathcal {G}^{{\text {GFM}}}_{\mathcal {A}} = (2^{Q} \cup Q_{{\text {acc}}},\varSigma ,\delta ^{{\text {GFM}}},\{I\},\alpha ') \end{aligned}$$

with

$$\begin{aligned} \delta ^{{\text {LD}}}&= \delta \cup \delta _{{\text {bridge}}}^{{\text {LD}}}\cup \delta _{{\text {acc}}} \quad \text { and } \quad \delta ^{{\text {GFM}}}= \theta \cup \delta _{{\text {bridge}}}^{{\text {GFM}}}\cup \delta _{{\text {acc}}}\\ \delta _{{\text {bridge}}}^{{\text {LD}}}&= \bigl \{\bigl (q,a,(\{q'\},\varnothing ,0)_i\bigr ) \mid (q,a,q') \in \delta \text { and } 1 \le i \le m \bigr \}\\[0.25ex] \delta _{{\text {bridge}}}^{{\text {GFM}}}&= \bigl \{\bigl (P,a,(P',\varnothing ,0)_i\bigr ) \mid P' \subseteq \theta (P,a) \text { and } 1 \le i \le m \bigr \} \end{aligned}$$

As $\delta _i^{{\text {break}}} \subseteq \delta _{{\text {acc}}}$ for all i, both $\mathcal {G}^{{\text {LD}}}_{\mathcal {A}}$ and $\mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}$ are syntactically limit-deterministic. The proofs of correctness are similar to ones of the corresponding constructions for GBA [5, Thm. 7.6]. We show later in Proposition 5.14 that $\mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}$ is GFM.

Theorem 5.7

$\mathcal {G}^{{\text {LD}}}_{\mathcal {A}}$ and $\mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}$ are syntactically limit-deterministic and satisfy $\mathcal {L}(\mathcal {G}^{{\text {LD}}}_{\mathcal {A}}) = \mathcal {L}(\mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}) = \mathcal {L}(\mathcal {A})$. Their number of states is in $O(n + 3^n \, m \, k)$ for $\mathcal {G}^{{\text {LD}}}_{\mathcal {A}}$ and $O(2^n + 3^n \, m \, k) = O(|\alpha |^2 \cdot 3^n)$ for $\mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}$, where $k = \max \{k_i \mid 1 \le i \le m\}$.

Corollary 5.8

Given TELA $\mathcal B$ (not necessarily in DNF) with acceptance condition $\beta$ and N states, there exists an equivalent LDBA with $2^{O(|\beta | + N)}$ states.

5.2 Probabilistic Model Checking

We now discuss how these constructions can be used for probabilistic model checking. First, consider the qualitative model checking problem to decide $\mathbf {Pr}^{\max }_{\mathcal {M}}(\mathcal {L}(\mathcal {A})) > 0$, under the assumption that $\mathcal {A}$ is a limit-deterministic TELA. While NP-hardness follows from the fact that the problem is already hard for deterministic TELA [29, Thm. 5.13], we now show that it is also in NP. Furthermore, it is in P for automata with a fin-less acceptance condition. This was already known for LDBA [11], and our proof uses similar arguments.

Proposition 5.9

Deciding $\mathbf {Pr}_{\mathcal {M}}^{\max }(\mathcal {L}(\mathcal {A})) > 0$, given an MDP $\mathcal {M}$ and a limit-deterministic TELA $\mathcal {A}$, is NP-complete. If $\mathcal {A}$ has a fin-less acceptance condition, then the problem is in P.

Now we show that $\mathcal {G}^{{\text {GFM}}}_\mathcal {A}$ is good-for-MDP [20]. In order to define this property, we introduce the product of an MDP with a nondeterministic automaton in which, intuitively, the scheduler is forced to resolve the nondeterminism by choosing the next state of the automaton (see [20, 23]). We assume that the automaton used to build the product has a single initial state, which holds for $\mathcal {G}^{{\text {GFM}}}_\mathcal {A}$.

Definition 5.10

Given an MDP $\mathcal {M}= (S,s_0,{\text {Act}},P,\varSigma ,L)$ and TELA $\mathcal {G} = (Q,\varSigma ,\delta ,\{q_0\},\alpha )$ we define the MDP $\mathcal {M}\times \mathcal {G} = (S \times Q, (s_0,q_0), {\text {Act}}\times Q, P^{\times }, \varSigma , L^{\times })$ with $L^{\times }((s,q)) = L(s)$ and

$$ P^{\times }\bigl ((s,q),(\alpha ,p),(s',q')\bigr ) = {\left\{ \begin{array}{ll} P(s,\alpha ,s') &{} \text {if } p = q' \text { and } (q,L(s),q') \in \delta \\ 0 &{} \text {otherwise} \end{array}\right. }$$

We define the accepting paths $\varPi _{acc}$ of $\mathcal {M}\times \mathcal {G}$ to be:

$$\begin{aligned} \varPi _{acc} = \{(s_0,q_0)\alpha _0(s_1,q_1)\alpha _1 \ldots \in {\text {Paths}}(\mathcal {M}\times \mathcal {G}) \mid q_0, L(s_0), q_1, L(s_1) \ldots \models \alpha \} \end{aligned}$$

A Büchi automaton $\mathcal {G}$ is good-for-MDP (GFM) if $\mathbf {Pr}^{\max }_{\mathcal {M}}(\mathcal {L}(\mathcal {G})) = \mathbf {Pr}^{\max }_{\mathcal {M}\times \mathcal {G}}(\varPi _{acc})$ holds for all MDP $\mathcal {M}$ [20]. The inequality “$\ge$” holds for all automata [23, Thm. 1], but the other direction requires, intuitively, that a scheduler on $\mathcal {M}\times \mathcal {G}$ is able to safely resolve the nondeterminism of the automaton based on the prefix of the run. This is trivially satisfied by deterministic automata, but good-for-games automata also have this property [23]. Limit-deterministic Büchi automata are not GFM in general, for example, $\mathcal {G}^{{\text {LD}}}_{\mathcal {A}}$ may not be (see Example 5.12).

We fix an arbitrary MDP $\mathcal {M}$ and show that $\mathbf {Pr}^{\max }_{\mathcal {M}}(\mathcal {L}(\mathcal {A})) \le \mathbf {Pr}^{\max }_{\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_\mathcal {A}}(\varPi _{acc})$. To this end we show that for any finite-memory scheduler $\mathfrak {S}$ on $\mathcal {M}$ we find a scheduler $\mathfrak {S'}$ on $\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_\mathcal {A}$ such that $\mathrm {Pr}^{\mathfrak {S}}_{\mathcal {M}}(\mathcal {L}(\mathcal {A})) \le \mathrm {Pr}^{\mathfrak {S}'}_{\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_\mathcal {A}}(\varPi _{acc})$. The restriction to finite-memory schedulers is allowed because the maximal probability to satisfy an $\omega$-regular property is always attained by such a scheduler [3, Secs. 10.6.3 and 10.6.4]. Let $\mathcal {M}_{\mathfrak {S}} \times \mathcal {D}$ be the product of the induced finite Markov chain $M_{\mathfrak {S}}$ with $\mathcal {D} = \bigotimes _{1 \le i \le m} \mathcal {D}_i$, where $\mathcal {D}_i = {\text {det}}\big ({\text {removeFin}}({\text {split}}(\mathcal {A})[i])\big )$ and “${\text {det}}$” is the GBA-determinization procedure from [37], which makes $\mathcal {D}$ a deterministic Rabin automaton. The scheduler $\mathfrak {S}'$ is constructed as follows. It stays inside the initial component of $\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}$ and mimics the action chosen by $\mathfrak {S}$ until the corresponding path in $\mathcal {M}_{\mathfrak {S}} \times \mathcal {D}$ reaches an accepting bottom strongly connected component (BSCC) B. This means that the transitions of $\mathcal {D}$ induced by B satisfy one of the Rabin pairs. The following lemma shows that in this case there exists a state in one of the breakpoint components to which $\mathfrak {S}'$ can safely move.

Lemma 5.11

Let $\mathfrak {s}$ be a state in an accepting BSCC B of $\mathcal {M}_{\mathfrak {S}} \times \mathcal {D}$ and $\pi _1$ be a finite path that reaches $\mathfrak {s}$ from the initial state of $\mathcal {M}_{\mathfrak {S}} \times \mathcal {D}$. Then, there exists $1 \le i \le m$ and $Q' \subseteq \theta \bigl (I,L(\pi _1)\bigr )$ such that:

$$\begin{aligned} \mathrm {Pr}_{\mathfrak {s}}(\{\pi \mid L(\pi ) \text { is accepted from } (Q',\varnothing ,0) \text { in } \mathcal {BP}_i\bigl \}) = 1 \end{aligned}$$

The lemma does not hold if we restrict ourselves to singleton $\{q\} \subseteq \theta \bigl (I,L(\pi _1)\bigr )$ (see Example 5.12). Hence, restricting $\delta _{{\text {bridge}}}^{{\text {GFM}}}$ to such transitions (as for $\delta _{{\text {bridge}}}^{{\text {LD}}}$, see Definition 5.6) would not guarantee the GFM property.

Example 5.12

Consider the automaton $\mathcal {A}$ with states $\{\mathtt {a}_i\mathtt {b}_j \mid i,j \in \{1,2\}\} \cup \{\mathtt {b}_i\mathtt {a}_j \mid i,j \in \{1,2\}\}$, where $\mathtt {a}_i\mathtt {b}_j$ has transitions labeled by $a_i$ to $\mathtt {b}_j\mathtt {a}_1$ and $\mathtt {b}_j\mathtt {a}_2$. Transitions of states $\mathtt {b}_i\mathtt {a}_j$ are defined analogously, and all states in $\{\mathtt {a}_i\mathtt {b}_j \mid i,j \in \{1,2\}\}$ are initial (Fig. 3a shows the transitions of $\mathtt {a}_1\mathtt {b}_1$). All transitions are accepting for a single Büchi condition, and hence $\mathcal {L}(\mathcal {A}) = (\{a_i b_j \mid i,j \in \{1,2\}\})^{\omega }$.

Consider the Markov chain $\mathcal {M}$ in Fig. 3b (transition probabilities are all 1/2 and omitted in the figure). Clearly, $\mathrm {Pr}_{\mathcal {M}}(\mathcal {L}(\mathcal {A})) = 1$. Figure 3c shows a part of the product of $\mathcal {M}$ with the breakpoint automaton $\mathcal {BP}$ for $\mathcal {A}$ (Definition 5.5) starting from $\bigl (a_1,(\{\mathtt {a}_1\mathtt {b}_1\},\varnothing ,0)\bigr )$. The state $\bigl (b_2,(\{\mathtt {b}_1\mathtt {a}_1,\mathtt {b}_1\mathtt {a}_2\},\varnothing ,0)\bigr )$ is a trap state as $\mathtt {b}_1\mathtt {a}_1$ and $\mathtt {b}_1\mathtt {a}_2$ have no $b_2$-transition. Hence, $\bigl (a_1,(\{\mathtt {a}_1\mathtt {b}_1\},\varnothing ,0)\bigr )$ generates an accepting path with probability at most 1/2. This is true for all states $\bigl (s,(P',\varnothing ,0)\bigr )$ of $\mathcal {M}\times \mathcal {BP}$ where $P'$ is a singleton. But using $\delta _{{\text {bridge}}}^{{\text {LD}}}$ to connect initial and accepting components implies that any accepting path sees such a state. Hence, using $\delta _{{\text {bridge}}}^{{\text {LD}}}$ to define $\mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}$ would not guarantee the GFM property.

Fig. 3.

Restricting $\delta _{{\text {bridge}}}^{{\text {GFM}}}$ to transitions with endpoints of the form $(s, (\{q\},\varnothing ,0))$ (similar to $\delta _{{\text {bridge}}}^{{\text {LD}}}$) would not guarantee the GFM property (see Example 5.12).

Using Lemma 5.11 we can define $\mathfrak {S}'$ such that the probability accepting paths under $\mathfrak {S}'$ in $\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}$ is at least as high as that of paths with label in $\mathcal {L}(\mathcal {A})$ in $\mathcal {M}_{\mathfrak {S}}$. This is the non-trivial direction of the GFM property.

Lemma 5.13

For every finite-memory scheduler $\mathfrak {S}$ on $\mathcal {M}$, there exists a scheduler $\mathfrak {S}'$ on $\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}$ such that:

$$\begin{aligned} \mathrm {Pr}_{\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}}^{\mathfrak {S}'}(\varPi _{acc}) \ge \mathrm {Pr}_{\mathcal {M}}^{\mathfrak {S}}(\mathcal {L}(\mathcal {A})) \end{aligned}$$

Proposition 5.14

The automaton $\mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}$ is good-for-MDP.

To compute $\mathbf {Pr}_{\mathcal {M}}^{\max }(\mathcal {L}(\mathcal {B}))$ one can translate $\mathcal {B}$ into an equivalent TELA $\mathcal {A}$ in DNF, then construct $\mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}$ and finally compute $\mathbf {Pr}^{\max }_{\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}}(\varPi _{{\text {acc}}})$. The automaton $\mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}$ is single-exponential in the size of $\mathcal {B}$ by Theorem 5.7, and $\mathbf {Pr}^{\max }_{\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}}(\varPi _{{\text {acc}}})$ can be computed in polynomial time in the size of $\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}$ [3, Thm. 10.127].

Theorem 5.15

Given a TELA $\mathcal {B}$ (not necessarily in DNF) and an MDP $\mathcal {M}$, the value $\mathbf {Pr}^{\max }_{\mathcal {M}}(\mathcal {L}(\mathcal {B}))$ can be computed in single-exponential time.

6 Experimental Evaluation

The product approach combines a sequence of deterministic automata using the disjunctive product. We introduce the langcover heuristic: the automata are “added” to the product one by one, but only if their language is not already subsumed by the automaton constructed so far. This leads to substantially smaller automata in many cases, but is only efficient if checking inclusion for the considered automata types is efficient. In our case this holds (the automata are deterministic with a disjunction of parity conditions as acceptance), but it is not the case for arbitrary deterministic TELA, or nondeterministic automata.

Implementation. We compare the following implementations of the constructions discussed above.² uses the TELA to GBA translator of Spot, simplifies (using Spot’s postprocessor with preference Small) and degeneralizes the result and then determinizes using a version of Safra’s algorithm [14, 33]. The ${\text {removeFin}}$ function that is used is an optimized version of Definition 3.4. In , and , the first step is replaced by the corresponding TELA to GBA construction (using Spot’s ${\text {removeFin}}$). The product approach (also implemented using the Spot-library) is called product and product (no langcover) (without the langcover heuristic). The intermediate GBA are also simplified. The construction $\mathcal {G}^{{\text {LD}}}_{\mathcal {A}}$ is implemented in limit-det., using the Spot-library and parts of Seminator. We compare it to limit-det. via GBA, which concatenates the TELA to GBA construction of Spot with the limit-determinization of Seminator. Similarly, good-for-MDP and good-for-MDP via GBA are the construction $\mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}$ applied to $\mathcal {A}$ directly, or to the GBA as constructed by Spot. Both constructions via GBA are in the worst case double-exponential. No post-processing is applied to any output automaton.

Experiments. Computations were performed on a computer with two Intel E5-2680 CPUs with 8 cores each at $2.70$ GHz running Linux. Each individual experiment was limited to a single core, 15 GB of memory and 1200 s. We use versions 2.9.4 of Spot (configured to allow 256 acceptance sets) and 2.0 of Seminator.

Table 1. Evaluation of benchmarks random and DNF. Columns “States”, “Time” and “Acceptance” refer to the respective median values, where mem-/timeouts are counted as larger than the rest. Values in brackets refer to the subset of input automata for which at least one determinization needed more than 0.5 s (447 (182) automata for benchmark random (DNF)).

Our first benchmark set (called random) consists of 1000 TELA with 4 to 50 states and 8 sets of transitions $T_1, \ldots , T_8$ used to define the acceptance conditions. They are generated using Spot’s procedure random_graph() by specifying probabilities such that: a triple $(q,a,q') \in Q \times \varSigma \times Q$ is included in the transition relation (3/|Q|) and such that a transition t is included in a set $T_j$ (0.2). We use only transition systems that are nondeterministic. The acceptance condition is generated randomly using Spot’s procedure acc_code::random(). We transform the acceptance condition to DNF and keep those acceptance conditions whose lengths range between 2 and 21 and consist of at least two disjuncts. To quantify the amount of nondeterminism, we divide the number of pairs of transitions of the form $(q,a,q_1),(q,a,q_2)$, with $q_1 \ne q_2$, of the automaton by its number of states.

Table 1 shows that the product produces smallest deterministic automata overall. Spot produces best results among the algorithms that go via a single GBA. One reason for this is that after GBA-simplifications of Spot, the number of acceptance marks of the intermediate GBA are comparable. Figure 4 (left) compares Spot and product and partitions the input automata according to acceptance complexity (measured in the size of their DNF) and amount of nondeterminism. Each subset of input automata is of roughly the same size (159–180) (see [21, Tab. 2]). The graph depicts the median of the ratio (product/ Spot) for the measured values. For time- or memouts of Spot (product) we define the ratio as 0 ($\infty$). If both failed, the input is discarded. The number of time- and memouts grows with the amount of nondeterminism and reaches up to 42%. The approach product performs better for automata with more nondeterminism and complex acceptance conditions as the results have fewer states and the computation times are smaller compared to Spot.

The limit-deterministic automata are generally much smaller than the deterministic ones, and limit-det via GBA. performs best in this category. However, the construction $\mathcal {G}^{{\text {LD}}}_{\mathcal {A}}$ (limit-det.) resulted in fewer time- and memouts.

For GFM automata we see that computing $\mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}$ directly, rather than first computing a GBA, yields much better results (good-for-MDP vs. good-for-MDP via GBA). However, the GFM automata suffer from significantly more time- and memouts than the other approaches. The automata sizes are comparable on average with Spot’s determinization (see [21, Fig. 7]). Given their similarity to the pure limit-determinization constructions, and the fact that their acceptance condition is much simpler than for the deterministic automata, we believe that future work on optimizing this construction could make it a competitive alternative for probabilistic model checking using TELA.

Fig. 4.

Comparison of Spot and product, with input automata grouped by the size of the DNF of their acceptance condition and the amount of nondeterminism.

The second benchmark (called DNF) consists of 500 TELA constructed randomly as above, apart from the acceptance conditions. They are in DNF with 2–3 disjuncts, with 2–3 ${{\text {Inf}}}$-atoms and 0–1 ${{\text {Fin}}}$-atoms each (all different). Such formulas tend to lead to larger CNF conditions, which benefits the new approaches. Figure 4 (right) shows the median ratio of automata sizes, computation times and acceptance sizes, grouped by the amount of nondeterminism. We do not consider different lengths of acceptance conditions because the subsets of input automata are already relatively small (140–193). Again, product performs better for automata with more nondeterminism.

7 Conclusion

We have introduced several new approaches to determinize and limit-determinize automata under the Emerson-Lei acceptance condition. The experimental evaluation shows that in particular the product approach performs very well. Furthermore, we have shown that the complexity of limit-determinizing TELA is single-exponential (in contrast to the double-exponential blow-up for determinization). One of our constructions produces limit-deterministic good-for-MDP automata, which can be used for quantitative probabilistic verification.

This work leads to several interesting questions. The presented constructions would benefit from determinization procedures for GBA which trade a general acceptance condition (rather than Rabin or parity) for a more compact state-space of the output. Similarly, translations from LTL to compact, nondeterministic TELA would allow them to be embedded into (probabilistic) model-checking tools for LTL (a first step in this direction is made in [27]). It would be interesting to study, in general, what properties can be naturally encoded directly into nondeterministic TELA. Another open point is to evaluate the good-for-MDP automata in the context of probabilistic model checking in practice.