From Emerson-Lei automata to deterministic, limit-deterministic or good-for-MDP automata

Three new translations from TELA to GBA are proposed, and an example is given in which they perform exponentially better than state-of-the-art implementations. We demonstrate how they can be used to build novel determinization approaches for TELA. The determinization procedures are based on a product construction which combines multiple GBA. Our experiments show that this approach often outperforms approaches based on determinizing a single GBA. 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). We show that deciding whether \(\textbf{Pr}^{\max }_{\mathscr {M}}(\mathscr {L}(\mathscr {A})) > 0\) holds is NP-complete if the TELA \(\mathscr {A}\) is limit-deterministic, and in P if the acceptance of \(\mathscr {A}\) is fin-less (Proposition 5.3). Finally, a limit-determinization construction for TELA based on the breakpoint-construction is presented. We show that a version of this procedure yields good-for-MDP Büchi automata (Definition 5.4). Thereby \(\textbf{Pr}^{\max }_{\mathscr {M}}(\mathscr {L}(\mathscr {A}))\) is computable in single-exponential time for any MDP \(\mathscr {M}\) and TELA \(\mathscr {A}\) (Theorem 5.3). The experimental evaluation compares the performance of the different constructions using three benchmark sets.

This article is an extended version of the conference paper [26] which provides full proofs (including some technical lemmas which were omitted in the conference version) and further examples. The experiments are also extended to an additional benchmark set.

The upper-bound for determinization of TELA [40, 41] relies on a translation to GBA which first transforms the acceptance formula into disjunctive normal form (DNF). We refine this idea by discussing and comparing several ways of performing this transformation. In particular, we present different strategies to remove \({{\text {Fin}}}\)-atoms from the acceptance formula, which is a necessary ingredient of the approach. The removal of Fin-atoms is also discussed in [17, Sect. 4.5], together with a transformation into Büchi automata which relies on computing the conjunctive normal form of the acceptance formula after removing Fin-atoms. Our fin-removal strategies build on the ideas of [17], but our transformation to GBA avoids the CNF conversion and therefore sometimes produces exponentially smaller automata. Furthermore, we extend it to produce limit-deterministic automata. Translations from LTL to TELA have been proposed in [9, 32, 35], 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, 10, 12, 19], 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 [10, 12] is equivalent to the DNF that we use and it is a special case of the hyper-Rabin condition for which the emptiness problem is in P [11, 20]. Probabilistic model checking for deterministic automata under this condition is considered in [12], while [10] is concerned with standard emptiness while allowing nondeterminism. In contrast to the above works, we consider probabilistic model checking for nondeterministic automata under general Emerson-Lei conditions. A procedure to transform TELA into parity automata is presented in [39], but it does not guarantee the output to be deterministic.

The first limit-determinization procedure for nondeterministic Büchi automata was presented in [14, 15], and it relies on the idea of combining a copy of the automaton with its breakpoint automaton. This idea was also used in [7, 23]. We lift it to Emerson-Lei automata by using multiple different breakpoint automata, corresponding to different parts of the Emerson-Lei condition.

After the preliminaries in Section 2, we present the new translation approaches to construct GBA in Sect. 3. In Sect. 4, we show how to use them to determinize TELA and introduce the determinization based on a product construction. The translations to limit-deterministic TELA and good-for-MDP automata are contained in Sect. 5. Finally, we compare the different approaches in our experimental evaluation in Sect. 6 before we conclude the paper in Sect. 7.

A transition-based Emerson-Lei automaton (TELA) \(\mathscr {A}\) is a tuple \((Q, \Sigma , \delta , I, \alpha )\), where Q is a finite set of states, \(\Sigma \) is a finite alphabet, \(\delta \subseteq Q \times \Sigma \times Q\) is the transition relation, \(I \subseteq Q\) is the set of initial states and \(\alpha \) is a symbolic acceptance condition over \(\delta \), defined by:If \(\alpha \) is , , \({{\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 \(\mathscr {A}\) for an infinite word \(u = u_0 u_1 \ldots \in \Sigma ^\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 \)) \({{\,\textrm{iff }\,}}\) \(\inf (\rho ) \models \alpha \). The language of \(\mathscr {A}\), denoted by \(\mathscr {L}(\mathscr {A})\), is the set of all words for which there exists an accepting run of \(\mathscr {A}\). The sets of infinite words which are the language of some TELA are called \(\omega \)-regular. A TELA \(\mathscr {A}\) is deterministic if the set of initial states contains exactly one state and the transition relation is a function \(\delta : Q \times \Sigma \rightarrow Q\). It is complete, if for all \((q,a) \in Q \times \Sigma \): \(\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))\)).

A labeled Markov decision process (MDP) \(\mathscr {M}\) is a tuple \((S,s_0,{\text {Act}},P,\Sigma ,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 \Sigma \) is a labeling function of the states into a finite alphabet \(\Sigma \). 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 \(\mathscr {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 \(\mathscr {M}\) is denoted by \({\text {Paths}}(\mathscr {M})\) and \({\text {Paths}}_{{\text {fin}}}(\mathscr {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 \Sigma ^{\omega }\).

A Markov chain is an MDP with \(|{\text {Act}}(s)| \le 1\) for all states s. A scheduler of \(\mathscr {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 \(\mathscr {M}_{\mathfrak {S}}\) and thereby a probability measure over \({\text {Paths}}(\mathscr {M})\). The probability of a set of paths \(\Pi \) starting in \(s_0\) under this measure is \(\Pr _\mathscr {M}^{\mathfrak {S}}(\Pi )\). For an \(\omega \)-regular property \(\Phi \subseteq \Sigma ^{\omega }\) we define \(\textbf{Pr}^{\max }_{\mathscr {M}}(\Phi ) = \sup _{\mathfrak {S}}\Pr _{\mathscr {M}}^{\mathfrak {S}}(\{\pi \mid \pi \in {\text {Paths}}(\mathscr {M}) \text { and } L(\pi ) \in \Phi \})\). We denote by \(\Pr ^{\mathfrak {S}}_{\mathscr {M},s}(\Phi )\) and \(\textbf{Pr}^{\max }_{\mathscr {M},s}(\Phi )\) the corresponding values in the MDP one gets by setting the initial state in \(\mathscr {M}\) to \(s \in S\), and omit the \(\mathscr {M}\) in the subscript if it is clear from the context. In a Markov chain, which has a unique scheduler, we omit the superscripts. We refer to [3, Chapter 10] for more details.

The first operator splits a TELA along the top-level disjuncts of its acceptance condition. Let \(\mathscr {A} = (Q, \Sigma , \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}}(\mathscr {A}) := (\mathscr {A}_1, \ldots , \mathscr {A}_m)\) with \(\mathscr {A}_i = (Q, \Sigma , \delta , I, \alpha _i)\) for \(1 \le i \le m\), and \({\text {split}}(\mathscr {A})[i]{:}{=} \mathscr {A}_i\).

The analogous statement does not hold for conjunction and intersection (see Example 3.1). In other words, the intersection of languages of automata one gets by splitting along a top-level conjunction is not necessarily the language of the original automaton. This is because a conjunctive acceptance formula requires the existence of a run satisfying all conjuncts.

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 [17] and similar constructions are used in [32, 35]. While the sum operations yield smaller automata in general, only the product construction preserves determinism.

Note, that the acceptance \(\alpha _{GBA}\) contains the same number of atomic acceptance conditions as \(\mathscr {A}_0\) and \(\mathscr {A}_1\), i.e. the acceptance condition does not increase when \(\oplus _{GBA}\) is used to combine two GBA.

The additional \({{\text {Inf}}}(\delta _0)\) and \({{\text {Inf}}}(\delta _1)\) atoms in the acceptance condition of \(\mathscr {A}_0 \oplus \mathscr {A}_1\) are essential (see Example 3.2).

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 [10, 12]).

A single \({{\text {Fin}}}\) atom in each disjunct is enough because \({{\text {Fin}}}(T_1) \wedge {{\text {Fin}}}(T_2) \equiv _{\delta } {{\text {Fin}}}(T_1 \cup T_2)\) holds for all \(T_1,T_2,\delta \). Taking \(k_i \ge 1\) is also no restriction, as we can 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 |}\) and each disjunct contains at most \(|\beta |\) atomic acceptance conditions.

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 [42]. For a TELA \(\mathscr {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.

Another way to determinize a TELA \(\mathscr {A}\) in DNF is to determinize the automata \({\text {split}}(\mathscr {A})[i]\) one by one and then combining them with the disjunctive product construction of Definition 3.1:where “\({\text {det}}\)” is any GBA-determinization procedure. Let \({\mathscr {B}}\) be a TELA with acceptance \(\beta \) and n states, and let \(\alpha \) be an equivalent condition in DNF with m disjuncts. Then, for all the automata \({\text {removeFin}}({\text {split}}(\mathscr {A})[i])\), the number of states is bounded by O(n) and the number of acceptance sets of the GBA conditions is bounded by \(O(\beta )\). Assuming an optimal GBA-determinization procedure, the product combines m automata with \(2^{O(n (\log n + \log |\beta |))}\) states and hence the result has \(\big (2^{O(n \, (\log n + \log |\beta |))}\big )^m = 2^{O ( 2^{|\beta |} \cdot n (\log n + \log |\beta |))}\) states.

Let \(\mathscr {A} = (Q,\Sigma ,\delta ,I,\bigvee _{1 \le i \le m} \alpha _i)\) be a fixed TELA in DNF for the entire section, where \(\alpha _i = {{\text {Fin}}}(T^i_0) \wedge \bigwedge _{1 \le j \le k_i} {{\text {Inf}}}(T^i_j)\) for \(1 \le i \le m\). Additionally, define \(\mathscr {A}_i = {\text {split}}(\mathscr {A})[i]\). Replacing the product by a sum in the product-based determinization of the last section yields single exponential limit-deterministic automata (in contrast to the double-exponential lower-bound for determinization).

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 [15] (for Büchi automata) and [6, 7, 23] (for GBA) to Emerson-Lei conditions in DNF. These constructions use an initial component and an accepting breakpoint component [33] for \(\mathscr {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 \(\mathscr {A}\) without considering the \({{\text {Fin}}}\)-transitions of that disjunct. We will use the subset transition function \(\theta \) associated with \(\delta \), defined by: \(\theta (P,a) = \bigcup _{q \in P}\{ q' \mid (q,a,q') \in \delta \}\) for \((P,a) \in 2^Q \times \Sigma \), 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. The following definitions refer to the fixed automaton \(\mathscr {A}\) as defined in the beginning of the section.

In a state (R, B, l) of the above construction, intuitively R is the set of states reachable for the word seen so far in \(\mathscr {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 standard breakpoint construction underapproximates the language of a given GBA, in general.

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

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

Before giving a proof of Theorem 5.1 we prove two lemmas related to the breakpoint construction, which will be necessary for the correctness part of Theorem  5.1. The functions \(\theta \) and \(\theta _i\) are defined as in Definition  5.3.

The proofs of the lemmas follow known arguments for the correctness of limit-determinization for Büchi and generalized Büchi automata (see [15, Sect. 4.2] and [6, Sects. 7.4 and 7.6]). Still, the extension to Emerson-Lei requires additional arguments and hence we give the proofs here in our notation for completeness. The first lemma extends [6, Lemma 7.1].

The following lemma shows one direction of the correctness part of Theorem 5.1.

Now we are in a position to prove Theorem 5.1. The last part of the proof follows the proof of [6, Lemma 7.2].

As a direct corollary of Theorem  5.1 we get that TELA can be transformed into LDBA of single-exponential size.

This section discusses how the above constructions can be used for probabilistic model checking. We will use a product between an MDP \(\mathscr {M}\) and a nondeterministic automaton \(\mathscr {A}\) which was introduced in [28]. The construction is such that schedulers of the MDP are forced to resolve the nondeterminism of \(\mathscr {A}\) by choosing the next state of the automaton. We assume that the automaton used to build the product has a single initial state, which holds for \(\mathscr {G}^{{\text {GFM}}}_\mathscr {A}\).

We define the accepting paths \(\Pi _{acc}\) of \(\mathscr {M}\times \mathscr {G}\) to be:As a first application, consider the qualitative model checking problem which asks to decide \(\textbf{Pr}^{\max }_{\mathscr {M}}(\mathscr {L}(\mathscr {A})) > 0\), under the assumption that \(\mathscr {A}\) is a limit-deterministic TELA. While NP-hardness follows from the fact that the problem is already hard for deterministic TELA [34, 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 [15], and our proof uses similar arguments.

Our next aim is to show that the maximal probability in an MDP to satisfy a property specified as a TELA can be computed in single-exponential time. As a means to this end we will show that the automaton \(\mathscr {G}^{{\text {GFM}}}_\mathscr {A}\), as defined in Definition  5.4, is good-for-MDP (GFM) [24]. As before, we start with a TELA \(\mathscr {A} = (Q,\Sigma ,\delta ,I,\bigvee _{1 \le i \le m} \alpha _i)\) in DNF, with \(\alpha _i = {{\text {Fin}}}(T^i_0) \wedge \bigwedge _{1 \le j \le k_i} {{\text {Inf}}}(T^i_j)\) for \(1 \le i \le m\).

The GFM-property is defined using the product construction introduced above (Definition 5.5). A Büchi automaton \(\mathscr {G}\) is called good-for-MDP (GFM) iff \(\textbf{Pr}^{\max }_{\mathscr {M}}(\mathscr {L}(\mathscr {G})) = \textbf{Pr}^{\max }_{\mathscr {M}\times \mathscr {G}}(\Pi _{acc})\) holds for all MDP \(\mathscr {M}\) [24]. The inequality “\(\ge \)” holds for all automata [28, Thm. 1], but the other direction requires, intuitively, that a scheduler on \(\mathscr {M}\times \mathscr {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 [28]. Limit-deterministic Büchi automata are not GFM in general, for example, \(\mathscr {G}^{{\text {LD}}}_{\mathscr {A}}\) may not be (see Example 5.1).

The proof proceeds by fixing an arbitrary MDP \(\mathscr {M}\) and showing that \(\textbf{Pr}^{\max }_{\mathscr {M}}(\mathscr {L}(\mathscr {A})) \le \textbf{Pr}^{\max }_{\mathscr {M}\times \mathscr {G}^{{\text {GFM}}}_\mathscr {A}}(\Pi _{acc})\). To this end it is enough to show that for any finite-memory scheduler \(\mathfrak {S}\) on \(\mathscr {M}\) one finds a scheduler \(\mathfrak {S'}\) on \(\mathscr {M}\times \mathscr {G}^{{\text {GFM}}}_\mathscr {A}\) such that \(\Pr ^{\mathfrak {S}}_{\mathscr {M}}(\mathscr {L}(\mathscr {A})) \le \Pr ^{\mathfrak {S}'}_{\mathscr {M}\times \mathscr {G}^{{\text {GFM}}}_\mathscr {A}}(\Pi _{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, Sects. 10.6.3 and 10.6.4].

To define \(\mathfrak {S}'\) we analyze the behaviour of \(\mathfrak {S}\) in the product \(\mathscr {M}\times \mathscr {D}\) of \(\mathscr {M}\) with a specific deterministic automaton \(\mathscr {D}\) for \(\mathscr {L}(\mathscr {A})\), which we introduce later. In particular, we show that for each accepting bottom strongly connected component B of the induced Markov chain of \(\mathscr {M}\times \mathscr {D}\) under \(\mathfrak {S}\) there exists an accepting breakpoint component \(\mathfrak {B}_i\) such that, with probability one, words generated by B are accepted by \(\mathfrak {B}_i\). To show this, we first prove a sufficient condition for a word to be accepted by \(\mathfrak {B}_i\).

Recall that \({\text {removeFin}}({\text {split}}(\mathscr {A})[i])\) is a GBA with two components: the initial component \(Q_1\) is a copy of \(\mathscr {A}\) where no transition is accepting, and component \(Q_2\) is a copy of \(\mathscr {A}\) without the transitions of \(T_0^i\). The acceptance condition is the GBA condition \(\bigwedge _{1 \le j \le k_i} {{\text {Inf}}}(U_{j}^i)\) where \(U_j^i\) is the set of transitions corresponding to \(T_j^i \setminus T_0^i\) in the component \(Q_2\).

Now let \(\mathscr {D}_i = {\text {det}}({\text {removeFin}}({\text {split}}(\mathscr {A})[i]))\) be the Rabin automaton one gets by applying the construction of [42] to \({\text {removeFin}}({\text {split}}(\mathscr {A})[i])\). Their soundness-proof [42, Thm. 1] can be modified slightly to prove the following statement, where \(\gamma \) is the extended subset transition function of \({\text {removeFin}}({\text {split}}(\mathscr {A})[i])\). It shows that an accepting lasso-path through \(\mathscr {D}_i\) induces a special path through the powerset automaton of \({\text {removeFin}}({\text {split}}(\mathscr {A})[i])\). As a consequence, the corresponding word is accepted by \({\text {removeFin}}({\text {split}}(\mathscr {A})[i])\). Furthermore, the word labeling the loop of the lasso satisfies a condition which matches the one of Lemma 5.4, and hence is accepted by \(\mathfrak {B}_i\).

The above lemmas give a sufficient condition for a word to be accepted by \(\mathfrak {B}_i\) (Lemma 5.4), and show that words labeling a loop in the deterministic automaton \(\mathscr {D}_i\) induce a path through the powerset automaton of \({\text {remove\,\,Fin}}({\text {split}}(\mathscr {A})[i])\) (Lemma 5.5). Now, we show how these facts can be used to construct the scheduler \(\mathfrak {S}'\).

Recall that we are given a finite memory scheduler \(\mathfrak {S}\) of \(\mathscr {M}\) and to prove the GFM-property we have to provide a scheduler \(\mathfrak {S}'\) such that \(\Pr ^{\mathfrak {S}}_{\mathscr {M}}(\mathscr {L}(\mathscr {A})) \le \Pr ^{\mathfrak {S}'}_{\mathscr {M}\times \mathscr {G}^{{\text {GFM}}}_{\mathscr {A}}}(\Pi _{acc})\). Let \(\mathscr {M}_{\mathfrak {S}} \times \mathscr {D}\) be the product of the induced finite Markov chain \(M_{\mathfrak {S}}\) with \(\mathscr {D} = \bigotimes _{1 \le i \le m} \mathscr {D}_i\). The scheduler \(\mathfrak {S}'\) is constructed as follows. It stays inside the initial component of \(\mathscr {M}\times \mathscr {G}^{{\text {GFM}}}_{\mathscr {A}}\) and mimics the action chosen by \(\mathfrak {S}\) until the corresponding path in \(\mathscr {M}_{\mathfrak {S}} \times \mathscr {D}\) reaches an accepting bottom strongly connected component (BSCC) B. This means that the transitions of \(\mathscr {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 accepting breakpoint components \(\mathfrak {B}_{i}\) to which \(\mathfrak {S}'\) can safely move.

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

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

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

We compare the following implementations of the constructions discussed above.²Spot 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 [18, 38]. The \({\text {removeFin}}\) function that is used is an optimized version of Definition 3.3. If the input is a weak, Rabin or Street automaton, Spot uses dedicated algorithms instead of \({\text {removeFin}}\) to construct the GBA. In the constructions remFin\(\rightarrow \)split\(\alpha \), split\(\alpha \) \(\rightarrow \)remFin and remFin\(\rightarrow \)rewrite\(\alpha \), the first step is replaced by the corresponding TELA to GBA construction (using Spot’s function \({\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 \(\mathscr {G}^{{\text {LD}}}_{\mathscr {A}}\) is implemented in limit-det., using the Spot-library and parts of Seminator [8]. 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 \(\mathscr {G}^{{\text {GFM}}}_{\mathscr {A}}\) applied to \(\mathscr {A}\) directly, or to the GBA as constructed by Spot. Both constructions via GBA are in the worst case double-exponential. No post-processing, e.g. Spot’s postprocessor, is applied to any output automaton.

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 seconds. We use versions 2.9.4 of Spot (configured to allow 256 acceptance sets) and 2.0 of Seminator.

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 \Sigma \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 with common starting point and symbol (that is, 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 of about the same and Spot constructs GBA with fewer states. This difference in the number of states is expected, given the theoretical analysis in Sect. 3.2. The similarity of the numbers of acceptance marks is not supported by the theoretical analysis and can only be explained by Spot’s advanced GBA-simplification algorithms that might suit Spot ’s GBA better than the GBA constructed by the other approaches.

The limit-deterministic automata are in general much smaller than the deterministic ones, and limit-det via GBA. performs best in this category (see Fig. 6). However, the construction \(\mathscr {G}^{{\text {LD}}}_{\mathscr {A}}\) (limit-det.) resulted in fewer time- and memouts and, as shown in Fig. 6, it still produces for most cases outputs with fewer states than Spot .

For GFM automata we see that computing \(\mathscr {G}^{{\text {GFM}}}_{\mathscr {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 with Spot ’s determinization (see Fig. 6). 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.

We compare the two best performing determinization approaches, Spot and product, in more detail. Figure 6 shows that the results are widely spread, i.e. both approaches produce smaller results than the other one for a significant number of inputs. Figure 2 partitions the set of all 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). The number of timeouts and memouts increases with the amount of nondeterminism and the size of the input acceptance condition and reaches up to 42%. The values “states”, “time” and “acceptance” are the median value of the ratio of these metrics. If only one of the approaches was able to construct a result within the given time and memory bounds we define the ratio as 0 ( Spot did not construct a result) or infinity (product did not construct a result). If none of the approaches was able to construct a result, we do not consider this input automaton for the calculation. Values below 1 indicate that product produces smaller results and values above 1 indicate that Spot produces smaller results. The approach product produces for all subsets of input automata outputs with fewer states than Spot and the ratio of the computation time decreases the larger the amount of nondeterminism and the longer the acceptance condition is.

The second benchmark set (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. Table 1 shows that product produces way smaller results than Spot . Again, Table 2 partitions the set of input automata but we do not consider different lengths of acceptance conditions here because the subsets of input automata are already relatively small (140-193). Again, product performs better for automata with more nondeterminism.

The third benchmark set consists of the sequence of automata described in Fig. 4. Figure 7 shows the results for such input automata with 1-25 states. For these automata, Spot first computes GBA with an exponential number of acceptance sets. As a consequence most input automata lead to a time- or memout and, if the computation finishes, to large output automata. Therefore, our proposed alternative constructions can compute results for far larger input automata. The example also highlights the effect of the langcover heuristic: it benefits from the fact that the language of the input automaton under any individual disjunct of the DNF is the same. This is used to prune large parts of the state-space.