From LTL to deterministic automata

Abstract

We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula $\varphi$. The automaton is the product of a co-Büchi automaton for $\varphi$ and an array of Rabin automata, one for each ${\mathbf {G}}$-subformula of $\varphi$. The Rabin automaton for ${\mathbf {G}}\psi$ is in charge of recognizing whether ${\mathbf {F}}{\mathbf {G}}\psi$ holds. This information is passed to the co-Büchi automaton that decides on acceptance. As opposed to standard procedures based on Safra’s determinization, the states of all our automata have a clear logical structure, which allows for various optimizations. Experimental results show improvement in the sizes of the resulting automata compared to existing methods.

1 Introduction

Linear temporal logic (LTL) is the most popular language for the specification of properties of single computations of a program. The verification problem for LTL consists of deciding if all computations of a program satisfy a given LTL-formula formalizing a property. In the automata-theoretic approach to this problem [1,2,3], the negation of the formula is translated into an $\omega$-automaton, and the product of this automaton with the transition system describing the semantics of the program is analyzed. In particular, if this transition system—or some suitable abstraction of it—has a finite number of states, then the product can be exhaustively explored by a search algorithm, and the property can be checked automatically, at least in principle.

While the size of the $\omega$-automaton can be exponential or even double exponential in the length of the formula (depending on the kind of $\omega$-automaton), typical formulae used in practice are either small, or belong to classes for which this blowup does not happen. However, since the transition system is often very large, generating small $\omega$-automata is still crucial for the efficiency of the approach: Even a reduction of a few states in the $\omega$-automaton can lead to a much larger reduction in the product.

For functional LTL verification (as opposed to the probabilistic verification discussed in the next paragraph), verification algorithms only require to transform the LTL formula into a non-deterministic $\omega$-automaton, typically a Büchi or generalized Büchi automaton and, thanks to intense research in the last decade, the problem of generating small automata is well understood, e.g. [4,5,6]. Several tools implement a number of heuristic simplifications (of the formula, of intermediate automata generated during the translation, and of the final result), and generate Büchi automata of minimal or nearly minimal size for most common specifications, e.g. [7, 8]. An important factor for this success is the fact that the states of the automaton are LTL formulae, which allows one to use information about logical equivalence or implication between formulae to merge states.

The picture is still very different for quantitative LTL verification of probabilistic systems, i.e., for the problem of computing the probability with which an LTL property is satisfied, or deciding whether it exceeds a given bound. The standard approach to this problem requires to translate the LTL formula into a deterministic $\omega$-automaton [9, 10], typically a deterministic Rabin automaton (DRA). Contrary to the functional case, up to 2012 there were no algorithms providing a direct translation, all algorithms available proceeded in two steps: first, the formula was translated into a non-deterministic Büchi automaton (NBA), and then Safra’s construction [11]—or improvements on it [12, 13]—were applied to transform the NBA into a DRA. At the time of writing this paper this is also the default approach adopted in PRISM [14], a leading probabilistic model checker, which reimplements the optimized Safra’s construction of the ltl2dstar tool [15]. While Safra’s construction is a milestone of the theory of $\omega$-automata, it is also difficult to implement (see e.g. [16]). In particular, it is a monolithic construction that can be applied to any NBA, and therefore does not exploit the structure of LTL formulae.

In 2011 the second author initiated a research program for the design and implementation of a direct translation of LTL into deterministic $\omega$-automata that “bypasses” Safra’s construction. As a first result, a translation for the LTL fragment containing only the temporal operators ${\mathbf {F}}$ and ${\mathbf {G}}$ was presented in [17]. The translation yields a deterministic generalized Rabin automaton (DGRA), which can then be degeneralized into a standard DRA. Alternatively, a verification algorithm was proposed in [10], which does not require to degeneralize the DGRA into DRA, but uses directly DGRA, and exhibits the same worst-case complexity. In both cases much smaller automata were obtained for many formulae. (For instance, while the standard approach translates a conjunction of three fairness constraints into an automaton with over a million states, the algorithm of [17] yields a DRA with 462 states, and—when acceptance is defined on transitions—a DGRA with one single state.) Subsequently, the approach was extended to larger fragments of LTL containing the ${\mathbf {X}}$-operator and restricted appearances of ${\mathbf {U}}$ [18, 19]. However, a general algorithm remained elusive.

In this paper we present a novel approach that is able to handle full LTL. Although the worst-case complexity of our construction is worse than that of the traditional translation using Safra’s determinization (triple exponential vs. double exponential), our construction consistently produces smaller automata in all our benchmark sets. Moreover, our approach is compositional: the DGRA is obtained as a parallel composition of automata running in lockstep.¹ More specifically, the automaton for a formula $\varphi$ is the parallel composition of a co-Büchi automaton (a special case of DRA) and an array of DRAs, one for each ${\mathbf {G}}$-subformula of $\varphi$. Intuitively, the state of the co-Büchi automaton after reading a finite word corresponds to “the formula that remains to be fulfilled” (we say that the automaton monitors the remaining formula). For example, if $\varphi = (\lnot a \wedge {\mathbf {X}}a) \vee {\mathbf {X}}{\mathbf {X}}{\mathbf {G}}a$, then the remaining formula after reading $\emptyset \{a\}$ is ${\mathbf {tt}}$, and after reading $\{a\}$ it is ${\mathbf {X}}{\mathbf {G}}a$. In particular, if the automaton reaches the state ${\mathbf {tt}}$, it accepts.

If the co-Büchi automaton never reaches ${\mathbf {tt}}$, then it needs information from the DRAs to decide on acceptance. The DRA for a ${\mathbf {G}}$-subformula ${\mathbf {G}}\psi$ checks whether ${\mathbf {G}}\psi$ eventually holds, i.e., whether ${\mathbf {F}}{\mathbf {G}}\psi$ holds. Like the co-Büchi automaton, the DRA also monitors the remaining formula, but only partially: more precisely, it does not monitor any ${\mathbf {G}}$-subformula of $\psi$, because other DRAs are responsible for them. For instance, if $\psi = a \wedge {\mathbf {G}}b \wedge {\mathbf {G}}c$, then the DRA for ${\mathbf {G}}\psi$ checks ${\mathbf {F}}{\mathbf {G}}a$, and “delegates” checking ${\mathbf {F}}{\mathbf {G}}b$ and ${\mathbf {F}}{\mathbf {G}}c$ to other automata. Furthermore, and crucially, the DRA for ${\mathbf {G}}\psi$ may also provide the information that not only ${\mathbf {F}}{\mathbf {G}}\psi$, but a stronger formula ${\mathbf {F}}{\mathbf {G}}(\psi \wedge \psi ')$ holds. For example, the run of the DRA for ${\mathbf {G}}(a \vee {\mathbf {X}}c)$ on the word $c^\omega$ supplies the information that not only ${\mathbf {F}}{\mathbf {G}}(a \vee {\mathbf {X}}c)$, but also the stronger formula ${\mathbf {F}}{\mathbf {G}}((a \vee {\mathbf {X}}c) \wedge c)$ holds.

The acceptance condition of the full parallel composition is a disjunction over all possible subsets $\mathcal {G}$ of ${\mathbf {G}}$-subformulae, and all possible sets of stronger formulae ${{\mathcal {F}}}$ that the DRAs can check together. Intuitively, the parallel composition accepts a word w by means of the disjunct for $\mathcal {G}$ and ${{\mathcal {F}}}$ when w satisfies ${\mathbf {F}}\mathcal {G}$ (meaning that w satisfies ${\mathbf {F}}{\mathbf {G}}\psi$ for every ${\mathbf {G}}\psi \in \mathcal {G}$) and also ${{\mathcal {F}}}$. The co-Büchi automaton is in charge of checking the conditional property that if w satisfies ${\mathbf {F}}\mathcal {G}$ and ${{\mathcal {F}}}$, then it also satisfies $\varphi$.

A previous version of our compositional algorithm appeared in [20]. Since the construction was involved and had a number of corner cases, the third author mechanically verified it in the Isabelle theorem prover. The exercise revealed that, as expected, some minor corrections were necessary, but also exposed a more serious bug requiring a substantial change in a lemma. An analysis revealed that the smallest to us known formula for which the construction of [20] would have produced a wrong result is ${\mathbf {G}}({\mathbf {X}}a \vee {\mathbf {G}}{\mathbf {X}}b)$, which has a high chance of surviving a large amount of testing.

To summarize, in contrast to the traditional approaches our novel translation is (1) efficient in practice, (2) compositional, (3) preserves the logical structure of states, and (4) is proven correct in a theorem prover.

Related work There are many constructions translating LTL to NBA, e.g., [4,5,6,7,8, 21,22,23,24,25]. The one recommended by ltl2dstar and used in PRISM is LTL2BA [5]. The version of Safra’s construction described in [26], which includes a number of optimizations, has been implemented in ltl2dstar [15], and re-implemented in PRISM [14]. A comparison of LTL translators into deterministic $\omega$-automata can be found in [27].

Our compositional construction shares the idea of recursive use of automata with the construction of [28], where transducers for subformulae, called temporal testers, are composed. However, “testers are inherently non-deterministic” [28], whereas all our automata are deterministic.

Apart from LTL verification of probabilistic systems, Safra’s construction can also be applied as intermediate step to solve other problems, such as the LTL synthesis problem [29]. Bypassing Safra’s construction by means of “safraless approaches” to synthesis has been the subject of several papers [30,31,32].

Outline The paper is organized as follows: After Sect. 2, which introduces basic definitions about LTL and $\omega$-automata, the next four sections present LTL-to-DGRA constructions for increasingly general LTL fragments. As a warm-up, Sect. 3 considers the case of ${\mathbf {G}}$-free formulae. Section 4 considers the case of formulae ${\mathbf {F}}{\mathbf {G}}\varphi$, where $\varphi$ has no occurrence of ${\mathbf {G}}$. Loosely speaking, it gives the recipe to construct a single element of the array of DRAs. Section 5 then constructs a DGRA for an arbitrary formula ${\mathbf {F}}{\mathbf {G}}\varphi$ as an array of DRAs. Section 6 shows how to construct the co-Büchi automaton and the full parallel composition for an arbitrary formula. All four sections have the same structure. First, we obtain a logical characterization of the words that satisfy a formula of the corresponding fragment, and then derive the corresponding automaton from it.

The paper continues with Sect. 7, which describes some optimizations that reduce the number of states of the final DGRA, and the size of its acceptance condition. Section 8 contains some remarks about the worst-case complexity of our construction. Finally, Sect. 9 introduces Rabinizer, the tool implementing our construction, and presents a number of experimental results on different test suites of LTL formulae.

As mentioned above, the correctness proof of our construction has been mechanized using the Isabelle theorem prover. Section 10 shows how to access the mechanized proofs, and the relation between this paper and the formal proof. In particular, in the paper we sometimes omit cases in proofs by structural induction that do not provide special insight.

Finally, Sect. 11 presents our conclusions. Some technical proofs are presented in Appendix.

2 Basic definitions

We recall basic definitions of $\omega$-automata and linear temporal logic, and establish some notations.

In this paper, ${\mathbb {N}}$ denotes the set of natural numbers including zero. We say that a property holds for almost every $n \in \mathbb {N}$ if it holds for all but finitely many natural numbers.

2.1 Alphabets and words

An alphabet is any finite non-empty set $\varSigma$. The elements of $\varSigma$ are called letters. A word is an infinite sequence of elements of $\varSigma$. The set of all words is denoted by $\varSigma ^\omega$. A finite word is a finite sequence of elements of $\varSigma$, and the set of all finite words is denoted by $\varSigma ^*$.

The ith letter of a word $w\in \varSigma ^\omega$ is denoted by w[i], i.e. $w=w[0]w[1]\ldots$. Given $i, j \in \mathbb {N}$, we denote by $w_{ij}$ the finite word $w[i] w[i+1] \ldots w[j-1]$ if $i < j$, and the empty word if $j \le i$. We denote by $w_i$ the suffix $w[i] w[i+1] \ldots$.

A (finite or infinite) set of words is called a language.

2.2 Linear temporal logic

Linear temporal logic (LTL) extends propositional logic with temporal operators.

2.2.1 Syntax and semantics

Definition 1

(LTL Syntax) Let Ap be a finite set of atomic propositions. The formulae of linear temporal logic (LTL) over Ap are given by the syntax

$$\begin{aligned} \varphi {::=}\,&{\mathbf {tt}}\mid {\mathbf {ff}}\mid a \mid \lnot \varphi \mid \varphi \wedge \varphi \mid \varphi \vee \varphi \mid {\mathbf {X}}\varphi \mid {\mathbf {F}}\varphi \mid {\mathbf {G}}\varphi \mid \varphi {\mathbf {U}}\varphi \end{aligned}$$

where $a \in Ap$.

Formulae are interpreted on words over the alphabet $2^{Ap}$. That is, a letter is a subset of Ap.

Definition 2

(LTL Semantics) The satisfaction relation $\models$ between words and formulae is inductively defined as follows:

Given two formulae $\phi , \psi$, we say that $\phi$ entails $\psi$, denoted by $\phi \models \psi$, if $w \models \phi$ implies $w \models \psi$ for every $w\in (2^{Ap})^\omega$. We say that $\phi$ and $\psi$ are equivalent, denoted by $\phi \equiv \psi$, if $\phi \models \psi$ and $\psi \models \phi$.

2.2.2 Negation normal-form

In LTL negations can be “pushed inwards”; for instance, we have $\lnot {\mathbf {F}}{\mathbf {G}}a \equiv {\mathbf {G}}\lnot {\mathbf {G}}a \equiv {\mathbf {G}}{\mathbf {F}}\lnot a$. By pushing negations inwards until all negations appear only in front of atomic propositions, we obtain the negation normal form:

Definition 3

(Negation normal form) A formula of LTL is in negation normal form if it is given by the syntax:

$$\begin{aligned} \varphi {::=}\,&{\mathbf {tt}}\mid {\mathbf {ff}}\mid a \mid \lnot a \mid \varphi \wedge \varphi \mid \varphi \vee \varphi \mid {\mathbf {X}}\varphi \mid {\mathbf {F}}\varphi \mid {\mathbf {G}}\varphi \mid \varphi {\mathbf {U}}\varphi \end{aligned}$$

where $a \in Ap$.

Proposition 1

(Normal form theorem) Every formula of LTL is equivalent to a formula in negation normal form.

Proof

Exhaustive application of the following well-known rewrite rules (which replace a formula by an equivalent one) brings every formula in negation normal form:

$$\begin{aligned} \lnot {\mathbf {X}}\varphi \leadsto {\mathbf {X}}\lnot \phi , \ \lnot {\mathbf {F}}\varphi \leadsto {\mathbf {G}}\lnot \phi , \ \lnot {\mathbf {G}}\varphi \leadsto {\mathbf {F}}\lnot \phi , \ \lnot (\varphi {\mathbf {U}}\psi ) \leadsto (\lnot \psi {\mathbf {U}}(\lnot \psi \wedge \lnot \varphi )) \vee {\mathbf {G}}\lnot \psi . \end{aligned}$$

$\square$

Observe that, due to the last rule, the formula obtained by exhaustive rewriting can be exponentially longer than the original formula. However, if the formula is stored as a DAG (directed acyclic graph) instead of a tree, then the DAG of the formula in negation normal form is only linearly larger than the DAG of the original formula.

In the rest of the paper we assume that formulae of LTL are in negation normal form, and speak of “a formula” instead of “a formula in negation normal form”.

2.2.3 Propositional entailment, equivalence, and substitution

Loosely speaking, given two formulae $\varphi$ and $\psi$, we say that $\varphi$ propositionally entails $\psi$ if $\varphi \models \psi$ can be proved using only propositional reasoning. So, for instance, ${\mathbf {G}}a$ propositionally implies ${\mathbf {G}}a \vee {\mathbf {G}}b$, but ${\mathbf {G}}a$ does not propositionally imply ${\mathbf {F}}a$.

Definition 4

(Propositional implication and equivalence) A formula of LTL is proper if it is not a conjunction or a disjunction (i.e., if the root of its syntax tree is not $\wedge$ or $\vee$). The set of proper formulae of LTL over Ap is denoted by PF(Ap). A propositional assignment, or just an assignment, is a mapping ${{\mathcal {A}}} :PF(Ap) \rightarrow \{0, 1\}$. Given $\varphi \in PF(Ap)$, we write ${{\mathcal {A}}} \models \varphi$ iff ${{\mathcal {A}}}(\varphi ) = 1$, and extend the relation $\models _P$ to arbitrary formulae by:

We say that $\varphi$ propositionally entails $\psi$, denoted by $\varphi \models _P \psi$, if ${{\mathcal {A}}} \models _P \varphi$ implies ${{\mathcal {A}}} \models _P \psi$ for every assignment ${{\mathcal {A}}}$. Finally, $\varphi$ and $\psi$ are propositionally equivalent, denoted by $\varphi \equiv _P \psi$, if $\varphi \models _P \psi$ and $\psi \models _P \varphi$. We denote by $[\varphi ]_P$ the equivalence class of $\varphi$ under the equivalence relation $\equiv _P$. (Observe that $\varphi \equiv _P \psi$ implies $\varphi \equiv \psi$ holds.)

Definition 5

(Propositional substitution) Let $\psi ,\chi$ be formulae, and let $\Psi$ be a set of proper LTL-formulae. The formula $\psi [\Psi / \chi ]_P$ is inductively defined as follows:

• If $\psi = \psi _1 \wedge \psi _2 \quad$ then $\psi [\Psi / \chi ]_P = \psi _1[\Psi /\chi ]_P \wedge \psi _2[\Psi / \chi ]_P$.

• If $\psi = \psi _1 \vee \psi _2 \quad$ then $\psi [\Psi / \chi ]_P = \psi _1[\Psi /\chi ]_P \vee \psi _2[\Psi / \chi ]_P$.

• If $\psi$ is a proper formula and $\psi \in \Psi$ then $\psi [\Psi / \chi ]_P = \chi$, else $\psi [\Psi / \chi ]_P = \psi$.

2.2.4 The after function ${ af}(\varphi , w)$

Given a formula $\varphi$ and a finite word w, we define a formula ${ af}(\varphi ,w)$, read “$\varphi$ after w”. Intuitively, if a word $ww'$ (where w is a finite word) satisfies $\varphi$, then ${ af}(\varphi ,w)$ is the formula that holds “after having read w”, that is, the formula satisfied by $w'$. As shown in Proposition 2 below, the converse also holds: if $w'$ satisfies ${ af}(\varphi ,w)$, then $ww'$ satisfies $\varphi$.

Definition 6

Let $\varphi$ be a formula and $\nu \in 2^{Ap}$. We define the formula ${ af}(\varphi ,\nu )$ as follows:

We extend the definition to finite words: ${ af}(\varphi , \epsilon ) = \varphi$; and ${ af}(\varphi , \nu w) = { af}({ af}(\varphi ,\nu ),w)$ for every $\nu \in 2^{Ap}$ and every finite word w. Finally, we say that $\psi$ is reachable from $\varphi$ if $\psi = { af}(\varphi ,w)$ for some finite word w.

Example 1

Let $Ap = \{a,b,c\}$ and $\varphi = a \vee (b \; {\mathbf {U}}\; c)$. We have ${ af}(\varphi , \{a\}) = {\mathbf {tt}}$ ${ af}(\varphi , \{b\}) = (b \; {\mathbf {U}}\; c)$, ${ af}(\varphi , \{c\}) = {\mathbf {tt}}$, and ${ af}(\varphi , \emptyset ) = {\mathbf {ff}}$.

We collect a number of simple properties of ${ af}$, proved in the Appendix.

Lemma 1

For every formula $\varphi$ and every finite word $w \in (2^{Ap})^*$:

• (1) ${ af}(\varphi , w)$ is a boolean combination of proper subformulae of $\varphi$.

• (2) If ${ af}(\varphi , w) = {\mathbf {tt}}$, then ${ af}(\varphi , ww') = {\mathbf {tt}}$ for every $w' \in (2^{Ap})^*$, and analogously for ${\mathbf {ff}}$.

• (3) If $\varphi _1 \equiv _P \varphi _2$, then ${ af}(\varphi _1, w) \equiv _P { af}(\varphi _2, w)$.

• (4) If $\varphi$ has n proper subformulae, then the set of formulae reachable from $\varphi$ has at most $2^{2^n}$ equivalence classes of formulae with respect to propositional equivalence.

Observe that, by Lemma 1(3), the function ${ af}$ can be lifted to equivalence classes of formulae w.r.t. propositional equivalence. Abusing language, we also denote this lifted function by ${ af}$.

We now state the fundamental property of the After function, also proved in the Appendix: a word $ww'$ satisfies a formula $\varphi$ iff “after reading” w the “rest” of the word, i.e., the word $w'$, satisfies ${ af}(\varphi ,w)$.

Proposition 2

Let $\varphi$ be a formula, and let $ww' \in (2^{Ap})^\omega$ be an arbitrary word. Then $ww' \models \varphi$ iff $w' \models { af}(\varphi ,w)$.

2.3 Transition systems and $\omega$-automata

A deterministic transition system (DTS) over an alphabet $\varSigma$ is a tuple ${{\mathcal {T}}}=(Q, \varSigma , \delta , q_0)$ where Q is a set of states, $\varSigma$ is an alphabet, $\delta :Q \times \varSigma \rightarrow Q$ is a transition function, and $q_0 \in Q$ is the initial state. If $\delta (q, a) = q'$ then we call the triple $t=(q, a, q')$ a transition, and say that q, a, and $q'$ are the source, the letter, and the target of t. We denote by T the set of transitions of $\mathcal{T}$.

A run of ${{\mathcal {T}}}$ is an infinite sequence $\rho = t_0 t_1 \ldots$ of transitions such that the source of $t_0$ is the initial state $q_0$, and for every $i \ge 0$ the target of $t_i$ is equal to the source of $t_{i+1}$. A transition t occurs in $\rho$ if $t = t_i$ for some $i \ge 0$. A state q occurs in $\rho$ if it is the source or target of some $t_i$. Given a word $w = a_0a_1 \ldots \in \varSigma ^\omega$, we denote by $\rho (w)$ the unique run $t_0 t_1 t_2\ldots$ of ${{\mathcal {T}}}$ such that for every $i \ge 0$ the letter of $t_i$ is $a_i$.

The product of two DTSs ${{\mathcal {T}}}_1=(Q_1, \varSigma , \delta _1, q_{01})$ and ${{\mathcal {T}}}_2=(Q_2, \varSigma , \delta _2, q_{02})$ is the DTS ${{\mathcal {T}}}_1 \times {{\mathcal {T}}_2}= (Q, \varSigma , \delta , q_0)$, where $Q = Q_1 \times Q_2$, $\delta ((q_1, q_2), a) = (\delta _1(q_1,a), \delta (q_2, a))$ for every $q_1 \in Q_1, q_2 \in Q_2, a \in \varSigma$, and $q_0 = (q_{01},q_{02})$.

2.3.1 Acceptance conditions and $\omega$-automata

A state-based acceptance condition for ${{\mathcal {T}}}$ is a positive boolean formula over the formal variables $V_Q=\{{\textit{Inf}}(S), {\textit{Fin}}(S) \mid S \subseteq Q \}$. Acceptance conditions are interpreted over runs. Given a run $\rho$ of ${{\mathcal {T}}}$ and an acceptance condition $\alpha$, we consider the truth assignment that sets the variable $\textit{Inf}(S)$ to true iff $\rho$ visits (some state of) S infinitely often, and sets $\textit{Fin}(S)$ to true iff $\rho$ visits (all states of) S finitely often. The run $\rho$ satisfies $\alpha$ if this truth-assignment makes $\alpha$ true. The size of a condition $\alpha$ is its length as boolean formula.

A transition-based acceptance condition for ${{\mathcal {T}}}$ is defined exactly as a state-based acceptance condition, but replacing the set $V_Q$ by the set $V_T = \{\textit{Inf}(U), \textit{Fin}(U) \mid U \subseteq T \}$. In this paper we use state-based or transition-based acceptance conditions, depending on what is more convenient. It is well-known that a state-based conditions can be transformed into an equivalent transition-based one (i.e., a condition satisfied by the same runs). It suffices to replace each occurrence of $\textit{Inf}(S)$ by $\textit{Inf}({}^\bullet S)$, where ${}^\bullet S$ denotes the set of transitions with target in S, and similarly for $\textit{Fin}(S)$. Conversely, a transition-based condition can also be transformed into an equivalent state-based one by replicating the states. Given a DTS ${{\mathcal {T}}}=(Q, \varSigma , \delta , q_0)$ with a set T of transitions we construct the new DTS $\mathcal{T}'$ with states $\{q_0\} \cup T$, a transition $(q_0, a, t)$ for every transition $t = (q_0, a, q)$ of T, and a transition $(t, a, t')$ for every pair $t=(q_1, a, q_2)$ and $t'=(q_2, b, q_3)$ of transitions of T. Then, the condition over the transitions of ${{\mathcal {T}}}$ becomes an equivalent condition over the states of $\mathcal{T}'$.

A deterministic $\omega$-automaton over $\varSigma$ is a tuple $\mathcal {A}= (Q, \varSigma , \delta , q_0, \alpha )$, where $(Q, \varSigma , \delta , q_0)$ is a deterministic transition system and $\alpha$ is an acceptance condition. $\mathcal {A}$ accepts a word $w \in \varSigma ^*$ if the run $\rho (w)$ satisfies $\alpha$. The language of $\mathcal {A}$, denoted by $\mathsf {L}(\mathcal {A})$, is the set of words accepted by $\mathcal {A}$.

An acceptance condition $\alpha$ is a

• Büchi condition if $\alpha = \textit{Inf}(S)$ for some $S \subseteq Q$.

• co-Büchi condition if $\alpha =\textit{Fin}(S)$ for some $S \subseteq Q$.

• Rabin condition if $\alpha = \bigvee _{j=1}^n ( \textit{Fin}(F_j) \wedge \textit{Inf}(I_j))$ for sets $F_1, I_1, \ldots , F_n, I_n \subseteq Q$. The pair $P_j = (F_j, I_j)$ is called a Rabin pair.

• generalized Rabin condition if $\alpha = \bigvee _{j=1}^n ( \textit{Fin}(F_j) \wedge \bigwedge _{k=1}^{m_j} \textit{Inf}(I_{jk}))$ for sets $F_1, \ldots , F_n, I_{11}, \ldots , I_{n m_n} \subseteq Q$.

A deterministic Büchi, co-Büchi, Rabin or generalized Rabin automaton is a deterministic $\omega$-automaton with an acceptance condition of the corresponding kind. In the rest of the paper we shorten deterministic Rabin automaton to DRA, and the generalized version to DGRA.

Observe that Büchi and co-Büchi conditions are special cases of Rabin conditions. Further, every generalized Rabin automaton can be degeneralized into an equivalent Rabin automaton, which however may incur an exponential blowup [17]. The generalized Rabin condition arises naturally when considering intersection of Rabin automata. Observe that we do not need to consider $\bigwedge _{k=1}^{\ell _j} \textit{Fin}(F_{jk})$, but only $\textit{Fin}(F_j)$, because $\bigwedge _{k=1}^{n_j} \textit{Fin}(F_{jk})$ is equivalent to $\textit{Fin}(\bigcup _{k=1}^{\ell _j} F_{jk})$.

The following results are well known.

Proposition 3

Given DRAs $\mathcal {R}_1$ and $\mathcal {R}_2$ recognizing languages $L_1$ and $L_2$, respectively, we can construct DRAs, denoted $\mathcal {R}_1 \cup \mathcal {R}_2$ and $\mathcal {R}_1 \cap R_2$, recognizing $L_1 \cup L_2$ and $L_1 \cap L_2$, respectively. Moreover, the transition system of both $\mathcal {R}_1 \cup \mathcal {R}_2$ and $\mathcal {R}_1 \cap R_2$ is the product of the transition systems of $R_1$ and $R_2$.

Proposition 4

Let X be a finite set of indices, and let $\mathcal {R}_i = (Q, \varSigma , \delta , q_{0}, \alpha _i)$ be a family of DRAs, one for every index i belonging to some finite set I of indices, all of them with the same underlying transition system. Then $\mathcal {R}_\cup = (Q, \varSigma , \delta , q_{0}, \bigvee _{i \in I}\alpha _i)$ is a DRA recognizing $\bigcup _{i \in X} \mathsf {L}(\mathcal {R}_i)$, and $\mathcal {R}_\cap = (Q, \varSigma , \delta , q_{0}, \bigwedge _{i \in X} \alpha _i)$ is a generalized DRA recognizing $\bigcap _{i \in X} \mathsf {L}(\mathcal {R}_i)$.

3 Automata for ${\mathbf {G}}$-free formulae

We present a translation of ${\mathbf {G}}$-free formulae (i.e., formulae without any occurrence of the ${\mathbf {G}}$-operator) into a deterministic $\omega$-automaton with a very simple acceptance condition, which can be expressed both as a Büchi and a co-Büchi condition. The translation is by no means novel, but it serves as a warm-up for the next sections, which consider more general classes of formulae. Moreover, the section allows us to introduce the general scheme we use to design translations: first, we give a logical characterization theorem characterizing the words that satisfy a formula of the given class, and then we construct an automaton which accepts if f the condition of the characterization holds.

Theorem 1

(Logical characterization theorem I) Let $\varphi$ be a ${\mathbf {G}}$-free formula and let w be a word. Then $w \models \varphi$ iff there exists $i > 0$ such that ${ af}(\varphi , w_{0j}) \equiv _P {\mathbf {tt}}$ for every $j \ge i$.

Proof

By Lemma 1(2) it suffices to show that $w \models \varphi$ iff there exists $i > 0$ such that ${ af}(\varphi , w_{0i}) \equiv _P {\mathbf {tt}}$. (In the rest of this proof we use Lemma 1(2) without explicitly mentioning it.)

($\Leftarrow$): Assume there exists $i > 0$ such that ${ af}(\varphi , w_{0i}) \equiv _P {\mathbf {tt}}$. Then $w_i \models { af}(\varphi , w_{0i})$. By Proposition 2, we get $w = w_{0i}w_i \models \varphi$.

($\Rightarrow$): Assume $w \models \varphi$. We proceed by structural induction on $\varphi$. We only consider two representative cases.

• $\varphi = a$. Since $w \models \varphi$ we have $w = \nu w'$ for some word $w'$ and for some $\nu \in Ap$ such that $a \in \nu$. By the definition of ${ af}$ we have ${ af}(a, \nu ) \equiv _P {\mathbf {tt}}$, and, since $\nu = w_{01}$, we get ${ af}(\varphi , w_{01}) \equiv _P {\mathbf {tt}}$.

• $\varphi = \varphi _1 {\mathbf {U}}\varphi _2$. By the semantics of LTL there is $k \in \mathbb {N}$ such that $w_k \models \varphi _2$ and $w_\ell \models \varphi _1$ for every $0 \le \ell < k$. By induction hypothesis there exists for every $0 \le \ell < k$ an $i \ge \ell$ such that ${ af}(\varphi _1, w_{\ell i}) \equiv _P {\mathbf {tt}}$ and there exists an $i \ge k$ such that ${ af}(\varphi _2, w_{ki}) \equiv _P {\mathbf {tt}}$. Let j be the maximum of all those i’s. We prove ${ af}(\varphi _1 {\mathbf {U}}\varphi _2, w_{0j}) \equiv _P {\mathbf {tt}}$ via induction on k.

  • $k = 0$.

    $$\begin{aligned} \begin{array}{llr} &{} { af}(\varphi _1 {\mathbf {U}}\varphi _2, w_{0j}) \\ = &{} { af}(\varphi _2, w_{0j}) \vee ({ af}(\varphi _1, w_{0j}) \wedge { af}(\varphi _1 {\mathbf {U}}\varphi _2, w_{1j})) &{} \text {(def. of }{ af}) \\ \equiv _P &{} {\mathbf {tt}}\vee ({ af}(\varphi _1, w_{0j}) \wedge { af}(\varphi _1 {\mathbf {U}}\varphi _2, w_{1j})) &{} ({ af}(\varphi _2, w_{kj}) \equiv _P {\mathbf {tt}}) \\ \equiv _P &{} {\mathbf {tt}}\end{array} \end{aligned}$$

  • $k > 0$.

    $$\begin{aligned} \begin{array}{llr} &{} { af}(\varphi _1 {\mathbf {U}}\varphi _2, w_{0j}) \\ = &{} { af}(\varphi _2, w_{0j}) \vee ({ af}(\varphi _1, w_{0j}) \wedge { af}(\varphi _1 {\mathbf {U}}\varphi _2, w_{1j})) &{} \text {(def. of }{ af}) \\ \equiv _P &{} { af}(\varphi _2, w_{0j}) \vee ({\mathbf {tt}}\wedge { af}(\varphi _1 {\mathbf {U}}\varphi _2, w_{1j})) &{} ({ af}(\varphi _1, w_{0j}) \equiv _P {\mathbf {tt}}) \\ \equiv _P &{} { af}(\varphi _2, w_{0j}) \vee ({\mathbf {tt}}\wedge {\mathbf {tt}}) &{} \text {(ind. hyp.)} \\ \equiv _P &{} {\mathbf {tt}}\end{array} \end{aligned}$$

$\square$

We derive from Theorem 1 a deterministic $\omega$-automaton for a given ${\mathbf {G}}$-free formula $\varphi$. The states of the automaton are equivalence classes of formulae under propositional equivalence. The fundamental design idea is: after reading a finite word w, the current state of the automaton must be ${ af}(\varphi , w_{0j})$. So we take the equivalence class of ${ af}(\varphi , \epsilon )~=~\varphi$ as initial state, and the function ${ af}$ itself as transition function. By Theorem 1, a word satisfies $\varphi$ iff its run in this automaton visits the state $[{\mathbf {tt}}]_P$. Since we have ${ af}({\mathbf {tt}}, \nu ) = {\mathbf {tt}}$ for every $\nu \in 2^{Ap}$, the run visits $[{\mathbf {tt}}]_P$ iff it visits $[{\mathbf {tt}}]_P$ infinitely often, or if it visits all other states only finitely often. So we can take $F=\{ [{\mathbf {tt}}]_P \}$ as Büchi condition.

Definition 7

Let $\varphi$ be a ${\mathbf {G}}$-free formula. Let ${ Reach}(\varphi )$ denote the set of equivalence classes of the formulae reachable from $\varphi$ w.r.t. propositional equivalence. The transition system of $\varphi$ is the deterministic transition system ${{\mathcal {T}}}(\varphi ) = (Q, 2^{Ap}, q_0, \delta )$ where

• Q is the quotient of ${ Reach}(\varphi )$ under propositional equivalence. (In other words, $[\psi ]_P$ is a state of ${{\mathcal {T}}}(\varphi )$ iff ${ af}(\varphi , w) = \psi$ for some finite word w.)

• $q_0=[\varphi ]_P$, the equivalence class of $\varphi$.

• $\delta ([\psi ]_P, \nu ) = [{ af}(\psi , \nu )]_P$ for every $[\psi ]_P \in Q$ and every $\nu \in 2^{Ap}$. (I.e., there is a transition $[\varphi ]_P \mathop {\longrightarrow }\limits ^{\nu } [\psi ]_P$ iff ${ af}(\varphi , \nu ) = \psi$.)

The Büchi automaton for $\varphi$ is the tuple $\mathcal {B}(\varphi )= (Q, 2^{Ap}, q_0, \delta , F)$, where $F = \{[{\mathbf {tt}}]_P\}$. Observe that it can be also seen as a co-Büchi automaton with $F=Q\setminus \{[{\mathbf {tt}}]_P\}$.

Example 2

Figure 1 shows the automaton for the formula $\varphi = a \vee (b \; {\mathbf {U}}\; c)$. We assume $Ap= \{a, b, c\}$. The alphabet $2^{Ap}$ contains 8 elements, and so every state has 8 outgoing transitions. To avoid cluttering the figure, we use a boolean-function-like notation for transitions. For example, $q_2 \mathop {\longrightarrow }\limits ^{c} q_3$ denotes that there is a transition from $q_2$ to $q_3$ for every subset of $2^{ Ap}$ containing c. So, actually, $q_2 \mathop {\longrightarrow }\limits ^{c} q_3$ stands for four different transitions. Similarly, $q_1 \mathop {\longrightarrow }\limits ^{a+{\bar{a}}c} q_3$ means that there is a transition from $q_1$ to $q_3$ for each subset of $2^{ Ap}$ that either contains a, or does not contain a and contains c.

Fig. 1

Büchi (or co-Büchi) automaton for $a \vee (b \; {\mathbf {U}}\;c)$

Theorem 2

Let $\varphi$ be a ${\mathbf {G}}$-free formula. Then $\mathsf {L}(\mathcal {B}(\varphi ))= \mathsf {L}(\varphi )$

Proof

Immediate consequence of Theorem 1 and the definition of $\mathcal {B}(\varphi )$. $\square$

Remark

Computing $\mathcal {B}(\varphi )$ requires a data structure to represent the equivalence classes of the formulae of ${ Reach}(\varphi )$ with respect to propositional equivalence. Let $PF(\varphi )$ denote the set of proper subformulae of $\varphi$. By Lemma 1(1), a formula of ${ Reach}(\varphi )$ is a boolean combination of formulae of $PF(\varphi )$. Hence, every formula of ${ Reach}(\varphi )$ induces a boolean function over $PF(\varphi )$, and two formulae of ${ Reach}(\varphi )$ are propositionally equivalent iff they induce the same function. In other words, the equivalence class of a formula can be identified with its boolean function. In our implementation, described in Sect. 9, we use Binary Decision Diagrams as data structure for boolean functions. It is well known that with this data structure propositional equivalence can be checked in constant time. Other operations have exponential worst-case complexity, but in all our experiments the time needed to perform them is negligible.

4 DRAs for simple ${\mathbf {F}}{\mathbf {G}}$-formulae

We introduce the main building block of our paper: a procedure to construct a DRA for formulae ${\mathbf {F}}{\mathbf {G}}\varphi$ where $\varphi$ is ${\mathbf {G}}$-free, i.e., contains no occurrence of ${\mathbf {G}}$. (Notice that even the formula ${\mathbf {F}}{\mathbf {G}}a$ has no equivalent deterministic Büchi automaton.)

As in the previous section, we first characterize the words w satisfying a formula ${\mathbf {F}}{\mathbf {G}}\varphi$ where $\varphi$ is ${\mathbf {G}}$-free, and then show how to construct a DRA that accepts iff the condition of the characterization holds. However, in this section we divide this step into two parts. We first introduce an auxiliary automata model, called Mojmir automata,² and show how to construct a Mojmir automaton recognizing $\mathsf {L}({\mathbf {F}}{\mathbf {G}}\varphi )$. (Mojmir automata are designed to make this construction intuitive and easy to grasp.) Then we show how to transform Mojmir automata into equivalent DRAs.

4.1 Logical characterization

The logical characterization of the words satisfying ${\mathbf {F}}{\mathbf {G}}\varphi$ is an easy consequence of Theorem 1.

Theorem 3

(Logical characterization theorem II) Let ${\mathbf {F}}{\mathbf {G}}\varphi$ be a formula such that $\varphi$ is ${\mathbf {G}}$-free. Then $w \models {\mathbf {F}}{\mathbf {G}}\varphi$ iff for almost every $i \in \mathbb {N}$ there exists $j \ge i$ such that ${ af}(\varphi , w_{ij})\equiv _P {\mathbf {tt}}$.

Proof

By the semantics of LTL, $w \models {\mathbf {F}}{\mathbf {G}}\varphi$ iff $w_i \models \varphi$ for almost every $i \in \mathbb {N}$. By Theorem 1, $w \models {\mathbf {F}}{\mathbf {G}}\varphi$ iff for almost every $i \in \mathbb {N}$ there exists $j \ge i$ such that ${ af}(\varphi , w_{ij})\equiv _P {\mathbf {tt}}$. $\square$

4.2 Mojmir automata

By the definition of LTL, we have $w \models {\mathbf {F}}{\mathbf {G}}\varphi$ iff $w_i \models \varphi$ for all but finitely many $i \ge 0$. Let $A_\varphi$ be the deterministic co-Büchi automaton recognizing $\mathsf {L}(\varphi )$. From a mathematical point of view, we can recognize $\mathsf {L}({\mathbf {F}}{\mathbf {G}}\varphi )$ with the help of an infinite array of copies of $A_\varphi$. The ith automaton reads $w_i$, i.e., it skips the first $(i-1)$ letters of the input word, and then starts reading. Therefore, the i-th automaton accepts iff $w_i \models \varphi$. The array accepts iff almost every array element accepts. Figure 2 shows the first four elements of the array for the formula ${\mathbf {F}}{\mathbf {G}}(a \vee (b \; {\mathbf {U}}\; c))$. The figure shows the state of the elements after reading $(abc) \; ({\bar{a}}b{\bar{c}}) \; ({\bar{a}}b{\bar{c}})$. For example, the automaton on the left has read all three letters, and reached state $q_3$, graphically displayed by putting a token on the state, while the next one has only read the last two letters, and reached state $q_2$. The last automaton has not yet read any letter, and so it is currently in state $q_1$.

Fig. 2

The top row shows the first four elements of the array of co-Büchi automata for ${\mathbf {F}}{\mathbf {G}}(a \vee (b \; {\mathbf {U}}\; c))$ after reading $abc \; {\bar{a}}b{\bar{c}} \; {\bar{a}}b{\bar{c}}$. At the bottom, the corresponding configuration of the Mojmir automaton

We now observe that the complete array can be replaced by one single automaton that handles all the tokens simultaneously. We call such an automaton a Mojmir automaton. The bottom part of Fig. 2 shows the configuration of the Mojmir automaton corresponding to the array at the top. After reading $(abc) \; ({\bar{a}}b{\bar{c}}) \; ({\bar{a}}b{\bar{c}})$, the automaton has created four tokens, labelled with their birthdates. Intuitively, when the automaton reads a letter it moves all tokens according to the transition function, and then puts a fresh token in the initial state, labelled with the position of the letter. Initially there is a unique token at the initial state, labelled by 0. The automaton accepts if almost every token eventually reaches an accepting state.

Definition 8

A Mojmir automaton is a tuple $\mathcal {M}=(Q,\varSigma ,q_0,\delta , F)$, where $(Q,\varSigma ,q_0,\delta )$ is a DTS and $F \subseteq Q$ is a set of accepting states satisfying $\delta (F,\nu )\subseteq F$ for every $\nu \in \varSigma$, i.e., states reachable from accepting states are also accepting.

The run of $\mathcal {M}$ over a word $w=w[0]w[1]\ldots \in \varSigma ^\omega$ is the infinite sequence

$$\begin{aligned} (q^0_0) \; (q^1_0,q^1_1) \; (q^2_0,q^2_1,q^2_2) \; (q^3_0,q^3_1,q^3_2, q^3_3)\ldots \end{aligned}$$

where

$$\begin{aligned} q^{ time }_{ token }= {\left\{ \begin{array}{ll} q_0&{}\text {if}\; token = time ,\\ \delta \big (q^{ time -1}_{ token },w[ time -1] \big )&{}\text {if} \; token < time \end{array}\right. } \end{aligned}$$

The position of a token at a time in the run is given by the function ${ run}_w:\mathbb {N} \times \mathbb {N} \rightarrow Q \cup \{ \bot \}$, defined as follows:

$$\begin{aligned} { run}_w(token, time) = {\left\{ \begin{array}{ll} q^{\textit{time}}_{\textit{token}} &{} \text{ if } \; \textit{token} \le \textit{time} \\ \bot &{} \text{ if }\; \textit{token} > \textit{time} \end{array}\right. } \end{aligned}$$

For every time $t \in \mathbb {N}$, we denote by ${ conf}_w( t)$ the function defined by

$$\begin{aligned} token \mapsto { run}_w( token, t)) \end{aligned}$$

We call ${ conf}_w(t)$ the configuration of the run of $\mathcal {M}$ on w at time t. The run of $\mathcal {M}$ on w is accepting if for almost every $token \in \mathbb {N}$ there exists $time \in \mathbb {N}$ such that ${ run}_w( token, time) \in F$.

Given a ${\mathbf {G}}$-free formula $\varphi$, the Mojmir automaton equivalent to ${\mathbf {F}}{\mathbf {G}}\varphi$ has exactly the same syntactic structure as the Büchi automaton for $\varphi$: only the notions of run and acceptance are different.

Definition 9

Let $\varphi$ be a ${\mathbf {G}}$-free formula. The Mojmir automaton for ${\mathbf {F}}{\mathbf {G}}\varphi$ is $\mathcal {M}(\varphi )=({ Reach}(\varphi ), 2^{Ap}, [\varphi ]_P, { af}, \{[{\mathbf {tt}}]_P\})$.

Since $\mathcal {M}(\varphi )$ accepts iff almost every token eventually reaches an accepting state, $\mathcal {M}(\varphi )$ accepts a word w iff $w \models {\mathbf {F}}{\mathbf {G}}\varphi$, and so we have:

Theorem 4

Let $\varphi$ be a ${\mathbf {G}}$-free formula. Then $\mathsf {L}(\mathcal {M}(\varphi )) = \mathsf {L}({\mathbf {F}}{\mathbf {G}}\varphi )$.

Fig. 3

Mojmir automaton for ${\mathbf {F}}{\mathbf {G}}(a \vee (b \; {\mathbf {U}}\; c))$, and matrix representation of ${ run}_w( token, time)$ for $w = abc \; {\bar{a}}b\bar{c} \; {\bar{a}}b\bar{c} \ldots$

Example 3

Figure 3 shows the Mojmir automaton for ${\mathbf {F}}{\mathbf {G}}(a \vee (b \; {\mathbf {U}}\; c))$ and the matrix representation of ${ run}_w( token, time)$ for $w = abc \; {\bar{a}}b\bar{c} \; {\bar{a}}b\bar{c} \ldots$. The configurations of the run are given by the columns of the matrix. For instance, ${ conf}_w(2)$ is the mapping $0 \mapsto q_3, 1 \mapsto q_2, 2 \mapsto q_1, \forall i\ge 3:i \mapsto \bot$ given by the third column, indicating that after two steps the tokens 0, 1, 2 are in states $q_3, q_2, q_1$, respectively, and other tokens do not exist yet.

In the rest of the section we show how to construct a deterministic Rabin automaton equivalent to a given Mojmir automaton. In Sect. 4.3 we define an abstraction that assigns to each configuration ${ conf}_w(t)$ of a run an abstract object ${ sr}_w(t)$, called a state-ranking. Since the run of $\mathcal {M}$ on a word w is completely characterized by the sequence of configurations ${ conf}_w(0)\, { conf}_w(1) \, { conf}_w(2) \ldots$, the abstraction also abstracts a run into the infinite sequence of state-rankings ${ sr}_w(0) \, { sr}_w(1) \, { sr}_w(2) \ldots$. Sections 4.4 and 4.5 show that the abstraction has the following properties:

• 1. There is an easily computable function that given ${ sr}_w(t)$ and $w[t+1]$ returns ${ sr}_w(t+1)$. (Lemma 3)

• 2. A run is accepting iff its corresponding abstract run satisfies a certain Rabin condition. (Definition 16)

Finally, Sect. 4.6 derives the deterministic Rabin automaton. As the reader can expect, the automaton will have the state-rankings as states, the function of (1) as transition function, and the condition of (2) as acceptance condition.

4.3 State-rankings

Intuitively, a state-ranking of a Mojmir automaton $\mathcal {M}$ is a ranking of the states of $\mathcal {M}$. Our state-rankings are allowed to be partial, that is, to leave some states unranked.

Definition 10

Let $\mathcal {M}$ be a Mojmir automaton with n states. A state-ranking of $\mathcal {M}$ is a partial injective function $sr :Q \rightarrow \{\mathbf {1}, \ldots , \mathbf {n}\}$, such that if the image of sr contains $\mathbf {i}$, then it also contains $\mathbf {j}$ for every $\mathbf {j} < \mathbf {i}$. When sr(q) is undefined, we write $sr(q)=\bot$. The set of state-rankings of $\mathcal {M}$ is denoted by ${{\mathcal {S}}}{{\mathcal {R}}}$.

The state-ranking ${ sr}_w(t)$ associated to ${ conf}_w(t)$ is the result of performing a sequence of abstraction steps, which we illustrate on an example. Consider a Mojmir automaton $\mathcal {M}$ with states $\{q_0, q_1, q_2, q_3, q_4, q_5, q_6\}$. Assume that, after the first 8 steps of its run on some word, $\mathcal {M}$ has reached the following configuration, where for each state we give the set of tokens currently at that state:

$$\begin{aligned} \begin{array}{cccccccc} q_0 &{} q_1 &{} q_2 &{} q_3 &{} q_4 &{} q_5 &{} q_6\\ (\{3, 8\} &{} \{1, 2\} &{} \emptyset &{} \{5, 7\} &{} \{4\} &{} \{6\} &{} \{0\}) \end{array} \end{aligned}$$

(1)

Assume further that states $q_5, q_6$ are sinks, meaning that $\delta (q_5, \nu ) = q_5$ and $\delta (q_6, \nu ) = q_6$ for every alphabet letter $\nu$.³ We start the abstraction process by discarding the information about tokens in sinks. We use the symbol $\bot$ to denote this, and obtain:

$$\begin{aligned} \begin{array}{cccccccc} q_0 &{} q_1 &{} q_2 &{} q_3 &{} q_4 &{} q_5 &{} q_6 \\ (\{3, 8\} &{} \{1, 2\} &{} \emptyset &{} \{5, 7\} &{} \{4\} &{} \bot &{} \bot ) \end{array} \end{aligned}$$

We continue by keeping only the oldest token of each state (that is, the one with the smallest number). If the state is not populated by any token, again we just write $\bot$. We obtain:

$$\begin{aligned} \begin{array}{rcccccccl} q_0 &{} q_1 &{} q_2 &{} q_3 &{} q_4 &{} q_5 &{} q_6\\ (3 &{} 1 &{} \bot &{} 5 &{} 4 &{} \bot &{} \bot ) \end{array} \end{aligned}$$

We call tokens 3, 1, 5 and 4 the senior tokens of the configuration, or just the seniors.

Since a run has infinitely many tokens, the number of possible abstract configurations of the automaton is still infinite. So we discard even more information. We throw away the identities of the senior tokens, and keep only their relative seniority rank: the oldest senior token has rank 1, the second oldest rank 2, etc. We obtain the state-ranking

$$\begin{aligned} \begin{array}{cccccccc} q_0 &{} q_1 &{} q_2 &{} q_3 &{} q_4 &{} q_5 &{} q_6 \\ (\mathbf{2} &{} \mathbf{1} &{} \bot &{} \mathbf{4} &{} \mathbf{3} &{} \bot &{} \bot ) \end{array} \end{aligned}$$

It is useful to think of the set of tokens at a state as the partners of a partnership firm. The senior partner is the oldest token. The name of the firm is the rank of the senior partner. For instance, the firm $\mathbf{2}$ at state $q_0$ has tokens 3 and 8 as partners.

Let us formally define the rank ${ rk}_w(\tau , t)$ of token $\tau$ at time t, and the state-ranking ${ sr}_w(t)$ at time t.

Definition 11

Let $\mathcal {M}=(Q,\varSigma ,q_0,\delta , F)$ be a Mojmir automaton with n states. A state $q \in Q$ is a sink if $q \ne q_0$ and $\delta (q, \nu ) = q$ for every $\nu \in \varSigma$.

Let $w \in \varSigma ^\omega$ be a word, and consider the run of $\mathcal {M}$ on w. Given two tokens $\tau , \tau ' \in \mathbb {N}$, we say that $\tau$ is older than $\tau '$ if $\tau < \tau '$. The senior of token $\tau$ at time $t>\tau$ is the oldest token $\tau '$ such that ${ run}_w(\tau , t) = { run}_w(\tau ', t)$. If a token is its own senior, then we call $\tau$ a senior (at time t).

The rank of token $\tau$ at time $t>\tau$, denoted by ${ rk}_w(\tau , t)$, is defined as follows:

• If ${ run}_w(\tau , t)$ is a sink, then ${ rk}_w(\tau , t) = \bot$ (we say that $\tau$ is unranked at time t).

• If ${ run}_w(\tau , t)$ is not a sink, then let s be the senior of token $\tau$ at time t. The rank ${ rk}_w(\tau , t)$ is the number of senior tokens $\tau '$ such that ${ run}_w(\tau ', t)$ is not a sink and $\tau ' \le s$.

(Observe that ${ run}_w(\tau , t)={ run}_w(\tau ', t)$ implies that $\tau$ and $\tau '$ have the same seniors, and so that ${ rk}_w(\tau , t) = { rk}_w(\tau ', t)$; so all tokens at the same state get the same rank.)

Finally, the state-ranking at time t, denoted by ${ sr}_w(t)$, is the mapping $Q\rightarrow \mathbb {N}$ that assigns to each state $q \in Q$ its state-ranking ${ sr}_w(t,q) \in \{\mathbf {1}, \ldots , \mathbf {n}\}$, defined as follows:

• If q is a sink, then ${ sr}_w(t,q) = \bot$.

• If q is not a sink and no token $\tau$ satisfies ${ run}_w(\tau , t) = q$, then ${ sr}_w(t,q) = \bot$.

• If q is not a sink and some token $\tau$ satisfies ${ run}_w(\tau , t) = q$, then ${ sr}_w(t,q) = { rk}_w(\tau , t)$.

Example 4

Consider for example token 7 in the configuration (1). The senior of 7 is 5. The seniors are 3, 1, 5, 4. Since all seniors are at least as old as 5, the rank of token 7 is $\mathbf {4}$. Since the configuration is the result of reading the first 8 letters of a word w, we have ${ rk}_w(7, 8) = \mathbf {4}$.

While the birthdate of a token does not change along a run, its rank can change, and for two different reasons. Assume the current rank of a token $\tau$ is $\mathbf {4}$. If the firm of rank, say, $\mathbf {3}$, moves to a sink, then it “disappears”, and the rank of $\tau$ is upgraded to $\mathbf {3}$. If the token’s firm merges with the firm of rank, say, $\mathbf {2}$, the rank of $\tau$ is upgraded to $\mathbf {2}$. In both cases, we observe that, as long as the token does not reach a sink, its rank can only improve (get older) along a run.

Lemma 2

Let $\mathcal {M}=(Q,\varSigma ,q_0,\delta , F)$ be a Mojmir automaton and let $w \in \varSigma ^\omega$ be a word. For every token $\tau \in \mathbb {N}$:

• if ${ rk}_w(\tau , t) = \bot$ for some $t \in \mathbb {N}$, then ${ rk}_w(\tau , t') = \bot$ for every $t' \ge t$.

• if $t \le t'$ and ${ rk}_w(\tau , t),{ rk}_w(\tau , t') \in \mathbb {N}$, then ${ rk}_w(\tau , t) \ge { rk}_w(\tau , t')$.

Proof

Follows easily from the definitions. $\square$

4.4 Computing the successor of a state-ranking

Recall that the run of a Mojmir automaton on a word w is completely determined by the sequence of configurations ${ conf}_w(0)\, { conf}_w(1) \, { conf}_w(2) \ldots$. To this sequence corresponds a sequence ${ sr}_w(0) \, { sr}_w(1), { sr}_w(2) \ldots$ of state-rankings. We show that ${ sr}_w(t+1)$ can be directly computed from ${ sr}_w(t)$ and the letter $w[t+1]$. More precisely, we define a function ${ nxt}:{{\mathcal {S}}}{{\mathcal {R}}} \times \varSigma \rightarrow {{\mathcal {S}}}{{\mathcal {R}}}$ and show that it satisfies ${ nxt}({ sr}_w(t), w[t+1]) = { sr}_w(t+1)$ for every time t.

Let ${ sr}_w(t)$ be the state-ranking

$$\begin{aligned} \begin{array}{cccccccc} q_0 &{} q_1 &{} q_2 &{} q_3 &{} q_4 &{} q_5 &{} q_6 \\ (\mathbf{2} &{} \mathbf{1} &{} \bot &{} \mathbf{4} &{} \mathbf{3} &{} \bot &{} \bot ) \end{array} \end{aligned}$$

Assume $w[t+1]= \nu$ for some $\nu \in \varSigma$, and assume further that

$$\begin{aligned} \delta (q_0, \nu ) = q_5 \qquad \delta (q_1, \nu ) = q_2 = \delta (q_3, \nu ) \qquad \delta (q_4, \nu ) = q_3 \end{aligned}$$

We obtain ${ sr}_w(t+1)$ in four steps:

• (i) Move all senior tokens according to $\delta$. The token of rank $\mathbf {2}$ at $q_0$ moves to the sink $q_5$ (recall that $q_5$ and $q_6$ are sinks) and “disappears”. The tokens of ranks $\mathbf {1}$ and $\mathbf {4}$ move to state $q_2$. The token of rank $\mathbf {3}$ at $q_4$ moves to $q_3$. We obtain:

  $$\begin{aligned} \begin{array}{cccccccc} q_0 &{} q_1 &{} q_2 &{} q_3 &{} q_4 &{} q_5 &{} q_6 \\ (\bot &{} \bot &{} \{ \mathbf{1}, \mathbf{4} \} &{} \mathbf{3} &{} \bot &{} \bot &{} \bot ) \end{array} \end{aligned}$$

• (ii) If a state holds more than one token, keep only the most senior token. Only the token of rank $\mathbf {1}$ survives in $q_2$. Intuitively, the firms with rank $\mathbf {1}$ and $\mathbf {4}$ merge, and $\mathbf {1}$ becomes the senior partner.

  $$\begin{aligned} \begin{array}{cccccccc} q_0 &{} q_1 &{} q_2 &{} q_3 &{} q_4 &{} q_5 &{} q_6 \\ ( \bot &{} \bot &{} \mathbf{1} &{} \mathbf{3} &{} \bot &{} \bot &{} \bot ) \end{array} \end{aligned}$$

• (iii) Recompute the seniority ranks of the remaining tokens. The token of rank $\mathbf {3}$ is upgraded to rank $\mathbf {2}$.

  $$\begin{aligned} \begin{array}{cccccccc} q_0 &{} q_1 &{} q_2 &{} q_3 &{} q_4 &{} q_5 &{} q_6 \\ ( \bot &{} \bot &{} \mathbf{1} &{} \mathbf{2} &{} \bot &{} \bot &{} \bot ) \end{array} \end{aligned}$$

• (iv) If there is no token on the initial state, add one with the next lowest seniority rank. We add a token to $q_0$ of rank $\mathbf {3}$.

  $$\begin{aligned} \begin{array}{cccccccc} q_0 &{} q_1 &{} q_2 &{} q_3 &{} q_4 &{} q_5 &{} q_6 \\ (\mathbf{3} &{} \bot &{} \mathbf{1} &{} \mathbf{2} &{} \bot &{} \bot &{} \bot ) \end{array} \end{aligned}$$

The corresponding formal definition is:

Definition 12

Let $\mathcal {M}=(Q,\varSigma ,q_0,\delta , F)$ be a Mojmir automaton with n states and a set S of sinks. Let sr be a state-ranking of $\mathcal {M}$, and let $\nu \in \varSigma$. For every $q \in Q$, the set of ranks of sr that move to q under $\nu$, denoted by mvto(q), is given by:

$$\begin{aligned} mvto(q) = {\left\{ \begin{array}{ll} \{sr(q') \mid sr(q') \ne \bot \wedge \delta (q',\nu ) = q \} &{} \hbox { if } q \ne q_0 \\ \{sr(q') \mid sr(q') \ne \bot \wedge \delta (q',\nu ) = q \} \cup \{ \mathbf {n} \} &{} \hbox { if }q = q_0 \end{array}\right. } \end{aligned}$$

The state-ranking ${ nxt}(sr,\nu )$ is defined with $\min (\emptyset ) = \infty$ by:

$$\begin{aligned}&{ nxt}(sr,\nu ,q) \nonumber \\&\quad = {\left\{ \begin{array}{ll} |\{ q' \in Q \setminus S \mid \min ( mvto(q')) \le \min (mvto(q))\}| &{} \hbox {if}\; q \notin S \text{ and } mvto(q) \ne \emptyset \\ \bot &{} \text{ otherwise } \end{array}\right. } \end{aligned}$$

We get the following lemma.

Lemma 3

Let $\mathcal {M}$ be a Mojmir automaton and let w be a word. Then ${ sr}_w(t+1) = { nxt}({ sr}_w(t),w[t+1])$ for every $t \ge 0$.

Proof

(Sketch) The key observation for the proof is that ${ nxt}({ sr}_w(t),w[t+1])$ computes for a state q the set of senior states $q'$ at time $t+1$ and then takes the cardinality of this set as a value. This coincides with the definition of ${ sr}_w(t+1)$. $\square$

We already have all we need to define the states and transition function of the DRA equivalent to a given Mojmir automaton (although not the acceptance condition). The states of the Rabin automaton are the state-rankings, and the transition function is given by ${ nxt}$.

Example 5

Figure 4 shows our running example on the left, and the states and transitions of its corresponding Rabin automaton on the right. Since states $q_3$ and $q_4$ are sinks, state rankings only rank states $q_1$ and $q_2$. The initial state-ranking is $(\mathbf {1},\bot )$. The only other state-ranking reachable from it turns out to be $(\mathbf {2},\mathbf {1})$.

Fig. 4

A Mojmir automaton for $a \vee (b \; {\mathbf {U}}\; c)$ and its corresponding DRA

4.5 Deciding acceptance of an abstract run

We define a Rabin acceptance condition that turns the transition system above into a DRA equivalent to the Mojmir automaton. We start by classifying the tokens of a run of the Mojmir automaton.

Definition 13

Let $\mathcal {M}=(Q,\varSigma ,\delta , q_0, F)$ be a Mojmir automaton and let w be a word. A token $\tau \in \mathbb {N}$ of the run of $\mathcal {M}$ on w

• squats if it never reaches a sink

  (that is, if ${ run}_w(\tau , t) \in Q \setminus S$ for every $t \in \mathbb {N}$);

• fails if it eventually reaches a non-accepting sink

  (that is, if there exists $t \in \mathbb {N}$ such that ${ run}_w(\tau , t) \in S \setminus F$);

• succeeds if it eventually reaches an accepting state, sink or non-sink

  (that is, if there exists $t \in \mathbb {N}$ such that ${ run}_w(\tau , t) \in F$).

Further, we say that a token succeeds at rank $\mathbf {i}$ if it has rank $\mathbf {i}$ immediately before entering the set of accepting states, i.e., if there is $t \in \mathbb {N}$ such that ${ run}_w(\tau , t) \notin F \setminus \{q_0\}$, ${ run}_w(\tau , t+1) \in F$, and ${ rk}_w(\tau , t) = {\mathbf {i}}$.⁴

Observe that the three classes are not disjoint. More precisely, a token either fails, succeeds, or squats in non-accepting states. By definition, a Mojmir automaton accepts a word w if all but finitely many of the tokens generated during the run on w succeed (recall that tokens that reach an accepting state stay within the set of accepting states). So, given the abstract run of $\mathcal {M}$ on w, our task is to find a Rabin condition equivalent to “only finitely many tokens fail and only finitely many tokens squat in non-accepting states”. The condition equivalent to “only finitely many tokens fail” is simple: since a token fails when it moves into a non-accepting sink, we stipulate that transitions moving tokens into non-accepting sinks can only occur finitely often.

Finding a condition equivalent to “only finitely many tokens squat in non-accepting states” is a bit more involved. Observe that, since a squatter $\tau$ never reaches a sink, it has a rank at every moment in time. So, if infinitely many tokens squat in non-accepting states, then, since they are all confined within $Q \setminus (S \cup F)$, infinitely many firm merges must take place in this set of states. This suggests the following definition:

Definition 14

Let $\mathcal {M}=(Q,\varSigma ,\delta , q_0, F)$ be a Mojmir automaton and let w be a word. Let $\tau , \tau ' \in \mathbb {N}$ be two tokens such that $\tau < \tau '$. We say that $\tau$ and $\tau '$ merge during the run of $\mathcal {M}$ on w if there is $t \in \mathbb {N}$ and a state $q \notin F$ such that ${ run}_w(\tau , t) = q = { run}_w(\tau ', t)$, and one of the two following conditions hold:

• $\tau ' < t$ and ${ run}_w(\tau , t-1) \ne { run}_w(\tau ', t-1)$.

  (Both tokens already existed at time $t-1$, and were at different states)

• $\tau ' = t$.

  (Token $\tau '$ is created at time t.)

Further, we say that the tokens merge at rank $\mathbf {i}$ if ${ rk}_w(\tau , t) = \mathbf {i}$.

Notice the condition $q \notin F$ in the definition: we reserve the term “merge” for the merges occurring in non-accepting states.

If two tokens merge at some time t, then from that moment on they follow the same trajectory, and so we have:

Lemma 4

Let $\mathcal {M}=(Q,\varSigma ,\delta , q_0, F)$ be a Mojmir automaton and let w be a word. Let $\tau , \tau ' \in \mathbb {N}$ be two tokens that merge along the run of $\mathcal {M}$ on w. Then either both $\tau$ and $\tau '$ fail, or both succeed at the same rank, or both squat.

Proof

By the definition of merge there is a time $t_0$ such that ${ run}_w(\tau , t_0) = q \notin F$ and ${ run}_w(\tau , t) = { run}_w(\tau ', t)$ for all $t \ge t_0$. We proceed by case distinction and only consider two cases.

• $\tau$ fails. This means that the token $\tau$ moves at some point to a non-accepting sink and stays there forever. Let us call this time $t'$. Without loss of generality we assume that the merge happens outside the sinks S and we have $t' > t_0$. Hence we have ${ run}_w(\tau ', t') = { run}_w(\tau , t') = q_s$ and thus $\tau '$ also fails.

• $\tau$ succeeds at rank i. Thus the token $\tau$ moved at some time $t' > t_0$ from the non-accepting states to the accepting states with rank i. Since $\tau$ and $\tau '$ already merged and tokens that are in the same state have the same rank, also $\tau '$ succeeds with rank i. $\square$

We can now formulate and prove the main theorem of the section, presenting conditions equivalent to “only finitely many tokens fail” (condition (1)), and “only finitely many tokens squat in non-accepting states” (condition (2)):

Theorem 5

Let $\mathcal {M}=(Q,\varSigma ,\delta , q_0, F)$ be a Mojmir automaton and let w be a word. $\mathcal {M}$ accepts w if and only if the run of $\mathcal {M}$ on w satisfies the following two conditions:

• (1) Finitely many tokens fail.

• (2) There is a rank $\mathbf {i}$ such that

  • (2.1) infinitely many tokens succeed at rank ${\mathbf {i}}$, and

  • (2.2) finitely many pairs of tokens merge at rank older than ${\mathbf {i}}$, i.e. with a rank ${\mathbf {j}} < {\mathbf {i}}$.

Proof

$(\Rightarrow )$: Assume $\mathcal {M}$ accepts w. Then almost every token of the run of $\mathcal {M}$ on w succeeds. Therefore, since no token can succeed and fail, (1) holds.

Let $\mathbf {i}$ be the smallest rank satisfying (2.1) (since almost all tokens succeed and the number of ranks are finite, such an $\mathbf {i}$ exists). We prove that $\mathbf {i}$ satisfies (2.2). Let $M_i$ be the set of pairs $(\tau , \tau ')$ of tokens such that $\tau < \tau '$ and $\tau$ and $\tau '$ merge at rank older than $\mathbf {i}$. We prove that $M_i$ is finite. By Lemma 4 either both $\tau$ and $\tau '$ succeed, or none succeeds. Let $S_i$ be the set of pairs $(\tau , \tau ') \in M_i$ such that both $\tau$ and $\tau '$ succeed. Since $\mathcal {M}$ accepts w, almost every token succeeds, and so $M_i \setminus S_i$ is finite.

It remains to prove that $S_i$ is finite. By the definition of $\mathbf {i}$, it suffices to prove that for every $(\tau , \tau ') \in S_i$ both $\tau$ and $\tau '$ succeed at a rank older than $\mathbf {i}$. Let $t_0$ be the time at which $\tau$ and $\tau '$ merge. By the definition of a merge, at time $t_0$ neither $\tau$ nor $\tau '$ have reached the set of accepting states. Since $\tau$ and $\tau '$ merge at rank older than $\mathbf {i}$ and two merged tokens always have the same rank, we have ${ rk}_w(\tau ', t_0) < \mathbf {i}$. Let $t_1 > t_0$ be the time at which both tokens enter the set of accepting states. By Lemma 2(2), we have ${ rk}_w(\tau , t_1) < \mathbf {i}$ and ${ rk}_w(\tau ', t_1) < \mathbf {i}$, and so both $\tau$ and $\tau '$ succeed at a rank older than $\mathbf {i}$.

$(\Leftarrow )$: If $q_0 \in F$ then by the definition of Mojmir automata $\mathcal {M}$ accepts every word, and we are done. So assume $q_0 \notin F$.

By the definition of squatting, a token $\tau$ squats iff ${ rk}_w(\tau , t) \in \mathbb {N}$ for every $t \ge \tau$. By Lemma 2, the rank of $\tau$ can only get older, and so there is a time t such that ${ rk}_w(\tau , t) = { rk}_w(\tau , t')$ for every $t' \ge t$. We call this rank the stable rank of $\tau$, denoted by ${ strk}_w(\tau )$. The following lemma, proved in the Appendix, shows that all stable ranks are old. $\square$

Lemma 5

Let $\mathbf {i}$ be the rank of condition (2). If the rank of $\tau$ stabilizes, then ${ strk}_w(\tau ) < \mathbf {i}$.

We now use the lemma to prove the result by contradiction. Assume $\mathcal {M}$ does not accept w. Then, infinitely many tokens do not succeed in the run of $\mathcal {M}$ on w. Since by (1) only finitely many tokens fail, infinitely many tokens squat in non-accepting states. By Lemma 5, their stable ranks are all older than $\mathbf {i}$. So there is a rank $\mathbf {j} < \mathbf {i}$ such that infinitely many tokens have stable rank $\mathbf {j}$. Let $\tau$ be one of these tokens, and let t be the time at which its rank stabilizes. All tokens born after t whose rank stabilize at $\mathbf {j}$ eventually merge with $\tau$. Therefore, infinitely many pairs $(\tau , \tau ')$ merge at rank $\mathbf {i}$. But this contradicts our assumption that (2.2) holds.

We conclude the section with a definition that will be important in Sect. 6.

Definition 15

Let $\mathcal {M}$ be a Mojmir automaton and let w be a word. We say that $\mathcal {M}$ accepts w at rank $\mathbf {i}$ if $\mathcal {M}$ accepts w and the rank of condition (2) in Theorem 5 is $\mathbf {i}$.

Note that a word can be accepted at several ranks. In Sect.  6.2 we will show that the ranks at which the automaton $\mathcal {M}(\varphi )$ of a formula $\varphi$ accepts a word carry useful information.

4.6 From Mojmir automata to deterministic Rabin automata

From Theorem 5 we can easily derive a deterministic Rabin automaton equivalent to a given Mojmir automaton. More precisely, we show how to construct an automaton with a Rabin condition on transitions. Applying the construction of Sect. 2.3.1, this automaton can be transformed into one with a Rabin condition on states.

Definition 16

Let $\mathcal {M}=(Q,\varSigma ,q_0,\delta , F)$ be a Mojmir automaton with a set S of sinks. The deterministic Rabin automaton $\mathcal {R}(\mathcal {M}) = (Q_\mathcal {R},\varSigma , q_{0\mathcal {R}},\delta _\mathcal {R}, \alpha _\mathcal {R})$ is defined as follows:

• $Q_\mathcal {R}$ is the set ${{\mathcal {S}}}{{\mathcal {R}}}$ of state-rankings of $\mathcal {M}$;

• $q_{0\mathcal {R}}$ is the state-ranking satisfying $q_{0\mathcal {R}}(q_0)=\mathbf {1}$ and $q_{0\mathcal {R}}(q)=\bot$ for every $q \ne q_0$;

• $\delta _\mathcal {R}(sr,\nu ) = { nxt}(sr,\nu )$ for every state-ranking sr and letter $\nu$;

• $\alpha _\mathcal {R}= \bigvee _{i=1}^{|Q|} P_i$, where the ith Rabin pair is $P_i= ( fail \cup merge (\mathbf {i}), succeed (\mathbf {i}))$, and the sets $fail$, $merge (\mathbf {i})$, and $succeed (\mathbf {i})$ are defined as follows. A transition $(sr, \nu , sr')\in \delta _\mathcal {R}$ belongs to

  • $fail$ if there exists $q \in Q$ such that $sr(q) \in {\mathbb {N}}$ and $\delta (q, \nu )\in S\setminus F$.

  • $succeed (\mathbf {i})$ if there exists $q\notin F$ such that $sr(q)=\mathbf {i}$ and $\delta (q,\nu )\in F$, or $q_0 \in F$ and $sr(q_0)=\mathbf {i}$.⁵

  • $merge (\mathbf {i})$ if

    • there exists a state $q \in Q \setminus F$ and distinct states $q_1, q_2 \in Q$ such that $\delta (q_1, \nu ) = q = \delta (q_2, \nu )$, $sr(q_1)< \mathbf {i}$, and $sr(q_2) \ne \bot$; or

    • $q_0 \notin F$, and there exists a state q such that $\delta (q, \nu ) = q_0$ and $sr(q)< \mathbf {i}$.⁶

$\mathcal {R}(\mathcal {M})$ accepts a word w at rank $\mathbf {j}$ if $P_j$ is an accepting pair on the run of $\mathcal {R}(\mathcal {M})$ on w.

Example 6

Let us determine the accepting pairs of the DRA on the right of Fig. 4. We examine several representative cases.

• $t_1$ moves tokens from $q_1$ to the accepting sink $q_3$. Since $sr(q_1) = 1$, transition $t_1$ belongs to $succeed(\mathbf {1})$. Since we can safely ignore sinks ($q_3$, $q_4$) and states that are empty ($q_2$) for testing membership, we are done with $t_1$.

• $t_2$ takes tokens from the initial state and moves them to the non-accepting sink $q_4$. This matches the definition of $fail$, with $sr (q_1) \in {\mathbb {N}}$ and $\delta (q_1, {\bar{a}}\bar{b}{\bar{c}}) = q_4 \in S\setminus F$. Hence $t_2 \in fail$.

• $t_3$ moves tokens from $q_1$ to $q_2$. Since $q_2$ is neither a sink nor an accepting state, $t_3$ is not contained in $fail$ or in any $succeed$ set. Moreover, since $sr(q_2) = \bot$, it does not belong to any $merge$ set either.

• $t_8$ moves tokens from $q_1$ and $q_2$ to the non-accepting sink $q_3$. Hence $t_8 \in fail$. Moreover, the transition merges the tokens from $q_1$ and $q_2$ in $q_3$ with rank $sr(q_1) = 1$, and so $t_8$ is also contained in $merge (\mathbf {2})$.

Altogether we obtain

$$\begin{aligned} \textit{fail} = \{ t_2,t_7,t_8\} \quad \begin{array}{l} \textit{merge}(\mathbf {1}) = \emptyset \\ \textit{merge}(\mathbf {2})=\{t_5,t_8\} \end{array} \quad \begin{array}{l} \textit{succeed}(\mathbf {1}) = \{t_1,t_6\} \\ \textit{succeed}(\mathbf {2}) = \{t_4,t_6,t_7\} \end{array} \end{aligned}$$

It is easy to see that the runs accepted by the pair $P_1$ are those that take $t_2,t_7,t_8$ only finitely often, and visit $(\mathbf {1}, \bot )$ infinitely often. They are accepted at rank $\mathbf {1}$. The runs accepted at rank $\mathbf {2}$ are those accepted by $P_2$ but not by $P_1$. They take $t_1, t_2, t_5, t_6, t_7, t_8$ finitely often, and so they are exactly the runs with a $t_4^\omega$ suffix.

Lemma 6

Let $\mathcal {M}=(Q,\varSigma ,i,\delta , F)$ be a Mojmir automaton, and let $\mathcal {R}(\mathcal {M})$ be its corresponding Rabin automaton. For every word w, the sequence ${ conf}_w(0) { conf}_w(1) \ldots$ is the run of $\mathcal {M}$ on w iff $sr_w(0) sr_w(1) \ldots$ is the run of $\mathcal {R}(\mathcal {M})$ on w.

The Rabin condition of this automaton checks conditions (1) and (2) of Theorem 5. Consider a transition ${ conf}_w(t) \mathop {\longrightarrow }\limits ^{a} { conf}_w(t+1)$ between two configurations of $\mathcal {M}$ in which some token moves into a non-accepting sink. Then the transition ${ sr}_w(t) \mathop {\longrightarrow }\limits ^{a} { sr}_w(t+1)$ clearly belongs to the set $fail$, and vice versa. Similarly, transitions of $succeed (\mathbf {i})$ correspond to transitions of $\mathcal {M}$ that make some token succeed at rank $\mathbf {i}$, and transitions of $merge (\mathbf {i})$ correspond to transitions of $\mathcal {M}$ that merge two tokens at rank $\mathbf {i}$. So we obtain:

Theorem 6

Let $\mathcal {M}$ be a Mojmir automaton, and let $\mathcal {R}(\mathcal {M})$ be its corresponding Rabin automaton. Then $\mathsf {L}(\mathcal {M}) = \mathsf {L}(\mathcal {R}(\mathcal {M}))$. Moreover, for every $w \in \mathsf {L}(\mathcal {M})$ both $\mathcal {M}$ and $\mathcal {R}(\mathcal {M})$ accept w at the same ranks.

5 DRAs for arbitrary ${\mathbf {F}}{\mathbf {G}}$-formulae

We show how to translate formulae of the form ${\mathbf {F}}{\mathbf {G}}\varphi$ into DRAs. Thanks to the results of Sect. 4, it suffices to translate them into Mojmir automata. We show that the Mojmir automaton for a formula can be defined compositionally, as an intersection of Mojmir automata. The next proposition shows that Mojmir automata are closed under union and intersection (the proof can be found in the Appendix).

Proposition 5

Let $\mathcal {M}_1=(Q_1,\varSigma ,q_{01},\delta _1, F_1)$ and $\mathcal {M}_2=(Q_2,\varSigma ,q_{02},\delta _2, F_2)$. Let $Q=Q_1 \times Q_2$, let $q_0 = (q_{01},q_{02})$, and let $\delta :Q \times \varSigma \rightarrow Q$ be the function given by $\delta (q_1,q_2, \nu ) = (\delta _1(q_1, \nu ), \delta _2(q_2, \nu ))$ Then the tuples

$$\begin{aligned} \mathcal {M}_1 \cap \mathcal {M}_2= & {} \big (Q,\varSigma ,q_0,\delta , F_1 \times F_2 \big ) \\ \mathcal {M}_1 \cup \mathcal {M}_2= & {} \big (Q,\varSigma ,q_0,\delta , (F_1 \times Q_2) \cup (Q_1 \times F_2) \big ) \end{aligned}$$

are also Mojmir automata, and moreover $\mathsf {L}(\mathcal {M}_1 \cap \mathcal {M}_2) = \mathsf {L}(\mathcal {M}_1) \cap \mathsf {L}(\mathcal {M}_2)$ and $\mathsf {L}(\mathcal {M}_1 \cup \mathcal {M}_2) = \mathsf {L}(\mathcal {M}_1) \cup \mathsf {L}(\mathcal {M}_2)$.

5.1 A compositional construction: intuition

We present the intuition behind the construction by means of an example. Consider the formula

$$\begin{aligned} \varphi = {\mathbf {F}}{\mathbf {G}}({\mathbf {F}}a \vee ({\mathbf {G}}(a\vee {\mathbf {F}}b) \wedge c))) \end{aligned}$$

We use the abbreviations $\psi _2 = a \vee {\mathbf {F}}b$ and $\psi _1 = {\mathbf {F}}a \vee ({\mathbf {G}}\psi _2 \wedge c)$, and so we also refer to the formula as ${\mathbf {F}}{\mathbf {G}}\psi _1$.

We cannot directly apply the construction of the last section because ${\mathbf {F}}{\mathbf {G}}\psi _1$ contains the ${\mathbf {G}}$-subformula ${\mathbf {G}}\psi _2$. However, since $\psi _2$ does not contain any ${\mathbf {G}}$-subformula, we can construct a Mojmir automaton $\mathcal {M}(\psi _2)$ for ${\mathbf {F}}{\mathbf {G}}\psi _2$. We use this fact to define the automaton $\mathcal {M}(\psi _1)$ as the union of two Mojmir automata: The first automaton recognizes all words satisfying ${\mathbf {F}}{\mathbf {G}}\psi _1$ but not ${\mathbf {F}}{\mathbf {G}}\psi _2$ (and perhaps some other words satisfying ${\mathbf {F}}{\mathbf {G}}\psi _2$), while the second recognizes all words satisfying ${\mathbf {F}}{\mathbf {G}}\psi _1$ and ${\mathbf {F}}{\mathbf {G}}\psi _2$ (and perhaps some other words satisfying ${\mathbf {F}}{\mathbf {G}}\psi _1$). Consider for example the words

$$\begin{aligned} w_1 = (a{\bar{b}}{\bar{c}} \ {\bar{a}}{\bar{b}}c)^\omega \qquad w_2 = ({\bar{a}}bc)^\omega \qquad w_3 = ({\bar{a}}{\bar{b}}c)^\omega \end{aligned}$$

We have $w_1 \models {\mathbf {F}}{\mathbf {G}}\psi _1 \wedge \lnot {\mathbf {F}}{\mathbf {G}}\psi _2$, $w_2 \models {\mathbf {F}}{\mathbf {G}}\psi _1 \wedge {\mathbf {F}}{\mathbf {G}}\psi _2$ and $w_3 \not \models {\mathbf {F}}{\mathbf {G}}\psi _1$. So both automata will reject $w_3$. Moreover, the first automaton will accept $w_1$, and the second $w_2$.

The first automaton, called $\mathcal {M}(\psi _1, \emptyset )$ in Sect.  5.2 below, is just the Mojmir automaton for the formula ${\mathbf {F}}{\mathbf {G}}\psi _1[{\mathbf {G}}\psi _2 / {\mathbf {ff}}]$, i.e., the result of substituting ${\mathbf {G}}\psi _2$ by ${\mathbf {ff}}$ in ${\mathbf {F}}{\mathbf {G}}\psi _1$. It is easy to see that, since $\psi _1$ is in negation normal form, ${\mathbf {F}}{\mathbf {G}}\psi _1[{\mathbf {G}}\psi _2/{\mathbf {ff}}]$ logically implies ${\mathbf {F}}{\mathbf {G}}\psi _1$, and so every word accepted by $\mathcal {M}(\psi _1, \emptyset )$ satisfies ${\mathbf {F}}{\mathbf {G}}\psi _1$. Moreover, observe that if a word w does not satisfy ${\mathbf {F}}{\mathbf {G}}\psi _2$, then the formula ${\mathbf {G}}\psi _2$ is false for every suffix $w_i$ of w, and so, intuitively, treating ${\mathbf {F}}{\mathbf {G}}\psi _2$ as false still allows $\mathcal {M}(\varphi , \emptyset )$ to accept all words ${\mathbf {F}}{\mathbf {G}}\psi _1$ but not ${\mathbf {F}}{\mathbf {G}}\psi _2$. The automaton $\mathcal {M}(\varphi , \emptyset )$ that treats ${\mathbf {G}}\psi _2$ as ${\mathbf {ff}}$ is shown in Fig. 5. To observe the effect of “treating ${\mathbf {G}}\psi _2$ as ${\mathbf {ff}}$”, consider state $\psi _1$ and the letter ${\bar{a}}bc$. If we used the function ${ af}$ as transition relation, then we would obtain the transition $\psi _1 \mathop {\longrightarrow }\limits ^{{\bar{a}}bc} {\mathbf {F}}a \vee ({\mathbf {G}}\psi _2 \wedge {\mathbf {F}}b)$. Instead, since ${\mathbf {G}}\psi _2$ is treated as ${\mathbf {ff}}$, we get $\psi _1 \mathop {\longrightarrow }\limits ^{{\bar{a}}bc} {\mathbf {F}}a$.

Fig. 5

Mojmir automaton for words satisfying ${\mathbf {F}}{\mathbf {G}}\psi _1$ but not ${\mathbf {F}}{\mathbf {G}}\psi _2$

The second automaton is the intersection of two Mojmir automata. The first one is $\mathcal {M}(\psi _2)$, the Mojmir automaton for $\psi _2$, which guarantees that the intersection only accepts words satisfying ${\mathbf {F}}{\mathbf {G}}\psi _2$. The second one, which will be called $\mathcal {M}(\psi _1, \{\psi _2\})$ in Sect. 5.2, is intuitively in charge of checking that a word w satisfies ${\mathbf {F}}{\mathbf {G}}\psi _1$ assuming that it satisfies ${\mathbf {F}}{\mathbf {G}}\psi _2$. Both automata are shown in Fig. 6. We choose $\mathcal {M}(\psi _1, \{\psi _2\})$ as the Mojmir automaton for ${\mathbf {F}}{\mathbf {G}}\psi _1[{\mathbf {G}}\psi _2/{\mathbf {tt}}]$. At first sight, since ${\mathbf {F}}{\mathbf {G}}\psi _2$ and ${\mathbf {G}}\psi _2$ are not equivalent, replacing ${\mathbf {G}}\psi _2$ by ${\mathbf {tt}}$ looks wrong. Let us see why it is correct. Since ${\mathbf {G}}\psi _2$ eventually holds, the assumption that ${\mathbf {G}}\psi _2$ is true can only be incorrect for a finite time, or, in other words, for a finite number of tokens. Now we observe that the acceptance condition of Mojmir automata is insensitive to the fate of a finite number of tokens: if almost every token eventually reaches the accepting states, then after changing the fate of a finite number of tokens this is still the case, and vice versa. So replacing ${\mathbf {G}}\psi _2$ by ${\mathbf {tt}}$ is correct after all.

Consider state $\psi _1$ of $\mathcal {M}(\psi _1, \{\psi _2\})$. If we used the function ${ af}$ as transition relation, then we would obtain the transition $\psi _1 \mathop {\longrightarrow }\limits ^{{\bar{a}}c} {\mathbf {F}}a \vee {\mathbf {G}}\psi _2$. Since we handle ${\mathbf {G}}\psi _2$ as ${\mathbf {tt}}$, we get $\psi _1 \mathop {\longrightarrow }\limits ^{{\bar{a}}c} {\mathbf {tt}}$ instead.

Fig. 6

The automata $\mathcal {M}(\psi _1,\{\psi _2\})$ and $\mathcal {M}(\psi _2)$

We have thus constructed an automaton for ${\mathbf {F}}{\mathbf {G}}({\mathbf {F}}a \vee ({\mathbf {G}}(a\vee {\mathbf {F}}b) \wedge c))$. To handle formulae ${\mathbf {F}}{\mathbf {G}}\psi$ where $\psi$ has multiple ${\mathbf {G}}$-subformulae ${\mathbf {G}}\psi _1, \ldots , {\mathbf {G}}\psi _n$, possibly nested within each other, we generalize the procedure above, and construct an automaton $\mathcal {M}(\varphi , \mathcal {G})$ for each subset $\mathcal {G}$ of ${\mathbf {G}}$-subformulae. The automaton $\mathcal {M}(\varphi , \mathcal {G})$ accepts all words w such that $w \models \varphi$ and $w \models {\mathbf {F}}{\mathbf {G}}\psi$ for every ${\mathbf {G}}\psi \in \mathcal {G}$. The automaton is an intersection of automata, one for each formula in $\mathcal {G}$. The automaton for ${\mathbf {G}}\psi _i$ handles the ${\mathbf {G}}$-subformulae of $\psi _i$ that belong to $\mathcal {G}$ as ${\mathbf {tt}}$. Observe that circularity assumptions of the form “the automaton for ${\mathbf {G}}\psi _1$ assumes that ${\mathbf {F}}{\mathbf {G}}\psi _2$ holds, and the automaton for ${\mathbf {G}}\psi _2$ assumes that that ${\mathbf {F}}{\mathbf {G}}\psi _1$ holds” are not possible because no two formulae can be subformulae of each other.

The final point is to address the state-explosion problem. In the construction above, the final Mojmir automaton for a formula with ${\mathbf {G}}$-subformulae ${\mathbf {G}}\psi _1, \ldots , {\mathbf {G}}\psi _n$ is the union of $2^n$ Mojmir automata, and has an unacceptably large number of states. Fortunately, we can construct all these automata so that they have exactly the same states and transitions, and only differ on their set of accepting states. The idea is to construct $\mathcal {M}(\psi , \mathcal {G})$ using a different transition function. We replace ${ af}$ by another function ${ af}_{\mathbf {G}}$ that behaves like ${ af}$, except for ${\mathbf {G}}$ subformulae, where we set ${ af}_{\mathbf {G}}({\mathbf {G}}\psi , \nu ) = {\mathbf {G}}\psi$ instead of ${ af}({\mathbf {G}}\psi , \nu )= {\mathbf {G}}\psi \wedge { af}(\psi , \nu )$. Intuitively, we leave the decision whether to handle ${\mathbf {G}}\psi$ as ${\mathbf {tt}}$ or ${\mathbf {ff}}$ “open”. Then, for every set $\mathcal {G}$ we choose the accepting states appropriately: Since $\mathcal {M}(\varphi , \mathcal {G})$ assumes that all the formulae of $\mathcal {G}$ are true, we choose as accepting states those whose corresponding formulae are propositionally implied by $\mathcal {G}$.

In our example, both $\mathcal {M}(\psi _1, \emptyset )$ and $\mathcal {M}(\psi _1, \{\psi _2\})$ are the intersection of the two automata of Fig.  7; they differ only in the accepting states. In the case of $\mathcal {M}(\psi _1, \emptyset )$, the left automaton treats ${\mathbf {G}}\psi _2$ as ${\mathbf {ff}}$, and the right automaton is redundant; therefore, the only accepting state of the left automaton is ${\mathbf {tt}}$, and all states of the right automaton are accepting. In the case of $\mathcal {M}(\psi _1, \{\psi _2\})$, the left automaton on the left treats ${\mathbf {G}}\psi _2$ as ${\mathbf {tt}}$, and the right automaton checks that ${\mathbf {G}}\psi _2$ holds; therefore, the accepting states of the left automaton are ${\mathbf {F}}a \vee {\mathbf {G}}{\mathbf {F}}\psi _2$ and ${\mathbf {tt}}$, and the only accepting state of the right automaton is ${\mathbf {tt}}$.

Fig. 7

Intersections with the same structure equivalent to $\mathcal {M}(\psi _1, \emptyset )$ and $\mathcal {M}(\psi _1, \{\psi _2\}) \cap \mathcal {M}(\phi _2)$

5.2 Logical characterization

In order to formalize the notion of “handling a subformula ${\mathbf {G}}\psi$ as ${\mathbf {tt}}$” we introduce the following definition:

Definition 17

Let $\varphi$ be a formula and $\nu \in 2^{Ap}$. The formula ${ af}_{\mathbf {G}}(\varphi ,\nu )$ is inductively defined as ${ af}(\varphi ,\nu )$, with only this difference:

$$\begin{aligned} { af}_{\mathbf {G}}({\mathbf {G}}\varphi ,\nu ) = {\mathbf {G}}\varphi \qquad (\text{ instead } \text{ of } { af}({\mathbf {G}}\varphi ,\nu ) = { af}(\varphi ,\nu )\wedge {\mathbf {G}}\varphi ). \end{aligned}$$

We define ${ Reach}_{\mathbf {G}}(\varphi )~=~\{ [{ af}_{\mathbf {G}}(\varphi ,w)]_P \mid w \in (2^{Ap})^* \}$.

Example 7

Let $\varphi = \psi {\mathbf {U}}\lnot a$, where $\psi ={\mathbf {G}}(a \wedge {\mathbf {X}}\lnot a)$. We have

$$\begin{aligned} \begin{array}{lclcl} { af}_{\mathbf {G}}(\varphi , \{a\}) &{} = &{} { af}_{\mathbf {G}}(\psi ,\{a\}) \wedge \varphi &{} \equiv _p &{} \psi \wedge \varphi \\ { af}(\varphi , \{a\}) &{} = &{} { af}(\psi ,\{a\}) \wedge \varphi &{} \equiv _p &{} \lnot a \wedge \psi \wedge \varphi \end{array} \end{aligned}$$

The logical characterization theorem will be an easy corollary of Lemma 7 below. Given a formula $\varphi$ and a word w, the lemma characterizes the set of ${\mathbf {G}}$-subformulae of $\varphi$ that eventually hold at a word w, i.e., the subformulae ${\mathbf {G}}\psi$ such that $w \models {\mathbf {F}}{\mathbf {G}}\psi$. If $\varphi$ is of the form ${\mathbf {F}}{\mathbf {G}}\psi$, then clearly $w \models \varphi$ iff the subformula ${\mathbf {G}}\psi$ belongs to this set.

Definition 18

Given a formula $\varphi$, we denote by ${\mathbb {G}}(\varphi )$ the set of ${\mathbf {G}}$-subformulae of $\varphi$, i.e., the subformulae of $\varphi$ of the form ${\mathbf {G}}\psi$. Given a word w, we say that ${\mathbf {G}}\psi \in {\mathbb {G}}(\varphi )$ is eventually true in w if $w \models {\mathbf {F}}{\mathbf {G}}\psi$. We denote the set of eventually true ${\mathbf {G}}$-subformulae of $\varphi$ by $\mathcal {G}_{w}(\varphi )$.

Definition 19

A set of $\mathcal {G}\subseteq {\mathbb {G}}(\varphi )$ is closed for w if $\mathcal {G}\models _P { af}_{\mathbf {G}}(\psi , w_{ij})$ holds for almost all $i \in \mathbb {N}$, almost all $j \ge i$, and for every ${\mathbf {G}}\psi \in \mathcal {G}$.

The following lemma shows that eventually true ${\mathbf {G}}$-subformulae can be characterized using the closed sets.

Lemma 7

Let $\varphi$ be a formula and let w be a word.

• Every set $\mathcal {G}\subseteq {\mathbb {G}}(\varphi )$ closed for w is included in $\mathcal {G}_{w}(\varphi )$.

• $\mathcal {G}_{w}(\varphi )$ is closed for w.

Theorem 7

(Logical characterization theorem III) For every LTL formula ${\mathbf {F}}{\mathbf {G}}\varphi$ and every word w: $w \models {\mathbf {F}}{\mathbf {G}}\varphi$ iff there exists a closed set $\mathcal {G}\subseteq {\mathbb {G}}({\mathbf {F}}{\mathbf {G}}\varphi )$ for w containing ${\mathbf {G}}\varphi$.

Proof

($\Rightarrow$): Assume $w \models {\mathbf {F}}{\mathbf {G}}\varphi$. Then $\varphi \in \mathcal {G}_{w}({\mathbf {F}}{\mathbf {G}}\varphi )$ and by Lemma 7(2) $\mathcal {G}_{w}({\mathbf {F}}{\mathbf {G}}\varphi )$ is closed for w. So we can take $\mathcal {G}= \mathcal {G}_{w}(\varphi )$.

($\Leftarrow$): Assume some $\mathcal {G}\subseteq {\mathbb {G}}({\mathbf {F}}{\mathbf {G}}\varphi )$ containing ${\mathbf {G}}\varphi$ is closed for w. By Lemma 7(1) we have ${\mathbf {G}}\varphi \in \mathcal {G}_{w}({\mathbf {F}}{\mathbf {G}}\varphi )$, and so, by the definition of $\mathcal {G}_{w}({\mathbf {F}}{\mathbf {G}}\varphi )$, we get $w \models {\mathbf {F}}{\mathbf {G}}\varphi$. $\square$

Let us see that the theorem indeed generalizes Theorem 1. If $\varphi$ is a ${\mathbf {G}}$-free formula, then ${\mathbb {G}}({\mathbf {F}}{\mathbf {G}}\varphi )= \{{\mathbf {G}}\varphi \}$. So the only possible choice for $\mathcal {G}$ is $\mathcal {G}= \{{\mathbf {G}}\varphi \}$ and the only possible $\psi$ is $\psi =\varphi$. Further, we have

$$\begin{aligned} \begin{array}{clr} &{} \mathcal {G}\models _P { af}_{\mathbf {G}}(\psi , w_{ij}) \\ \text{ iff } &{} {\mathbf {G}}\psi \models _P { af}_{\mathbf {G}}(\psi , w_{ij}) \\ \text{ iff } &{} \emptyset \models _P { af}_{\mathbf {G}}(\psi , w_{ij}) &{} ({\mathbf {G}}\psi \text{ does } \text{ not } \text{ occur } \text{ in } { af}_{\mathbf {G}}(\psi , w_{ij})\\ \text{ iff } &{} { af}_{\mathbf {G}}(\psi , w_{ij}) \equiv _P {\mathbf {tt}}&{} \\ \text{ iff } &{} { af}(\psi , w_{ij}) \equiv _P {\mathbf {tt}}&{} ({ af}(\psi ,w_{ij})={ af}_{\mathbf {G}}(\psi , w_{ij} \text{ since } \varphi is {\mathbf {G}}-free) \end{array} \end{aligned}$$

So for a ${\mathbf {G}}$-free formula $\varphi$ the theorem states that $w \models {\mathbf {F}}{\mathbf {G}}\varphi$ iff ${ af}(\varphi , w_{ij})\equiv _P {\mathbf {tt}}$ for almost every $i \in \mathbb {N}$ and almost every $j \ge i$.

Let us construct a Mojmir automaton for ${\mathbf {F}}{\mathbf {G}}\varphi$ from Theorem 7. The key is the following simple fact:

For the proof, notice first that (*) implies (**); for the other direction recall that if ${ af}_{\mathbf {G}}(\varphi , w_{ij})\equiv _P {\mathbf {tt}}$ then ${ af}_{\mathbf {G}}(\varphi , w_{ij'})\equiv _P {\mathbf {tt}}$ for every $j' \ge j$.

Now, we observe that (**) has the form of the acceptance condition of a Mojmir automaton. Intuitively, we can reshape it into “for every token $i \in \mathbb {N}$ there exists a time $j \in \mathbb {N}$ such that ${ af}_{\mathbf {G}}(\varphi , w_{ij})\equiv _P {\mathbf {tt}}$”. So we define:

Definition 20

Let $\varphi$ be a formula and let $\mathcal {G}\subseteq {\mathbb {G}}(\varphi )$. The Mojmir automaton of $\varphi$ with respect to $\mathcal {G}$ is $\mathcal {M}(\varphi ,\mathcal {G})=$ $({ Reach}_{\mathbf {G}}(\varphi ), \varphi , { af}_{\mathbf {G}}, F_\mathcal {G})$, where $F_\mathcal {G}$ is the set of formulae $\psi \in { Reach}_{\mathbf {G}}(\varphi )$ such that $\mathcal {G}\models _P \psi$.

As we announced earlier, only the set of accepting states of $\mathcal {M}(\varphi ,\mathcal {G})$ depends on $\mathcal {G}$. The following lemma, proved in the Appendix, shows that $\mathcal {M}(\varphi ,\mathcal {G})$ is indeed a Mojmir automaton, i.e., that states reachable from accepting states are also accepting.

Lemma 8

Let $\varphi$ be a formula and let $\mathcal {G}\subseteq {\mathbb {G}}(\varphi )$. For every $\psi \in { Reach}_{\mathbf {G}}(\varphi )$ and every $\nu \in 2^{Ap}$, if $\mathcal {G}\models _P \psi$ then $\mathcal {G}\models _P { af}_{\mathbf {G}}(\psi ,\nu )$.

Example 8

Let $\varphi = ({\mathbf {G}}\psi ) {\mathbf {U}}\lnot a$, where $\psi =a \wedge {\mathbf {X}}\lnot a$. We have ${\mathbb {G}}(\varphi )=\{{\mathbf {G}}\psi \}$, and so two automata $\mathcal {M}(\varphi , \emptyset )$ and $\mathcal {M}(\varphi , \{{\mathbf {G}}\psi \})$, whose common transition system is shown in Fig. 8. We have one single automaton $\mathcal {M}(\psi , \emptyset )$, shown on the right of the figure. A formula $\psi '$ is an accepting state of $\mathcal {M}(\psi , \emptyset )$ if ${\mathbf {tt}}\models _p \psi '$; and so the only accepting state of this automaton is ${\mathbf {tt}}$. The same holds for $\mathcal {M}(\varphi , \emptyset )$. On the other hand, $\psi '$ is an accepting state of $\mathcal {M}(\varphi , \{{\mathbf {G}}\psi \})$ if ${\mathbf {G}}\psi \models \psi '$, and so both ${\mathbf {G}}\psi$ and ${\mathbf {tt}}$ are accepting states.

Fig. 8

Transition systems of the Mojmir automata for $\varphi =({\mathbf {G}}\psi ){\mathbf {U}}\lnot a$ and for $\psi =a \wedge {\mathbf {X}}\lnot a$

As a corollary of Lemma 7 and Definition 20 we obtain:

Corollary 1

Let $\varphi$ be a formula, w a word, and $\mathcal {G}\subseteq {\mathbb {G}}(\varphi )$.

• If for every ${\mathbf {G}}\psi \in \mathcal {G}$ we have $w \in \mathsf {L}(\mathcal {M}(\psi ,\mathcal {G}))$, then for every ${\mathbf {G}}\psi \in \mathcal {G}$ we have $w \models {\mathbf {F}}{\mathbf {G}}\psi$.

• If for every ${\mathbf {G}}\psi \in \mathcal {G}$ we have $w \models {\mathbf {F}}{\mathbf {G}}\psi$, then for every ${\mathbf {G}}\psi \in \mathcal {G}_{w}(\varphi )$ we have $w \in \mathsf {L}(\mathcal {M}(\psi ,\mathcal {G}_{w}(\varphi )))$.

Moreover, as a particular case:

Theorem 8

Let ${\mathbf {F}}{\mathbf {G}}\varphi$ be a formula and let w be a word. Then $w \models {\mathbf {F}}{\mathbf {G}}\varphi$ iff there is $\mathcal {G}\subseteq {\mathbb {G}}({\mathbf {F}}{\mathbf {G}}\varphi )$ containing ${\mathbf {G}}\varphi$ such that $w \in \mathsf {L}(\mathcal {M}(\psi ,\mathcal {G}))$ for every ${\mathbf {G}}\psi \in \mathcal {G}$.

5.3 The product automaton

Theorem 8 allows us to construct a generalized Rabin automaton for an arbitrary ${\mathbf {F}}{\mathbf {G}}$-formula ${\mathbf {F}}{\mathbf {G}}\varphi$.

Definition 21

Let $\varphi ={\mathbf {F}}{\mathbf {G}}\chi$ be a ${\mathbf {F}}{\mathbf {G}}$-formula, and let ${\mathbb {G}}(\varphi )$ be the set of ${\mathbf {G}}$-subformulae of $\varphi$. For every formula ${\mathbf {G}}\psi \in {\mathbb {G}}(\varphi )$, let $\mathcal {R}(\psi ,\mathcal {G}) =(Q_\psi , q_{0\psi }, \delta _\psi , Acc_\psi ^\mathcal {G})$ be the Rabin automaton obtained by applying Definition 16 to the Mojmir automaton $\mathcal {M}(\psi ,\mathcal {G})$. (Recall that $Q_\psi$, $q_{0\psi }$, and $\delta _\psi$ do not depend on $\mathcal {G}$.)

We define the generalized Rabin automaton automaton $\mathcal {R}(\varphi )$ as

$$\begin{aligned} {{\mathcal {R}}}(\varphi )= \displaystyle \left( \prod _{{\mathbf {G}}\psi \in {\mathbb {G}}(\varphi )} Q_\psi ,\; 2^{Ap},\; \prod _{{\mathbf {G}}\psi \in {\mathbb {G}}(\varphi )} q_{0\psi }, \; \prod _{{\mathbf {G}}\psi \in {\mathbb {G}}(\varphi )} \delta _\psi ,\; \; Acc \right) \end{aligned}$$

where the accepting condition Acc, which expresses “some $\mathcal {G}\subseteq {\mathbb {G}}(\varphi )$ containing ${\mathbf {G}}\psi$ is closed”, is given by

$$\begin{aligned} Acc := \bigvee _{\{\mathcal {G}\subseteq {\mathbb {G}}(\varphi ) \mid {\mathbf {G}}\chi \in \mathcal {G}\}} \; \bigwedge _{{\mathbf {G}}\psi \in \mathcal {G}} Acc_\psi ^{\mathcal {G}} \end{aligned}$$

Since each $Acc_\psi ^\mathcal {G}$ is a Rabin condition, Acc is a generalized Rabin condition. $\mathcal {R}(\varphi )$ can be transformed into an equivalent Rabin automaton using the construction of Sect. 2.3.1. Notice however that, as shown in [10], for many applications it is better to keep the generalized Rabin condition.

Theorem 9

Let $\varphi$ be a ${\mathbf {F}}{\mathbf {G}}$-formula and let w be a word. Then $w \models \varphi$ iff $w \in L(\mathcal {R}(\varphi ))$.

Proof

Assume $\varphi ={\mathbf {F}}{\mathbf {G}}\chi$. By the definition of its accepting condition, $\mathcal {R}(\varphi )$ accepts a word w iff there is a set $\mathcal {G}\subseteq {\mathbb {G}}(\varphi )$ containing ${\mathbf {G}}\chi$ such that $\mathcal {R}(\psi ,\mathcal {G})$ accepts w for every ${\mathbf {G}}\psi \in \mathcal {G}$. By Theorem 6, this is the case iff $\mathcal {M}(\psi , \mathcal {G})$ accepts w for every ${\mathbf {G}}\psi \in \mathcal {G}$. By Theorem 8 this is the case iff $w \models \varphi$. $\square$

Fig. 9

Automata $\mathcal {B}(\varphi )$ and $\mathcal {M}(\psi )$ for $\varphi = b \vee {\mathbf {X}}{\mathbf {G}}\psi$ and $\psi = a \vee {\mathbf {X}}(b {\mathbf {U}}c)$

6 DRAs for arbitrary formulae

In order to explain the last step of our procedure, let $Ap=\{a,b,c\}$ be a set of atomic propositions, and consider the formula $\varphi = b \vee {\mathbf {X}}{\mathbf {G}}\psi$ over Ap, where $\psi = a \vee {\mathbf {X}}(b {\mathbf {U}}c)$. Following the ideas of the previous section, we try to construct an automaton for $\varphi$ as the union of

• (i) an automaton $\mathcal {M}(\varphi , \emptyset )$ accepting all words satisfying $\varphi$ but not ${\mathbf {F}}{\mathbf {G}}\psi$ (plus possibly other words satisfying $\varphi$), and

• (ii) an automaton $\mathcal {M}(\varphi , \{\psi \})$ accepting all words satisfying $\varphi$ and ${\mathbf {F}}{\mathbf {G}}\psi$ (plus possibly other words satisfying $\varphi$).

By the same argument we gave in the previous section, for $\mathcal {M}(\varphi , \emptyset )$ we can take a Mojmir automaton accepting the words satisfying $\varphi [{\mathbf {G}}\psi /{\mathbf {ff}}] = b \vee {\mathbf {X}}{\mathbf {ff}}\equiv b$. We now try to construct $\mathcal {M}(\varphi , \{\psi \})$ as the intersection of two Mojmir automata: $\mathcal {M}(\psi )$, which guarantees that the intersection only accepts words satisfying ${\mathbf {F}}{\mathbf {G}}\psi$, and an automaton that accepts the words satisfying $\varphi$ under the assumption that they satisfy ${\mathbf {F}}{\mathbf {G}}\psi$. The automaton $\mathcal {M}(\psi )$ is shown on the right of Fig. 9. But what can the other automaton be?

We consider the following idea. As transition system of the automaton we take ${{\mathcal {T}}}(\varphi )$ (see Definition 7). This guarantees that the state reached after reading a finite word $w_{0i}$ is ${ af}(\varphi ,w_{0i})$. Further, we choose a co-Büchi accepting condition stating that states $\varphi ' \in { Reach}(\varphi )$ that do not satisfy ${\mathbf {G}}\psi \models _P \varphi '$ occur only finitely often in the run. Then, an accepting run on a word w gets eventually trapped in states satisfying ${\mathbf {G}}\psi \models _P \varphi '$. So, since ${\mathbf {G}}\psi$ eventually holds, for a sufficiently large i we have $w_i \models { af}(\varphi , w_{0i})$, and so by Proposition 2 we have $w \models \varphi$.

Unfortunately, while this reasoning is sound, it is not complete. In our example, this idea leads to the automaton $\mathcal {B}(\varphi )$ shown on the left of Fig. 9. Since we have ${\mathbf {G}}\psi \models _P {\mathbf {tt}}$ and ${\mathbf {G}}\psi \models _P {\mathbf {G}}\psi$, the accepting states of $\mathcal {B}(\varphi )$ are $q_1$ and $q_2$. Consider the word $w = {\bar{a}}{\bar{b}}{\bar{c}} \, ({\bar{a}}bc)^\omega$. We have $w \models \varphi$, but the run for w starts at $q_0$, moves to $q_2$, and then moves to $q_3$ and stays there forever. So w is rejected. The point is that neither $\mathcal {G}= \emptyset$ nor $\mathcal {G}= \{{\mathbf {G}}\psi \}$ satisfy $\mathcal {G}\models _P q_3$.

In the rest of the section we show that this is, however, nearly correct. We construct a correct automaton with the same states and transitions as the one above, but with a modified accepting condition. For this we first interpret this failed attempt in logical terms.

6.1 Logical characterization theorem

Our failed attempt amounts to, given a word w, checking if there is a closed set $\mathcal {G}$ for w satisfying $\mathcal {G}\models _P { af}(\varphi , w_{0j})$ for almost every $j \in \mathbb {N}$. The following proposition summarizes our observation that this condition does not characterize the words satisfying $\varphi$.

Proposition 6

Let $\varphi$ be a formula and w a word. If there exists a set $\mathcal {G}\subseteq {\mathbb {G}}(\varphi )$ such that (1) $\mathcal {G}$ is closed for w and (2) $\mathcal {G}\models _P { af}(\varphi , w_{0j})$ for almost every $j \in \mathbb {N}$, then $w \models \varphi$. However, the converse does not hold.

Proof

Assume such a $\mathcal {G}$ exists. Since $\mathcal {G}$ is closed for w, by Lemma 7(b) we have $w \models {\mathbf {F}}{\mathbf {G}}\psi$ for every ${\mathbf {G}}\psi \in \mathcal {G}$, and so there exists an index $i \in \mathbb {N}$ such that $w_j \models \mathcal {G}$ for every $j \ge i$. By (2), we have $\mathcal {G}\models _P { af}(\varphi , w_{0j})$ for some $j \ge i$ and hence $w_j \models { af}(\varphi , w_{0j})$. Finally, by Proposition 2, $w \models \varphi$.

The converse does not hold due to the previous example where neither $\mathcal {G}= \emptyset$ nor $\mathcal {G}= \{{\mathbf {G}}\psi \}$ satisfy $\mathcal {G}\models _P { af}(\varphi , w_{0i})$. $\square$

In the rest of the section we weaken condition (2) of Proposition 6 so that the converse also holds, thus yielding a logical characterization theorem that generalizes Theorem 7. More precisely, our goal is to find an adequate formula $\mathcal {F}(\mathcal {G}, w_{0j})$ such that after replacing condition (2) by

$$\begin{aligned} (2*) \quad \mathcal {G}\wedge \mathcal {F}(\mathcal {G}, w_{0j}) \models _P { af}(\varphi , w_{0j})\quad \hbox { for almost every } j \in \mathbb {N}. \end{aligned}$$

both Proposition 6 and its converse hold. Observe that we replace $\mathcal {G}$ by the stronger formula $\mathcal {G}\wedge \mathcal {F}(\mathcal {G}, w_{0j})$, which makes the propositional implication easier to satisfy.

6.1.1 A first candidate for $\mathcal {F}(\mathcal {G}, w_{0j})$

The formula $\mathcal {F}(\mathcal {G}, w_{0j})$ should satisfy $w_j \models \mathcal {F}(\mathcal {G}, w_{0j})$ for almost every $j \in \mathbb {N}$, because then we can still prove that (1) and (2*) imply $w \models \varphi$ using the same proof as in Proposition 6. So we search for a formula satisfying this condition.

Let us examine the closure condition in more detail. Given ${\mathbf {G}}\psi \in \mathcal {G}$, it states that for almost all $i \in \mathbb {N}$ we have $\mathcal {G}~\models _P~{ af}_{\mathbf {G}}(\psi , w_{ij})$ for almost all $j \ge i$. So there is a smallest index i such that $\mathcal {G}\models _P { af}_{\mathbf {G}}(\psi , w_{ij})$ holds for almost every $j \ge i$. We give it a name, and define a first candidate for $\mathcal {F}(\mathcal {G}, w_{0j})$.

Definition 22

Let $\varphi$ be a formula and let w be a word. Let $\mathcal {G}\subseteq {\mathbb {G}}(\varphi )$ be closed for w and let ${\mathbf {G}}\psi \in \mathcal {G}$. The threshold $thr _w(\psi ,\mathcal {G})$ of $\psi$ in $\mathcal {G}$ is the smallest index i such that $\mathcal {G}\models _P { af}_{\mathbf {G}}(\psi , w_{jk})$ holds for every $j \ge i$ and almost all $k \ge j$. Further, we define

$$\begin{aligned} \mathcal {F}_1(\psi , \mathcal {G}, w_{0j})= & {} \bigwedge _{i = thr _w(\psi ,\mathcal {G}) }^j { af}_{\mathbf {G}}(\psi , w_{ij}) \\ \mathcal {F}_1(\mathcal {G}, w_{0j})= & {} \bigwedge _{{\mathbf {G}}\psi \in \mathcal {G}} \mathcal {F}_1(\psi , \mathcal {G}, w_{0j}) \end{aligned}$$

Recall that $w_{ij}=\epsilon$ if $i \ge j$ by definition. Since ${ af}_{\mathbf {G}}(\psi , \epsilon )=\psi$, we can also define

$$\begin{aligned} \mathcal {F}_1(\psi , \mathcal {G}, w_{0j}) = \left\{ \begin{array}{ll} \psi &{} \text{ if } j=0 \\ \psi \wedge \bigwedge _{i = thr _w(\psi ,\mathcal {G}) }^{j-1} { af}_{\mathbf {G}}(\psi , w_{ij}) &{} \text{ if } j>0 \end{array}\right. \end{aligned}$$

Example 9

Consider the formula $\varphi = b \vee {\mathbf {X}}{\mathbf {G}}\psi$ and $\psi =a \vee {\mathbf {X}}(b{\mathbf {U}}c)$ and let $\mathcal {G}= \{{\mathbf {G}}\psi \}$. For $w = (a{\overline{b}}{\overline{c}})^\omega$ we have ${ af}_{\mathbf {G}}(\psi , w_{ij})= {\mathbf {tt}}$ for every $0 \le i < j$. So $\mathcal {G}$ is closed for w. Further we have $thr _w(\psi ,\mathcal {G}) = 0$, and so $\mathcal {F}_1(\psi ,\mathcal {G}, w_{0j})= \psi$ for every $j \ge 0$.

For $w = ({\overline{a}}{\overline{b}}c)^\omega$ we have ${ af}_{\mathbf {G}}(\psi , w_{i(i+1)})= b {\mathbf {U}}c$ for every $i \ge 0$, and ${ af}_{\mathbf {G}}(\psi , w_{ij})= {\mathbf {tt}}$ for every $j > i+1 \ge 1$. So $\mathcal {G}$ is closed for w. Further we have $thr _w(\psi ,\mathcal {G}) = 0$, and so

$$\begin{aligned} \mathcal {F}_1(\psi , \mathcal {G}, w_{0j}) = \left\{ \begin{array}{ll} \psi &{} \text{ if } j = 0 \\ \psi \wedge b {\mathbf {U}}c &{} \text{ if } j>0 \end{array}\right. \end{aligned}$$

For $w={\overline{a}}bc (ab{\overline{c}})^\omega$ we have ${ af}_{\mathbf {G}}(\psi , w_{0j})= b {\mathbf {U}}c$ for all $j > 0$ and ${ af}_{\mathbf {G}}(\psi , w_{ij})= {\mathbf {tt}}$ for all other pairs $j > i$. So $\mathcal {G}$ is closed for w. Further we have $thr _w(\psi ,\mathcal {G}) = 1$, because ${\mathbf {G}}\psi \not \models _P { af}_{\mathbf {G}}(\psi , w_{0j}) = b {\mathbf {U}}c$ for all $j > 0$. So $\mathcal {F}_1(\psi , \mathcal {G}, w_{0j})= \psi$ for every $j \ge 0$.

Let us prove that our first candidate indeed satisfies $w_j \models \mathcal {G}\wedge \mathcal {F}_1(\mathcal {G}, w_{0j})$ for almost every j.

Lemma 9

Let $\varphi$, w, $\mathcal {G}$ and ${\mathbf {G}}\psi$ as in Definition 22. Then $w_j \models \mathcal {G}\wedge \mathcal {F}_1(\mathcal {G}, w_{0j})$ for almost every $j \in \mathbb {N}$

Proof

By the semantics of LTL, there exists an index k such that for every ${\mathbf {G}}\psi \in {\mathbb {G}}(\varphi )$ either $w_{k} \models {\mathbf {G}}\psi$ or $w_{k} \not \models {\mathbf {F}}{\mathbf {G}}\psi$ holds. We say that ${\mathbb {G}}(\varphi )$ stabilizes at k. By Theorem 7, we further have $w_k \models \mathcal {G}$. So $w_j \models \mathcal {G}$ for every $j \ge k$. We now show that $w_j \models { af}_{\mathbf {G}}(\psi , w_{ij})$ holds for every $j \ge k$, every ${\mathbf {G}}\psi \in \mathcal {G}$, and every $i \ge thr _w(\psi ,\mathcal {G})$, which concludes the proof. We consider two cases. If $\mathcal {G}\models _P { af}_{\mathbf {G}}(\psi , w_{ij})$ holds, then the claim follows from $w_k \models \mathcal {G}$. If $\mathcal {G}\not \models _P { af}_{\mathbf {G}}(\psi , w_{ij})$ then, since $i \ge thr _w(\psi ,\mathcal {G})$, there exists $j' > j$ such that $\mathcal {G}\models _P { af}_{\mathbf {G}}(\psi , w_{ij'})$. Since $j' \ge k$, we have $w_{j'} \models \mathcal {G}$, and so $w_{j'} \models { af}_{\mathbf {G}}(\psi , w_{ij'}) = { af}_{\mathbf {G}}({ af}_{\mathbf {G}}(\psi , w_{ij}),w_{jj'})$. It remains to show that $w_{j'} \models { af}_{\mathbf {G}}({ af}_{\mathbf {G}}(\psi , w_{ij}),w_{jj'})$ implies $w_j \models { af}_{\mathbf {G}}(\psi , w_{ij})$. The proof is by structural induction on the structure of $\psi$. All cases are identical to those of Proposition 2, with the exception of $\psi = {\mathbf {G}}\psi '$. If $\psi = {\mathbf {G}}\psi '$ we have ${ af}_{\mathbf {G}}({ af}_{\mathbf {G}}(\psi , w_{ij}),w_{jj'}) = { af}_{\mathbf {G}}(\psi , w_{ij}) = {\mathbf {G}}\psi '$, and so we have to prove that $w_{j'} \models {\mathbf {G}}\psi '$ implies $w_j \models {\mathbf {G}}\psi$. Since $j' > j$, this does not seem at first to be the case, but recall that we have $j' > j \ge k$ by hypothesis; since ${\mathbb {G}}(\varphi )$ stabilizes at k, the two suffixes $w_{j'}$ and $w_j$ satisfy the same formulae of ${\mathbb {G}}(\varphi )$, and we are done. $\square$

Unfortunately, our first candidate is not good enough for a logical characterization: we can find a formula $\varphi$ and a word w such that $w \models \varphi$ but no set $\mathcal {G}$ satisfies conditions (1) and (2*).

Example 10

Let $\varphi = {\mathbf {G}}\psi$, where $\psi ={\mathbf {X}}a \vee {\mathbf {G}}b$, and $w=a^\omega$. We have $w \models \varphi$. The only non-empty set closed for w is $\mathcal {G}= \{ \varphi \}$. However, for this $\mathcal {G}$ condition (2*) does not hold. Indeed, we have

$$\begin{aligned} \begin{array}{rcll} { af}_{\mathbf {G}}(\psi , w_{ij}) &{} = &{} a \vee {\mathbf {G}}b &{}\quad \text{ for } \text{ every } j = i + 1 \\ { af}_{\mathbf {G}}(\psi , w_{ij}) &{} = &{} {\mathbf {tt}}&{}\quad \text{ for } \text{ every } j> i + 1 \\ { af}(\varphi , w_{0j}) &{} = &{} \varphi \wedge a &{}\quad \text{ for } \text{ every } j > i \ge 1 \end{array} \end{aligned}$$

and so (2*) holds only if $\varphi \wedge (a \vee {\mathbf {G}}b) \models _P \varphi \wedge a$, which is not the case.

6.1.2 A second (and correct) candidate

Observe that, intuitively, if both (1) and (2*) hold, then w satisfies $\varphi$ even if it does not satisfy any of the formulae of ${\overline{\mathcal {G}}} = {\mathbb {G}}(\varphi ) \setminus \mathcal {G}$. Using this, we show that Lemma 9 still holds if we strengthen $\mathcal {F}_1(\mathcal {G}, w_{0i})$ by, loosely speaking, replacing occurrences of formulae of ${\overline{\mathcal {G}}}$ by ${\mathbf {ff}}$. Let us define this formula $\mathcal {F}(\mathcal {G}, w_{0i})$, our final candidate.

Definition 23

Let $\varphi$, w, $\mathcal {G}$, and ${\mathbf {G}}\psi$ as in Definition 22, and let ${\overline{\mathcal {G}}} = {\mathbb {G}}(\varphi ) \setminus \mathcal {G}$. We define

$$\begin{aligned} \mathcal {F}(\psi , \mathcal {G}, w_{0j})= & {} \mathcal {F}_1(\psi , \mathcal {G}, w_{0j})[{\overline{\mathcal {G}}}/{\mathbf {ff}}]_P \\ \mathcal {F}(\mathcal {G}, w_{0i})= & {} \bigwedge _{{\mathbf {G}}\psi \in \mathcal {G}} \mathcal {F}(\psi , \mathcal {G}, w_{0i}) \end{aligned}$$

Example 11

In Example 10 we have $\mathcal {G}= \{\varphi \}$, hence ${\overline{\mathcal {G}}} = \{{\mathbf {G}}b\}$. So $\mathcal {F}(\psi , w_{0i}) = (a \vee {\mathbf {G}}b)[\{{\mathbf {G}}b\}/ {\mathbf {ff}}]_P = a$, and now condition (2*) holds.

For the three words of Example 9 we have $\mathcal {G}= {\mathbb {G}}(\varphi )$, and so $\mathcal {F}(\psi , w_{0i})=\mathcal {F}_1(\psi , w_{0i})$.

Lemma 10

Let $\varphi$, w, $\mathcal {G}$ and ${\mathbf {G}}\psi$ be as in Definition 22. Then $w_j \models \mathcal {G}\wedge \mathcal {F}(\mathcal {G}, w_{0i})$ for almost every $j \in \mathbb {N}$.

Proof

The proof is analogous to the proof of Lemma 9 and additionally relies on the following equivalence, which can proven by a straightforward induction on $\psi$.

$$\begin{aligned} \mathcal {G}\models _P { af}_{\mathbf {G}}(\psi [{\overline{\mathcal {G}}}/{\mathbf {ff}}]_P, w_{0i}) \quad \text {if{}f} \quad \mathcal {G}\models _P { af}_{\mathbf {G}}(\psi , w_{0i})[{\overline{\mathcal {G}}}/{\mathbf {ff}}]_P \end{aligned}$$

$\square$

We show that the new candidate indeed yields a logical characterization theorem.

Theorem 10

(Logical characterization theorem IV) Let $\varphi$ be a formula and w a word. Then $w \models \varphi$ iff there exists $\mathcal {G}\subseteq {\mathbb {G}}(\varphi )$ satisfying (1) $\mathcal {G}$ is closed for w, and (2*) $\mathcal {G}\wedge \mathcal {F}(\mathcal {G}, w_{0i}) \models _P { af}(\varphi , w_{0i})$ for almost every $i \in \mathbb {N}$.

Proof

($\Leftarrow$) By (1) and (2*), we have $w_j \models \mathcal {G}\wedge \mathcal {F}(\mathcal {G}, w_{0i})$ and $\mathcal {G}\wedge \mathcal {F}(\mathcal {G}, w_{0j}) \models _P { af}(\varphi , w_{0j})$ for almost every $j \in \mathbb {N}$, which implies $w_j \models { af}(\varphi , w_{0j})$ for almost every $j \in \mathbb {N}$, and therefore $w \models \varphi$.

($\Rightarrow$) Assume $w \models \varphi$. Let $\mathcal {G}_w$ be the set of all formulae ${\mathbf {G}}\psi \in {\mathbb {G}}{\varphi }$ such that $w \models {\mathbf {F}}{\mathbf {G}}\psi$. Then by Lemma 7, $\mathcal {G}_w$ satisfies (1). For (2*), we first consider the special case in which $thr _w(\psi ,\mathcal {G}) = 0$ holds for all ${\mathbf {G}}\psi \in \mathcal {G}_w$, that is, we not only have $w \models {\mathbf {F}}{\mathbf {G}}\psi$ but even $w \models {\mathbf {G}}\psi$ for every $\psi \in \mathcal {G}_w$. Then, by the same reasoning as in the proof of Theorem 7, we obtain that $\mathcal {G}_\varphi \models _P { af}_{\mathbf {G}}(\varphi , w_{0j})$ holds for almost all $j \in \mathbb {N}$. So, after unfolding the definition of $\mathcal {F}(\mathcal {G}_\varphi , w_{0j})$, it remains to show that for almost all $j \in \mathbb {N}$:

$$\begin{aligned} { af}_{\mathbf {G}}(\varphi , w_{0j})[{\overline{\mathcal {G}_w}}/{\mathbf {ff}}]_P \; \wedge \; \bigwedge _{{\mathbf {G}}\psi \in \mathcal {G}_w} \left( {\mathbf {G}}\psi \wedge \bigwedge _{i = 0}^j { af}_{\mathbf {G}}(\psi , w_{ij})[{\overline{\mathcal {G}_w}}/{\mathbf {ff}}]_P \right) \models _P { af}(\varphi , w_{0j}) \end{aligned}$$

which is proven by a straightforward induction on $\varphi$. We consider only two sample cases:

• $\varphi = a$. Since $\varphi = a$ does not have any ${\mathbf {G}}$-subformulae, the conjunction over all $\mathcal {G}_w$ on the left hand side is simply ${\mathbf {tt}}$ and also the propositional substitution has no effect. After simplification we obtain ${ af}_{\mathbf {G}}(a, w_{0j}) \models _P { af}(a, w_{0j})$ which is true.

• $\varphi = {\mathbf {G}}\varphi '$. In the case ${\mathbf {G}}\varphi ' \not \in \mathcal {G}_w$, the left-hand side is propositionally equal to ${\mathbf {ff}}$ and hence the claim holds. Thus assume ${\mathbf {G}}\varphi ' \in \mathcal {G}_w$. Let us now examine the right-hand side:

  $$\begin{aligned} { af}({\mathbf {G}}\varphi ', w_{0i}) = {\mathbf {G}}\varphi ' \wedge \bigwedge _{0 = i}^j{{ af}(\varphi ', w_{ij})} \end{aligned}$$

  Since ${\mathbf {G}}\varphi ' \in \mathcal {G}_w$, the first conjunct is implied by the left-hand side. Let now ${ af}(\varphi ', w_{ij})$ be an arbitrary conjunct of the right-hand side. Then there is a matching ${ af}_{\mathbf {G}}(\varphi ', w_{ij})[{\overline{\mathcal {G}_w}}/{\mathbf {ff}}]_P$ on the left-hand side. We now apply the induction hypothesis on this pair and obtain that ${ af}(\varphi ', w_{ij})$ is propositionally entailed by the whole left-hand side. Applying this idea to all conjuncts yields the claim.

Let us now consider the general case. Let k be the maximum of $thr _w(\psi ,\mathcal {G})$ for elements of $\mathcal {G}_w$. Then we have $w_k \models {\mathbf {G}}\psi$ for every $\psi \in \mathcal {G}_w$. Let $\varphi ' = { af}(\varphi , w_{0k})$. By Proposition 2, we have $w_k \models \varphi '$, and we can apply the reasoning above to obtain: for almost every $i \in \mathbb {N}$: $\mathcal {G}\wedge \mathcal {F}_{w_k}(\mathcal {G}, w_{0ki}) \models _P { af}(\varphi ', w_{ki})$. Since $\mathcal {F}(\mathcal {G}, w_{0(k+i)})$ contains all conjuncts of $\mathcal {F}_{w_k}(\mathcal {G}, w_{ki})$, after unfolding the definitions we finally obtain $\mathcal {G}\wedge \mathcal {F}(\mathcal {G}, w_{0i}) \models _P { af}(\varphi , w_{0i})$ for almost every $i \in \mathbb {N}$. $\square$

6.2 From the logical characterization to automata

As in the previous section, we transform the logical characterization into an automaton. For this, we show that $\mathcal {F}(\mathcal {G}, w_{0i})$ is closely related to the ranks at which the automata $\mathcal {M}(\psi , \mathcal {G})$ accept the word w. Loosely speaking, the fact that these automata accept tells us that the formulae of $\mathcal {G}$ eventually hold, and the ranks at which they accept allows us to determine the formula $\mathcal {F}_1(\mathcal {G}, w_{0i})$—and hence also $\mathcal {F}(\mathcal {G}, w_{0i})$—for sufficiently large i. We need a preliminary definition.

Definition 24

Let $\mathcal {M}$ be a Mojmir automaton with set of states $Q_\mathcal {M}$, and let $sr :Q_\mathcal {M}\rightarrow \mathbb {N}$ be a state-ranking that assigns to each state $q \in Q_\mathcal {M}$ a rank sr(q). For every $k \in \mathbb {N}$, we define

$$\begin{aligned} {{\mathcal {S}}}( sr,k) = \{ q \in Q_\mathcal {M}\mid sr(q) \ge k \} \end{aligned}$$

In words: ${{\mathcal {S}}}( sr, k)$ is the set of states that have rank at least k in the state-ranking sr.

Example 12

For a state-ranking

$$\begin{aligned} \begin{array}{cccccccc} q_0 &{} q_1 &{} q_2 &{} q_3 &{} q_4 &{} q_5 &{} q_6 \\ (\mathbf{2} &{} \mathbf{1} &{} \bot &{} \mathbf{4} &{} \mathbf{3} &{} \bot &{} \bot ) \end{array} \end{aligned}$$

we have for example ${{\mathcal {S}}}( sr, 1) = \{q_0, q_1, q_3, q_4 \}$, and ${{\mathcal {S}}}( sr, 3) = \{q_3, q_4 \}$. For the bottom state of the DRA in Fig. 4 (which is a state-ranking of the Mojmir automaton on the left of the figure) we get ${{\mathcal {S}}}( sr, 1)=\{a \vee (b {\mathbf {U}}c), b {\mathbf {U}}c\}$ and ${{\mathcal {S}}}( sr, 2)=\{a \vee (b {\mathbf {U}}c)\}$.

We can now state the theorem. Recall that the Mojmir automaton $\mathcal {M}(\psi ,\mathcal {G})$ was defined in Definition 20, and that the states of its corresponding Rabin automaton $\mathcal {R}(\psi , \mathcal {G})$ are state-rankings for the states of the Mojmir $\mathcal {M}(\psi ,\mathcal {G})$.

Theorem 11

Let $\mathcal {G}\subseteq {\mathbb {G}}(\varphi )$ be closed for w, and let ${\mathbf {G}}\psi \in \mathcal {G}$. For every $i \ge 0$, let sr(i) be the state of $\mathcal {R}(\psi ,\mathcal {G})$ reached after $w_{0i}$ (in other words, $sr(i) = \delta _\psi (q_{0\psi }, w_{0i})$, where $\delta _\psi$ is the transition function of $\mathcal {R}(\psi ,\mathcal {G}))$. Finally, let ${\mathbf {r}}$ be the smallest rank at which $\mathcal {R}(\psi ,\mathcal {G})$ accepts w. Then

$$\begin{aligned} \mathcal {G}\wedge \mathcal {F}_1(\psi , \mathcal {G}, w_{0i}) \equiv _P \mathcal {G}\wedge {{\mathcal {S}}}(sr(i), {\mathbf {r}}) \quad \text{ for } \text{ almost } \text{ every } i \in \mathbb {N}. \end{aligned}$$

Fig. 10

Transition system ${{\mathcal {T}}}(\varphi )$ and automata $\mathcal {M}(\psi )$, and $\mathcal {R}(\psi )$ for $\varphi = b \vee {\mathbf {X}}{\mathbf {G}}\psi$ and $\psi = a \vee {\mathbf {X}}(b {\mathbf {U}}c)$

Before proving the theorem, let us consider an example.

Example 13

Figure 10 shows the transition system ${{\mathcal {T}}}(\varphi )$, the Mojmir automaton $\mathcal {M}(\psi )$, and the DRA $\mathcal {R}(\psi )$ for the formula $\varphi = b \vee {\mathbf {X}}{\mathbf {G}}\psi$ with $\psi = a \vee b {\mathbf {U}}c$ (cf. Fig. 9). The state $(\mathbf {i},\mathbf {j})$ of $\mathcal {R}(\psi )$ indicates that $\psi$ has rank $\mathbf {i}$ and $b{\mathbf {U}}c$ has rank $\mathbf {j}$. We have

$$\begin{aligned} {\textit{fail}} = \{t_3, t_8\} \quad \begin{array}{l} {\textit{merge}}(\mathbf {1}) = \emptyset \\ {\textit{merge}}(\mathbf {2}) = \{t_6\} \end{array} \quad \begin{array}{l} {\textit{succeed}}(\mathbf {1}) = \{t_1, t_5, t_7\} \\ {\textit{succeed}}(\mathbf {2}) = \{t_4, t_7, t_8\} \end{array} \end{aligned}$$

We examine again the three words of Example 9.

Let $w = a^\omega$. The run of $\mathcal {R}(\psi )$ on w is $t_1^\omega$, and so $\mathcal {R}(\psi )$ accepts w at rank $\mathbf {1}$. Recall that $\mathcal {F}_1(\psi ,\mathcal {G}, w_{0i})= \psi$ for every $i \ge 0$. So we have

$$\begin{aligned} \mathcal {G}\wedge \mathcal {F}_1(\mathcal {G}, w_{0i}) = {\mathbf {G}}\psi \wedge \psi \quad \text{ for } \text{ almost } \text{ every } i \in \mathbb {N} \end{aligned}$$

Further, since ${{\mathcal {S}}}( sr(i), 1)$ is the conjunction of the states q of $\mathcal {M}(\psi )$ such that $sr(w_{0i}, q) \ge \mathbf {1}$, and the run of $\mathcal {R}(\psi )$ on w only visits $(\mathbf {1}, \bot )$, we have $sr(i) = (\mathbf {1}, \bot )$ for every $i \ge 0$, and so ${{\mathcal {S}}}( sr(i), 1) = q_1 = \psi$. We get

$$\begin{aligned} \mathcal {G}\wedge {{\mathcal {S}}}( sr(i), 1) = {\mathbf {G}}\psi \wedge \psi \quad \text{ for } \text{ almost } \text{ every } i \in \mathbb {N} \end{aligned}$$

which is indeed propositionally equivalent to $\mathcal {G}\wedge \mathcal {F}_1(\mathcal {G}, w_{0i})$.

Let now $w = c^\omega$. The run of $\mathcal {R}(\psi )$ on w is $t_2t_5^\omega$, and so $\mathcal {R}(\psi )$ accepts w at rank $\mathbf {1}$. But now we have $\mathcal {F}_1(\psi ,\mathcal {G}, w_{0i}) \equiv _P \psi \wedge (b {\mathbf {U}}c)$ for every $i \ge 2$, and so

$$\begin{aligned} \mathcal {G}\wedge \mathcal {F}(\mathcal {G}, w_{0i}) = {\mathbf {G}}\psi \wedge \psi \wedge (b {\mathbf {U}}c) \quad \text{ for } \text{ almost } \text{ every } i \in \mathbb {N} \end{aligned}$$

Since the run of $\mathcal {R}(\psi )$ on w gets trapped in state $(\mathbf {2}, \mathbf {1})$, we have ${{\mathcal {S}}}( sr(i), 1) = \psi \wedge b {\mathbf {U}}c$ for almost every $i \ge 2$, and so

$$\begin{aligned} \mathcal {G}\wedge {{\mathcal {S}}}( sr(i), 1) = {\mathbf {G}}\psi \wedge \psi \wedge (b {\mathbf {U}}c) \quad \text{ for } \text{ almost } \text{ every } i \in \mathbb {N} \end{aligned}$$

Finally, let $w = {\bar{a}}bc \ ab{\bar{c}}^\omega$. The run of $\mathcal {R}(\psi )$ on w is $t_2t_4^\omega$, and so $\mathcal {R}(\psi )$ accepts w at rank $\mathbf {2}$ and not at rank $\mathbf {1}$. We have $\mathcal {F}_1(\psi ,\mathcal {G}, w_{0i})= \psi$ for every $i \ge 1$, and so

$$\begin{aligned} \mathcal {G}\wedge \mathcal {F}_1(\mathcal {G}, w_{0i}) = {\mathbf {G}}\psi \wedge \psi \quad \text{ for } \text{ almost } \text{ every } i \in \mathbb {N} \end{aligned}$$

Further, since the run of $\mathcal {R}(\psi )$ on w gets trapped in state $(\mathbf {2}, \mathbf {1})$, we have ${{\mathcal {S}}}( sr(i), 2) = \psi$ for almost every $i \ge 0$, and so

$$\begin{aligned} \mathcal {G}\wedge {{\mathcal {S}}}( sr(i), 2) = {\mathbf {G}}\psi \wedge \psi \quad \text{ for } \text{ almost } \text{ every } i \in \mathbb {N} \end{aligned}$$

Before proving the theorem we have a closer look at the succeeding tokens of a Mojmir automaton. Assume that a Mojmir automaton accepts a word, and we are given the rank at which the word is accepted. The following lemma (proved in the Appendix) shows that from some moment on whether a token succeeds or not depends only on its birthdate, its current rank, and its current state. Most importantly, all young enough tokens will succeed.

Lemma 11

Let $\mathcal {M}(\psi ,\mathcal {G})$ be the Mojmir automaton for a formula $\psi$. Assume $\mathcal {M}(\psi , \mathcal {G})$ accepts a word w at the smallest accepting rank ${\mathbf {r}}$. For almost every $t \in \mathbb {N}$ and for every token $\tau$ of the run of $\mathcal {M}(\psi ,\mathcal {G})$ on w, the token succeeds iff

• 1. $\tau > t$, or

• 2. ${ sr}_w(t,{ run}_w(\tau ,t)) \ge {\mathbf {r}}$, or

• 3. ${ run}_w(\tau ,t) \in F$.

The proof of the Theorem is based on the crucial insight that each ${ af}_{\mathbf {G}}(\psi , w_{\tau t})$ precisely corresponds to the state that token $\tau$ occupies at time t.

Proof Of Theorem 11

Consider the run of $\mathcal {M}(\psi , \mathcal {G})$ on the word w. Let t be large enough so that

• every token $\tau$ succeeds iff one of the three conditions of Lemma 11 holds, and

• all tokens $\tau < thr _w(\psi ,\mathcal {G})$ that succeed have already reached the set of accepting states of $\mathcal {M}(\psi , \mathcal {G})$.

Let $m \ge t$. We prove $\mathcal {G}\wedge \mathcal {F}_1(\psi , \mathcal {G}, w_{0m}) \equiv _P \mathcal {G}\wedge {{\mathcal {S}}}( sr(m), {\mathbf {r}})$.

($\Rightarrow$): $\mathcal {G}\wedge \mathcal {F}_1(\psi , \mathcal {G}, w_{0m}) \models _P \mathcal {G}\wedge {{\mathcal {S}}}( sr(m), {\mathbf {r}})$.

By definition we have ${{\mathcal {S}}}( sr(m),r) = \{ q \in Q_{\mathcal {M}(\psi , \mathcal {G})} \mid sr_w(m, q) \ge {\mathbf {r}}\}$, and so it suffices to show that $\mathcal {G}\models _P q$ or $\mathcal {F}_1(\psi , \mathcal {G}, w_{0m}) \models _P q$ holds for every $q \in {{\mathcal {S}}}( sr(m), {\mathbf {r}})$. Assume $\mathcal {G}\not \models _P q$. We prove $\mathcal {F}_1(\psi , \mathcal {G}, w_{0m}) \models _P q$.

We position ourselves at time m: when we talk about the rank or the state of a token we mean its rank or state at time m. Since $sr_w(m,q) \ge {\mathbf {r}}$, in particular the state q is ranked, and so every token on state q has rank $sr_w(m, q)$. Let $\tau$ be any of these tokens. By our choice of t, and since $t \le m$, all tokens with rank greater than or equal to ${\mathbf {r}}$ succeed. So $\tau$ succeeds. Moreover, since $\mathcal {G}\not \models _P q$, the state q is not an accepting state of $\mathcal {M}(\psi , \mathcal {G})$, and so $\tau$ has not succeeded yet. So $\tau$ will eventually reach the accepting states of $\mathcal {M}(\psi , \mathcal {G})$ in the future. Moreover, by our choice of t, all tokens born before $thr _w(\psi ,\mathcal {G})$ have already reached the accepting states. So we have $\tau \ge thr _w(\psi ,\mathcal {G})$, and so, by the definition of $\mathcal {F}_1(\psi , \mathcal {G}, w_{0m})$, we get $\mathcal {F}_1(\psi , \mathcal {G}, w_{0m}) \models _P { af}_{\mathbf {G}}(\psi , w_{\tau m})$ (notice that $\tau < m$ because we assume that token $\tau$ was already born at time t). By the definition of the transition system of $\mathcal {M}(\psi , \mathcal {G})$, the equivalence class $[{ af}_{\mathbf {G}}(\psi , w_{\tau m})]_P$ is precisely the state of $\mathcal {M}(\psi , \mathcal {G})$ reached by token $\tau$ at time m, that is, $q = [{ af}_{\mathbf {G}}(\psi , w_{\tau m})]_P$. So $\mathcal {F}_1(\psi , \mathcal {G}, w_{0m}) \models _P q$.

($\Leftarrow$): $\mathcal {G}\wedge {{\mathcal {S}}}( sr(m),{\mathbf {r}}) \models _P \mathcal {G}\wedge \mathcal {F}_1(\psi , \mathcal {G}, w_{0m})$.

By the definition of $\mathcal {F}_1$ it suffices to show that the left-hand-side implies ${ af}_{\mathbf {G}}(\psi , w_{im})$ for every $thr _w(\psi ,\mathcal {G}) \le i \le m$. Without loss of generality we assume $\mathcal {G}\not \models { af}_{\mathbf {G}}(\psi , w_{im})$. Consider the token created at time i. Since it is created after time $thr _w(\psi ,\mathcal {G})$, it will eventually reach the accepting states by the definition of the threshold and succeed. Furthermore, since $i \le m$, one of the three conditions of Lemma 11 with $t=m$ and $\tau =i$ holds. Since i cannot satisfy conditions (1) or (3) ($\mathcal {G}\not \models { af}_{\mathbf {G}}(\psi , w_{im})$), it must satisfy condition (2). So the rank of the state ${ run}_w(i,m)$ at time m is at least ${\mathbf {r}}$, and so it belongs to ${{\mathcal {S}}}( sr(m), {\mathbf {r}})$. But the state ${ run}_w(i,m)$ is the state reached by token i at time m, and so it is equal to $[{ af}_{\mathbf {G}}(\psi , w_{im})]_P$. So $\mathcal {G}\wedge {{\mathcal {S}}}( sr(m), {\mathbf {r}}) \models _P { af}_{\mathbf {G}}(\psi , w_{im})$. $\square$

6.3 The automaton $\mathcal {A}(\varphi )$: informal definition

Let us first recall the structure of the DGRA $\mathcal {R}({\mathbf {F}}{\mathbf {G}}\psi )$ for a ${\mathbf {F}}{\mathbf {G}}$-formula. It is the union of DGRAs $\mathcal {R}(\mathcal {G})$, one for each subset $\mathcal {G}\subseteq {\mathbb {G}}(\varphi )$ containing ${\mathbf {G}}\psi$. Given a set $\mathcal {G}= \{{\mathbf {G}}\psi _1, \ldots , {\mathbf {G}}\psi _n\}$ of ${\mathbf {G}}$-subformulae, $\mathcal {R}(\mathcal {G})$ accepts all words w satisfying $\varphi$ and ${\mathbf {F}}{\mathbf {G}}\psi _1, \ldots , {\mathbf {F}}{\mathbf {G}}\psi _n$. It is defined as the intersection of the DRAs $\mathcal {R}(\psi _1, \mathcal {G}), \ldots , \mathcal {R}(\psi _n, \mathcal {G})$, which have all the same transition systems (i.e., the same states, transitions, and initial state), but differ on their accepting conditions. Recall that each $\mathcal {R}(\psi _i, \mathcal {G})$ can accept at different ranks (as many as the number of accepting pairs in $\mathcal {R}(\psi _i, \mathcal {G})$).

Given an arbitrary formula $\varphi$, we also define its DGRA $\mathcal {A}(\varphi )$ as a union of DGRAs. However, the union now contains an element $\mathcal {R}(\mathcal {G},\mathbf{r})$ for every set $\mathcal {G}= \{ {\mathbf {G}}\psi _1, \ldots , {\mathbf {G}}\psi _n\} \subseteq {\mathbb {G}}(\varphi )$, and for each possible vector $\mathbf{r}=({\mathbf {r}}_1, \ldots , \mathbf r_n)$ of accepting ranks of $\mathcal {R}(\psi _1, \mathcal {G}), \ldots , \mathcal {R}(\psi _n, \mathcal {G})$. For example, if $n=2$ and $\mathcal {R}(\psi _1, \mathcal {G})$ and $\mathcal {R}(\psi _2, \mathcal {G})$ have 3 and 2 accepting pairs, respectively, then instead of one single DGRA $\mathcal {R}(\mathcal {G})$ we have six DGRAs $\mathcal {R}(\mathcal {G},({\mathbf {1}},{\mathbf {1}})), \ldots , \mathcal {R}(\mathcal {G},(\mathbf 3,{\mathbf {2}}))$.

The transition system of $\mathcal {R}(\mathcal {G},\mathbf{r})$ is the product of the transition system ${{\mathcal {T}}}(\varphi )$ and the transition system of $\mathcal {R}(\mathcal {G})$. Recall that ${{\mathcal {T}}}(\varphi )$ has $Reach(\varphi )$ as set of states, and ${ af}$ as transition function. Since, in turn, the transition system of $\mathcal {R}(\mathcal {G})$ is the product of the transition systems of $\mathcal {R}(\psi _1, \mathcal {G}), \ldots , \mathcal {R}(\psi _n, \mathcal {G})$, a state of $\mathcal {R}(\mathcal {G})$ is a tuple $( sr_1, \ldots , sr_n)$, where $sr_i$ is a state-ranking of the formulae of $Reach_{\mathbf {G}}(\psi _i)$, and a state of $\mathcal {R}(\mathcal {G},\mathbf{r})$ is a tuple $(\chi , sr_1, \ldots , sr_n))$, where $\chi \in Reach(\varphi )$.

It remains to describe the accepting condition of $\mathcal {R}(\mathcal {G}, \mathbf{r})$. We say that $\mathcal {R}(\mathcal {G})$ accepts at rank-vector $\mathbf{r}=({\mathbf {r}}_1, \ldots , {\mathbf {r}}_n)$ if each $\mathcal {R}(\psi _i, \mathcal {G})$ accepts at rank ${\mathbf {r}}_i$. Our goal is to design the accepting condition as a conjunction of two conditions guaranteeing that:

• (i) $\mathcal {G}$ is closed (which implies that $\mathcal {R}(\mathcal {G})$ accepts), and moreover $\mathcal {R}(\mathcal {G})$ accepts at rank-vector $\mathbf{r}$, and

• (ii) $\mathcal {R}(\mathcal {G},\mathbf{r})$ eventually stays within states $(\chi , sr_1, \ldots , sr_n)$ satisfying

  $$\begin{aligned} \mathcal {G}\wedge {{\mathcal {S}}}( sr_1, r_1)[{\overline{\mathcal {G}}}/{\mathbf {ff}}]_P \wedge \cdots \wedge {{\mathcal {S}}}( sr_n, r_n)[{\overline{\mathcal {G}}}/{\mathbf {ff}}]_P \models _P \chi \end{aligned}$$

In particular, (i) checks condition (1) of the logical characterization theorem, Theorem 10. Let us now see that (ii) checks condition (2*). By definition, the formula $\chi$ reached after reading a finite prefix $w_{0i}$ of a word w is the formula ${ af}(\varphi , w_{0i})$. Therefore, (ii) is equivalent to

$$\begin{aligned}&\mathcal {G}\wedge ({{\mathcal {S}}}( sr_1(w_{0i}, r_1)) \wedge \cdots \wedge {{\mathcal {S}}}( sr_n(w_{0i}, r_n)))[{\overline{\mathcal {G}}}/{\mathbf {ff}}]_P \models _P { af}(\varphi ,w_{0i})\nonumber \\&\quad \text{ for } \text{ almost } \text{ every } i \in \mathbb {N} \end{aligned}$$

which by Theorem 11 is equivalent after propositional substitution of ${\overline{\mathcal {G}}}$ with ${\mathbf {ff}}$ on both sides to

$$\begin{aligned} \mathcal {G}\wedge \mathcal {F}(\psi , \mathcal {G}, w_{0i}) \models _P { af}(\varphi , w_{0i}) \quad \text{ for } \text{ almost } \text{ every } i \in \mathbb {N} \end{aligned}$$

and so to condition (2*) of the logical characterization theorem.

We still have to express (i) and (ii) as generalized Rabin conditions. Condition (i) is a conjunction of conditions expressing that $\mathcal {R}(\psi _i, \mathcal {G})$ accepts at rank ${\mathbf {r}}_i$ for every $1 \le i \le n$. Let $P_1 \vee \cdots \vee P_{n}$ be the accepting condition of $\mathcal {R}(\psi _i, \mathcal {G})$. Recall that $\mathcal {R}(\psi _i, \mathcal {G})$ accepts at rank ${\mathbf {r}}_i$ if it accepts with the Rabin pair $P_{r_i}$. $P_{r_i} \vee P_{r_i+1} \vee \cdots \vee P_n$. Further, condition (ii) is a co-Büchi condition, which is a special case of a Rabin condition. So the conjunction of (i) and (ii) is a conjunction of Rabin conditions, and so a generalized Rabin condition.

Observe that condition (i) can be decomposed into a conjunction of conditions, each of which concerns only one of the automata in the product. On the contrary, condition (ii) involves all components of the product, and cannot be decomposed.

As in the case of ${\mathbf {F}}{\mathbf {G}}$-formulae, it remains to deal with the state-explosion problem. Recall that, when we introduced the automata $\mathcal {R}(\psi , \mathcal {G})$, we observed that they can all be constructed so that they all have the same transition system, and therefore the intersection $\mathcal {R}(\mathcal {G})$ has the same transition system as well. Since $\mathcal {R}(\mathcal {G})$ and $\mathcal {R}(\mathcal {G},\mathbf{r})$ have the same transition system, the same happens now.

6.4 The automaton $\mathcal {A}(\varphi )$: formal definition

We conclude the section by giving a precise definition of the automaton $\mathcal {A}(\varphi )$.

Definition 25

Let $\varphi$ be an arbitrary formula, and let ${\mathbb {G}}(\varphi ) = \{{\mathbf {G}}\psi _1, \ldots , {\mathbf {G}}\psi _n\}$ be the set of ${\mathbf {G}}$-subformulae of $\varphi$. For every formula ${\mathbf {G}}\psi _i \in {\mathbb {G}}(\varphi )$, let $\mathcal {R}(\psi _i,\mathcal {G}) =(Q_i, 2^{Ap}, q_{0i}, \delta _i, Acc_i^\mathcal {G})$ be the DRA obtained by applying Definition 16 to the Mojmir automaton $\mathcal {M}(\psi _i,\mathcal {G})$. Recall that a state of $Q_i$ is a state-ranking of the states of $\mathcal {M}(\psi _i,\mathcal {G})$. We use $sr_i$ to denote a state-ranking of $Q_i$.

The DGRA $\mathcal {A}(\varphi ) = (Q_\varphi , 2^{Ap}, q_{0\varphi }, \delta _\varphi , Acc_\varphi )$ is defined as follows:

• $Q_\varphi = { Reach}(\varphi ) \times Q_1 \times \cdots \times Q_n$.

• $q_{0\varphi } = \left( \varphi , q_{01}, \ldots , q_{0n} \right)$.

• $\delta _\varphi ((\chi , sr_{1}, \ldots , sr_{n}), a) = \left( { af}(\chi ,a), \delta _1( sr_1, a), \ldots , \delta _n( sr_n, a)\right)$.

• $Acc_\varphi$ is a disjunction containing a disjunct $Acc^\mathcal {G}_{\mathbf{r}}$ for each pair $(\mathcal {G}, \mathbf{r})$, where $\mathcal {G}\subseteq {\mathbb {G}}(\varphi )$ and $\mathbf{r}$ is a mapping assigning to each $\psi \in \mathcal {G}$ a rank, i.e., a number between $\mathbf {1}$ and the number of Rabin pairs of $\mathcal {R}(\psi ,\mathcal {G})$; each $Acc^\mathcal {G}_{\mathbf{r}}$ is then of the form

  $$\begin{aligned} \displaystyle M^\mathcal {G}_{\mathbf{r}} \wedge \bigwedge _{{\mathbf {G}}\psi \in \mathcal {G}} Acc^{\mathcal {G}}_{\mathbf{r}}(\psi ) \end{aligned}$$

  where $Acc^{\mathcal {G}}_{\mathbf{r}}(\psi )$ denotes the Rabin pair of $\mathcal {R}(\psi ,\mathcal {G})$ with number $\mathbf{r}(\psi )$, and $M^\mathcal {G}_{\mathbf{r}}$ says that transitions taken infinitely often by $\mathcal {A}(\varphi )$ must lead into the following set:

  $$\begin{aligned} \{ (\chi , sr_1, \ldots , sr_n) \in Q_\varphi \mid \mathcal {G}\wedge \bigwedge _{{\mathbf {G}}\psi _i \in \mathcal {G}} {{\mathcal {S}}}( sr_i, \mathbf{r}(\psi _i))[{\overline{\mathcal {G}}}/{\mathbf {ff}}]_P \models _P \chi \}\ . \end{aligned}$$

  Observe that $M^\mathcal {G}_\mathbf{r}$ can be phrased as a co-Büchi condition on transitions. Therefore, the whole condition $Acc_\varphi$ is a generalized Rabin condition.

Example 14

Recall Example 13 illustrated in Fig. 10. The states of $\mathcal {A}(\varphi )$ are pairs $(\chi , sr)$, where $\chi$ is a state of ${{\mathcal {T}}}(\varphi )$ (on the left of the figure) and sr is a state of $\mathcal {R}(\psi )$ (on the right). Rank vectors have only one component, and so we write $\mathbf{r}$ instead of $\mathbf{r}$. Since $\mathcal {R}(\psi )$ has two Rabin pairs, we have $\mathbf{r}=\mathbf {1}$ or $\mathbf{r}=\mathbf {2}$.

For $\mathcal {G}=\emptyset$ we have $Acc^\emptyset _{\mathbf{r}} = M_\mathbf{r}^\emptyset$, and, independently of $\mathbf{r}$, condition $M_\mathbf{r}^\emptyset$ requests that $\mathcal {A}(\varphi )$ eventually stays in states $(\chi , sr)$ satisfying ${\mathbf {tt}}\models \chi$, and so in the set $\{ \, (q_1, sr_0)\, , (q_1, sr_1)\, \}$.

For $\mathcal {G}=\{\psi \}$ we have $Acc^\psi _{\mathbf{r}} = M_\mathbf{r}^\psi \wedge Acc^{\psi }_{\mathbf{r}}$. Condition $Acc^{\psi }_{\mathbf{r}}$ states that $\mathcal {R}(\psi )$ must accept using the pair $P(\mathbf{r})$. Let us now examine $M_\mathbf{1}^\psi$ and $M_\mathbf{2}^\psi$, starting with the latter.

$M_\mathbf {2}^\psi$ requests that $\mathcal {A}(\varphi )$ eventually stays in states $(\chi , sr)$ satisfying ${\mathbf {G}}\psi \wedge {{\mathcal {S}}}(sr, \mathbf {2})[{\overline{\mathcal {G}}}/{\mathbf {ff}}]_P \models _P \chi$. Since ${{\mathcal {S}}}(sr_0, \mathbf {2}) = {\mathbf {tt}}$ and ${{\mathcal {S}}}(sr_1, \mathbf {2}) = \psi$ (see the Mojmir automaton in the middle of the figure), $\mathcal {A}(\varphi )$ must eventually stay in states $(\chi , sr_0)$ satisfying ${\mathbf {G}}\psi \models _P \chi$ or states $(\chi , sr_1)$ satisfying ${\mathbf {G}}\psi \wedge \psi \models _P \chi$, and so in the states $\{q_1, q_2\} \times \{ sr_0, sr_1 \}$.

$M_\mathbf {1}^\psi$ requests that $\mathcal {A}(\varphi )$ eventually stays in states $(\chi , sr)$ satisfying ${\mathbf {G}}\psi \wedge {{\mathcal {S}}}(sr, \mathbf {1})[{\overline{\mathcal {G}}}/{\mathbf {ff}}]_P \models _P \chi$. Since ${{\mathcal {S}}}(sr_1, \mathbf {1})=\{p_0, p_1\} = \psi \wedge (b {\mathbf {U}}c)$, we have ${\mathbf {G}}\psi \wedge {{\mathcal {S}}}(sr_1, \mathbf {1})[{\overline{\mathcal {G}}}/{\mathbf {ff}}]_P \models _P \chi$ for $\chi = {\mathbf {G}}\psi \wedge (b {\mathbf {U}}c)$, the formula of state $q_3$. So $\mathcal {A}(\varphi )$ must eventually stay in the set $(\{q_1, q_2\} \times \{ sr_0, sr_1 \}) \cup \{ (q_3, sr_1)\}$.

We now proceed to our final result.

Theorem 12

For any LTL formula $\varphi$, $\mathsf {L}(\mathcal {A}(\varphi ))=\mathsf {L}(\varphi )$.

Proof

($\Rightarrow$) By Theorem 10 we only need to prove that if $\mathcal {A}(\varphi )$ accepts w with $\mathcal {G}\subseteq {\mathbb {G}}(\varphi )$ and rank vector $\mathbf{r}$, then (1) $\mathcal {G}$ is closed for w and (2*) $\mathcal {G}\wedge \mathcal {F}(\mathcal {G}, w_{0i}) \models _P { af}(\varphi , w_{0i})$ holds for almost every $i \in \mathbb {N}$. By construction $\mathcal {A}(\varphi )$ only accepts with closed $\mathcal {G}$’s and thus (1) holds. For (2*) we observe that $\mathcal {A}(\varphi )$ also accepts w with the rank vector $\mathbf{r}^*$ that maps every element of $\mathcal {G}$ to the smallest accepting rank for w. So we obtain from $M^\mathcal {G}_{\mathbf{r}^*}$:

$$\begin{aligned} \mathcal {G}\wedge \bigwedge _{{\mathbf {G}}\psi _i \in \mathcal {G}} {{\mathcal {S}}}(sr_i, \mathbf{r}^*(\psi _i))[{\overline{\mathcal {G}}}/{\mathbf {ff}}]_P \models _P { af}(\varphi , w_{0i}) \end{aligned}$$

By Theorem 11 we have $\mathcal {G}\wedge {{\mathcal {S}}}(sr_i, {{\mathbf {r}}}) \models _P \mathcal {G}\wedge \mathcal {F}_1(\mathcal {G}, w_{0i})$ for almost every $i \in \mathbb {N}$, and by propositional substitution of ${\overline{\mathcal {G}}}$ with ${\mathbf {ff}}$ on both sides we conclude that property (2*) holds.

($\Leftarrow$): Let $\mathcal {G}\subseteq {\mathbb {G}}(\varphi )$ be a set satisfying the conditions of Theorem 10, and let $\mathbf{r}$ be the rank vector that maps every element of $\mathcal {G}$ to the corresponding smallest accepting rank. We now prove that $\mathcal {A}(\varphi )$ accepts w with $Acc^\mathcal {G}_{\mathbf{r}}$. Since $\mathcal {G}$ is closed for w, the Rabin pairs $Acc^{\mathcal {G}}_{\mathbf{r}}(\psi )$ are accepting for all ${\mathbf {G}}\psi \in \mathcal {G}$. Hence it remains to show that also $M^\mathcal {G}_{\mathbf{r}}$ is accepting. For this we use the other direction of Theorem 11, i.e., that $\mathcal {G}\wedge \mathcal {F}_1(\mathcal {G}, w_{0i}) \models _P \mathcal {G}\wedge {{\mathcal {S}}}(sr_i, \mathbf {{\mathbf {r}}})$ for almost every $i \in \mathbb {N}$, and propositional substitute ${\overline{\mathcal {G}}}$ with ${\mathbf {ff}}$ on both sides. $\square$

7 Optimizations

The construction described in the previous sections can be optimized in a number of ways. In fact, we have already presented an important optimization: the fact that sink states are not ranked. It is possible to handle sinks just as any other state, but this leads to much larger Rabin automata. Even the toy examples of the paper would then be too large to be drawn.

We implemented further optimizations reducing the number of states or the size of the accepting condition of the automata. Some, but not all, have been mechanically proven. The effect of the optimizations can be seen on examples in Tables 3 and 5.

7.1 Reducing the state space

The first obvious reduction is to construct only the states reachable from the initial states. Further, we merge equivalent states in several ways. Interestingly, this happens based on the formulae that label the states, and not on the graph structure of the automaton, as is the case for, e.g., simulation-based reductions.

Fig. 11

Original and optimized co-Büchi automata for ${\mathbf {F}}{\mathbf {G}}a$

Fig. 12

A co-Büchi automaton for ${\mathbf {G}}{\mathbf {F}}((a\wedge {\mathbf {X}}{\mathbf {X}}a)\vee (\lnot a\wedge {\mathbf {X}}{\mathbf {X}}\lnot a))$ and the optimized automaton inside the grey area (with an arbitrary initial state)

• 1. Unfolding formulae.

  Let the one-step unfolding ${\mathfrak {U}\mathrm {nf}}$ of a formula be inductively defined by the following rules:

  $$\begin{aligned} \begin{array}{rl} {\mathfrak {U}\mathrm {nf}}(a)&{}=a\\ {\mathfrak {U}\mathrm {nf}}(\lnot a)&{}=\lnot a\\ {\mathfrak {U}\mathrm {nf}}(\varphi \wedge \psi )&{}={\mathfrak {U}\mathrm {nf}}(\varphi )\wedge {\mathfrak {U}\mathrm {nf}}(\psi )\\ {\mathfrak {U}\mathrm {nf}}(\varphi \vee \psi )&{}={\mathfrak {U}\mathrm {nf}}(\varphi )\vee {\mathfrak {U}\mathrm {nf}}(\psi ) \end{array} \qquad \begin{array}{rl} {\mathfrak {U}\mathrm {nf}}({\mathbf {X}}\varphi )&{}={\mathbf {X}}\varphi \\ {\mathfrak {U}\mathrm {nf}}({\mathbf {F}}\varphi )&{}={\mathfrak {U}\mathrm {nf}}(\varphi )\vee {\mathbf {F}}\varphi \\ {\mathfrak {U}\mathrm {nf}}({\mathbf {G}}\varphi )&{}={\mathfrak {U}\mathrm {nf}}(\varphi )\wedge {\mathbf {G}}\varphi \\ {\mathfrak {U}\mathrm {nf}}(\varphi {\mathbf {U}}\psi )&{}={\mathfrak {U}\mathrm {nf}}(\psi )\vee ({\mathfrak {U}\mathrm {nf}}(\varphi )\wedge (\varphi {\mathbf {U}}\psi )) \end{array} \end{aligned}$$

  The optimization consists of always using unfolded formulae as states. Note that ${ af}({\mathfrak {U}\mathrm {nf}}(\varphi ),\cdot )={ af}(\varphi ,\cdot )$ since ${ af}$ is ${\mathfrak {U}\mathrm {nf}}$ followed by plugging in the valuation read. Therefore, the only change in the transition system of the automaton is to merge states labelled by $\varphi _1\ne \varphi _2$ such that ${\mathfrak {U}\mathrm {nf}}(\varphi _1)={\mathfrak {U}\mathrm {nf}}(\varphi _2)$. This is an efficient way to under-approximate LTL equivalence by propositional equivalence, which is also easier to check (PSPACE vs. NP), e.g. using BDDs. As a simple example, the optimized automaton for ${\mathbf {F}}{\mathbf {G}}a$ has one state, instead of two states, as illustrated in Fig. 11.

• 2. Different initial states for DRAs.

  Since no finite prefix influences acceptance of Rabin automata for ${\mathbf {F}}{\mathbf {G}}$-formulae, introducing arbitrary initial states for them does not change the accepted language. Therefore, instead of using “transient” states, which cannot be visited once left, we try to use states that are reachable even after reading some prefixes. For instance, consider the formula ${\mathbf {G}}{\mathbf {F}}((a\wedge {\mathbf {X}}{\mathbf {X}}a)\vee (\lnot a\wedge {\mathbf {X}}{\mathbf {X}}\lnot a))$. The automaton, depicted in Fig. 12, corresponds to a buffer keeping track of several last letters read. Without the optimization, we start with an empty buffer; such an initial state of the Rabin automaton has only a single token in the initial state of the Mojmir automaton. Then we read a letter and move to a buffer filled with either a or ${\bar{a}}$. In the next step, we move to a buffer with two letters and from that point switch only among the two-letter buffers. The total size is thus $2^0+2^1+2^2=7$. However, if we start with an already full buffer (filled with whatever letters), the acceptance is not affected, but the reachable state space is only of size $2^2=4$.

• 3. Irrelevant DRAs.

  Recall that a state of our parallel composition is an array of formulae, one corresponding to the current state of the co-Büchi automaton, and the others to the states of the DRAs. We say that a DRA is irrelevant at a state if its corresponding ${\mathbf {G}}$-formula either does not appear inside the current formula of the co-Büchi automaton, or it only appears in conjunction with another formula without any occurrence of ${\mathbf {G}}$. For instance, after reading a in $a\wedge {\mathbf {F}}b \wedge {\mathbf {F}}{\mathbf {G}}c \vee \lnot a\wedge {\mathbf {F}}{\mathbf {G}}d$, the co-Büchi automaton reaches the state ${\mathbf {F}}b\wedge {\mathbf {F}}{\mathbf {G}}c$, where the DRA for the formula d is irrelevant. Consider now ${\mathbf {F}}b \wedge {\mathbf {F}}{\mathbf {G}}c$. At this state the DRA for c is irrelevant, due to the conjunction with ${\mathbf {F}}b$. Intuitively, the co-Büchi automaton waits for a b, and only after that it is important to monitor the satisfaction of ${\mathbf {F}}{\mathbf {G}}c$. Indeed, postponing the monitoring by finite time does not affect acceptance, similarly to the previous optimization. Moreover, if b never holds, then it is unnecessary to check satisfaction of ${\mathbf {F}}{\mathbf {G}}c$.

7.2 Reducing the acceptance condition

All disjuncts of a generalized Rabin condition are of the form $(F,\bigwedge _{k\in K} I_k)$, which we call a generalized pair. We consider a transition-based condition and denote the set of all transitions by T. We remove generalized pairs that cannot be satisfied, as well as those whose satisfaction implies satisfaction of another pair. In order to detect such pairs, we first simplify them. The optimizations are performed to exhaustion in the following order.

• 1. Remove every generalized pair $(F,{\mathcal {I}})$ such that $F=T$.

  Such pairs never accept, since the whole T cannot be avoided.

• 2. Replace every generalized pair $(F,{\mathcal {I}}\wedge I)$ such that $I\cup F=T$ by $(F,{\mathcal {I}})$.

  If F is visited only finitely often then $T\setminus F\subseteq I$ is visited infinitely often.

• 3. Replace every generalized pair $(F,\bigwedge _{k\in K} I_k)$ by $(F,\bigwedge _{k\in K} I_k\setminus F)$.

  Visiting F infinitely often excludes acceptance.

• 4. Remove every generalized pair $(F,{\mathcal {I}}\wedge \emptyset )$.

  The empty set cannot be visited (infinitely often).

• 5. Replace every generalized pair $(F,{\mathcal {I}}\wedge I\wedge J)$ such that $I\subseteq J$ by $(F,{\mathcal {I}}\wedge I)$.

  If I is visited infinitely often then so is J.

• 6. Remove every generalized pair $(F,\bigwedge _{k\in K} I_k)$ for which there exists $(F',\bigwedge _{k'\in K'} I'_{k'})$ such that $F' \subseteq F$, and for each $k' \in K'$ there is $k\in K$ such that $I_{k} \subseteq I'_{k'}$.

  A run accepted by the unprimed pair is also accepted by the primed pair.

For example, consider the formula $({\mathbf {G}}{\mathbf {F}}(a \wedge {\mathbf {X}}b) \vee {\mathbf {F}}{\mathbf {G}}(b \vee {\mathbf {X}}\lnot a)) \wedge ({\mathbf {G}}{\mathbf {F}}(b \wedge {\mathbf {X}}c) \vee {\mathbf {F}}{\mathbf {G}}(!c \vee {\mathbf {X}}a)) \wedge ({\mathbf {G}}{\mathbf {F}}(b \wedge {\mathbf {X}}{\mathbf {X}}a) \vee {\mathbf {F}}{\mathbf {G}}(\lnot c \vee X \lnot b))$. We start with 4568 pairs and after each phase we are left with 4052, 3715, 1997, 131, 122, and finally 12 pairs, respectively.

8 Complexity bounds

Before discussing the implementation of our construction and experimental results we briefly discuss the worst-case complexity and compare it with that of Safra-based constructions.

Recall that the smallest DRA for an LTL formula of length n may have $\Theta (2^{2^n})$ states. This is the case even for the fragment of LTL containing only conjunction, disjunction and the ${\mathbf {F}}$-operator [33, Theorem 3.8]. Indeed, the paper shows that all DRAs for the formula

$$\begin{aligned} {\mathbf {F}}\bigwedge _{i=1}^n(a_i\vee {\mathbf {F}}b_i) \end{aligned}$$

have a double exponential number of states (in n). This lower bound is essentially matched by LTL-to-DRA translations based on Safra’s construction. These translations first transform $\varphi$ into a NBA of size ${\mathcal {O}}(2^n)$, and then apply Safra’s construction, which runs in $m^{{\mathcal {O}}(m)}$ time and space, for an automaton of size m [11]. The overall complexity is thus

$$\begin{aligned} 2^{n\cdot {\mathcal {O}}(2^n)}=2^{{\mathcal {O}}(2^{n+\log n})} \end{aligned}$$

Besides, the number of Rabin pairs of Safra-based translations is at most ${\mathcal {O}}(m)={\mathcal {O}}(2^n)$.

In our translation of a formula $\varphi$, the set of states of our co-Büchi automaton is ${ Reach}(\varphi )$, and the set of states of our DRAs are state-rankings over ${ Reach}_{\mathbf {G}}(\psi )$ for subformulae $\psi$ of $\varphi$. By Lemma 1, if $\varphi$ has n proper subformulae then both ${ Reach}(\varphi )$ and ${ Reach}_{\mathbf {G}}(\psi )$ have size at most $2^{2^n}$. Since a state-ranking is a permutation of Mojmir states, the resulting DRA contains in the worst-case all permutations. Hence the number of states in the product (co-Büchi automaton and at most n DRAs) is at most

$$\begin{aligned} 2^{2^{n}}\cdot \big ((2^{2^{n}})!\big )^n=2^{2^{{\mathcal {O}}(2^n)}} \end{aligned}$$

Further, each pair corresponds to DRAs accepting at one of less than $2^{2^n}$ ranks, or not accepting at all. Altogether, there are at most $(2^{2^n})^n=2^{2^{{\mathcal {O}}(n)}}$ pairs.

We conjecture that there is a family of formulae for which our construction indeed produces automata of triple exponential size, although we have not yet been able to find one.

Consider now the LTL fragment with syntax

$$\begin{aligned} \begin{array}{rll} \lambda &{} {::=} &{} \lambda \wedge \lambda \mid \lambda \vee \lambda \mid {\mathbf {G}}{\mathbf {F}}\alpha \mid {\mathbf {F}}{\mathbf {G}}\alpha \\ \alpha &{} {::=} &{} a \mid \lnot a \mid \alpha \wedge \alpha \mid \alpha \vee \alpha \\ \end{array} \end{aligned}$$

where $a\in Ap$. This fragment contains many interesting fairness formulae, like those of the family $\bigwedge _{i=1}^n \left( {\mathbf {G}}{\mathbf {F}}\ a_i \rightarrow {\mathbf {G}}{\mathbf {F}}b_i \right)$. Our construction yields DGRAs with only one single state, provided we use the unfolding optimization presented in Sect. 7. Indeed, a simple induction shows that for every formula $\varphi$ in the fragment and for every $\nu \in 2^{Ap}$, we have ${\mathfrak {U}\mathrm {nf}}({ af}(\varphi , \nu )) \equiv _P {\mathfrak {U}\mathrm {nf}}(\varphi )$. Therefore, if we take ${\mathfrak {U}\mathrm {nf}}(\varphi )$ as the initial state, the co-Büchi automaton only has one reachable state. By a similar argument, replacing ${ af}$ by ${ af}_{\mathbf {G}}$, the Mojmir automaton $\mathcal {M}(\psi )$ for a ${\mathbf {G}}$-subformula ${\mathbf {G}}\psi$ also has one single state, and the same holds for its corresponding Rabin automaton. Since every component of the parallel composition only has one state, the same holds for the parallel composition itself. Note that without the unfolding optimization the co-Büchi automaton for $\bigwedge _{i=1}^n {\mathbf {F}}{\mathbf {G}}a_i$ would have $2^n$ states.

9 Implementation and experimental results

9.1 Implementation

The construction is implemented in a tool Rabinizer 3, which was reported on in [34]. It is written in Java and uses JavaBDD to work with formulae as Boolean functions. Furthermore, in order to optimize the construction time, we have implemented a new version 3.1 of the tool.⁷ It uses BDDs also for labelling edges in automata and explores the state space in this more symbolic way rather than examining successors for each valuation separately.

The implementation allows to choose between the mechanically proved construction and switching on any subset of the described optimizations. Furthermore, apart from producing the resulting transition-based generalized Rabin automata, it can also convert the result to state-based automata as well as degeneralize them into Rabin automata.

Finally, there is a choice of output formats: dot format, useful for graphical representation, e.g. by dotty or Graphviz; and the HOA (Hanoi omega-automata) format, the new standard [35], nowadays implemented by other translators as well as PRISM. This allows for linking Rabinizer to PRISM, resulting in a significantly faster probabilistic LTL model checker, see [10, 34].

9.2 Experimental results

We compare the performance of the following tools and methods in terms of the number of states of the resulting automata.

• (L*) ltl2dstar [15] implements and optimizes [26] Safra’s construction [11]. It uses LTL2BA [5] to obtain the non-deterministic Büchi automata (NBA) first. Other translators to NBA may also be used, such as Spot [8] or LTL3BA [7] and in some cases may yield better results (see [27] for comparison thereof), but LTL2BA is recommended by ltl2dstar and is used this way in PRISM [14].

• (R1/2) Rabinizer [18] and Rabinizer 2 [19] implement a direct construction based on [17] for fragments LTL$({\mathbf {F}},{\mathbf {G}})$ and LTL$_{\setminus {\mathbf {G}}{\mathbf {U}}}$ ⁸, respectively. The latter tool is applied here only on formulae not in LTL$({\mathbf {F}},{\mathbf {G}})$.

• (L3) LTL3DRA [36] implements a construction via alternating automata, which is “inspired by [17]” (quoted from [36]) and performs several optimizations.

• (R3) Rabinizer 3.1 performs our new construction. Unless specified otherwise we employ the previously described optimizations. Notice that we produce a state space with a logical structure, which permits many further optimizations; for instance, one could incorporate the suspension optimization of LTL3BA [37].

For L* and R1/2 we produce DRAs (although Rabinizer 2 can also produce DGRAs) with state-based acceptance conditions. For L3 and R3 we produce DGRAs with transition-based acceptance conditions (tDGRAs), which can be directly used for probabilistic model checking without any blow-up [10]. Inapplicability of a tool to a formula is denoted in tables by −. All automata in this section were constructed within a few seconds, with the exception of the larger automata generated by ltl2dstar: it took several minutes for automata over ten thousand states and hours for hundreds of thousands of states. The automaton for $\bigwedge _{i=1}^3({\mathbf {G}}{\mathbf {F}}a_i\rightarrow {\mathbf {G}}{\mathbf {F}}b_i)$ took even more than a day and “?” denotes a time-out after one day.

Table 1 shows formulae of the LTL$({\mathbf {F}},{\mathbf {G}})$ fragment. The upper part comes from BEEM (BEnchmarks for Explicit Model checkers) [38], the lower one from [25] on which ltl2dstar was originally tested [39]. There are overlaps between the two sets. All the formulae were used already in [17, 36]. Although more general, our method usually achieves the same results as the optimized LTL3DRA, outperforming the first two approaches.

Table 1 Experimental results on LTL($\mathbf {F}$,$\mathbf {G}$)-fragment

Table 2 shows formulae of LTL$_{\setminus {\mathbf {G}}{\mathbf {U}}}$ used in [19]. The first part comes mostly from the same sources and [22]. The second part is considered in [19] in order to demonstrate the difficulties of the standard approach to handle

• 1. many ${\mathbf {X}}$-operators inside the scope of other temporal operators, especially ${\mathbf {U}}$, where the DRAs are already quite complex, and

• 2. conjunctions of liveness properties where the efficiency of generalized Rabin acceptance condition may be fully exploited.

Table 2 Experimental results on LTL$_{\setminus {\mathbf {G}}{\mathbf {U}}}$ -fragment

Table 3 contains formulae of the general LTL. The first part contains two randomly picked formulae illustrating the same two phenomena as in the previous table now on general LTL formulae. The second part contains two examples of formulae from a network monitoring project Liberouter.⁹ The third part contains five more complex formulae from Spec Pattern [40].¹⁰ and express the following “after Q until R” properties:

$\varphi _{35}:$ :

${\mathbf {G}}(!q \vee ({\mathbf {G}}p \vee (!p {\mathbf {U}}(r \vee (s \wedge !p \wedge {\mathbf {X}}(!p {\mathbf {U}}t))))))$

$\varphi _{40}:$ :

${\mathbf {G}}(!q \vee (((!s \vee r) \vee {\mathbf {X}}({\mathbf {G}}(!t\vee r) \vee !r {\mathbf {U}}(r\wedge (!t \vee r)))) {\mathbf {U}}(r \vee p) \vee {\mathbf {G}}((!s \vee {\mathbf {X}}{\mathbf {G}}!t))))$

$\varphi _{45}:$ :

${\mathbf {G}}(!q \vee (!s \vee {\mathbf {X}}({\mathbf {G}}!t \vee !r {\mathbf {U}}(r\wedge !t)) \vee {\mathbf {X}}(!r {\mathbf {U}}(r \wedge {\mathbf {F}}p))) {\mathbf {U}}(r \vee {\mathbf {G}}(!s \vee {\mathbf {X}}({\mathbf {G}}!t \vee !r {\mathbf {U}}(r\wedge !t)) \vee {\mathbf {X}}(!r {\mathbf {U}}(t \wedge {\mathbf {F}}p)))))$

$\varphi _{50}:$ :

${\mathbf {G}}(!q \vee (!p \vee (!r {\mathbf {U}}(s \wedge !r \wedge {\mathbf {X}}(!r {\mathbf {U}}t)))) {\mathbf {U}}(r \vee {\mathbf {G}}(!p \vee (s \wedge {\mathbf {X}}{\mathbf {F}}t))))$

$\varphi _{55}:$ :

${\mathbf {G}}(!q \vee (!p \vee (!r {\mathbf {U}}(s \wedge !r \wedge !z \wedge {\mathbf {X}}((!r \wedge !z) {\mathbf {U}}t)))) {\mathbf {U}}(r \vee {\mathbf {G}}(!p \vee (s \wedge !z \wedge {\mathbf {X}}(!z {\mathbf {U}}t)))))$

Here we also compare unoptimized and optimized versions of our construction.

Table 3 Experimental results on general LTL

Table 4 Experimental results on general LTL

Table 4 contains formulae of the general LTL generated randomly by randltl [8]. The first part contains formulae over at most 4 atomic propositions and of length 10 to 20 (before simplifications enforced by randltl). The second part contains formulae over at most 8 atomic propositions and of length 15–50 (before the simplifications). Each part contains 1000 formulae and their negations; time-out per formula was set to 1 minute, using ltlcross [8]. Since the formulae are of general LTL we compare only ltl2dstar and (optimized) Rabinizer 3.1. In addition, we also provide comparison to Spot [8], one of the most efficient tools producing non-deterministic transition-based generalized Büchi automata (the tables displays the percentage of actually non-deterministic automata produced). The table provides the average and maximal number of states per automaton on each set; for the more complex set we also provide the percentage of automata greater than 10, 100, and 1000 states (among the results that did not time out). Finally, we also display the percentage of results smaller than, equal to, and greater than those of Rabinizer 3.1.

9.3 Advantages and limits of the approach

In this section, we focus on formulae with extremely complex acceptance conditions. This is caused by combinations of “infinitary” behaviour, whose satisfaction does not depend on any finite prefix of the word. A typical example is the “fairness”-fragment given by $\lambda$ of Sect. 8. In this case, our DGRA have only one state. While DRA need to remember the last letter read, the transition-based acceptance together with the generalized acceptance condition allow transition-based DGRA not to remember anything. Such formulae are the most difficult for our as well as the traditional determinization approach.

The formulae from Table 5 were used before in [17, 36] and include fairness-like constraints.

Table 5 Experimental results on “fairness”-fragment given by $\lambda$ of Sect. 8

Table 6 shows that it is very beneficial to use the generalized Rabin acceptance. Furthermore, using transition-based acceptance even more states are saved.

Table 6 Experimental comparisons of acceptance conditions

However, when the the automata are used for probabilistic model checking, transition-based acceptance does not improve the results so much. Indeed, although state-based DGRA are larger than their transition-based counterpart tDGRA, the respective product is not much larger (often not at all), see Table 7. For instance, consider the case when the only extra information that DGRA carries in states, compared to tDGRA, is the labelling of the last transition taken. Then this information is absorbed in the product, as the system’s states carry their labelling anyway. Therefore, in this relatively common case for simpler formulae (like the one in Table 7), there is no difference in sizes of products with DGRA and tDGRA.

Table 7 Model checking Pnueli–Zuck mutex protocol with 5 processes (altogether $m=308,800$ states) from the benchmark set [14] for the property that either all processes 1–4 enter the critical section infinitely often, or process 5 asks to enter it only finitely often

Further, notice that the DGRA in Table 7 is larger than the DRA obtained by degeneralization of tDGRA and subsequent transformation to a state-based automaton. However, the product with the DGRA is of the size of the original system, while for DRA it is larger! This demonstrates the superiority of generalized Rabin automata over standard Rabin automata with respect to the product size and thus also computation time, which is superlinear in the size.

Finally, Table 8 compares the running times for the discussed fairness-fragment.

Table 8 Running times for constructing an automaton and its acceptance condition for fairness constraints $\bigwedge _{i=1}^k ({\mathbf {F}}{\mathbf {G}}a_i \vee {\mathbf {G}}{\mathbf {F}}b_i)$ for different k

10 Formalization in Isabelle

We have mechanically verified the proof of correctness of our construction using the Isabelle theorem prover,¹¹ which provides a rich library of formalised mathematics and convenient support for proof development. A detailed introduction can be found in [41]. Similar work was pioneered by the CAVA project,¹² which already verified a range of automata-theoretic algorithms [42]. In fact some of the theories developed in the context of the CAVA project are also reused in our work. The formalization was carried out by one of us, and constituted his Master’s thesis. The formal proof can be found at [43], and consists of around 11,000 lines.

10.1 Relation between formalisation and the content of this paper

The formalization is split into several “theories”. A theory is just a collection of definitions and results, which can reuse results from other theories. Our theories are listed in Table 9.

Table 9 Important theories and their content

For the main definitions, lemmas, and theorems of this paper, Table 10 shows their corresponding name and location in the formalized theories. With the help of this table, interested readers can establish the correspondence between our results and their formal versions. For example, we reproduce here Theorem 7 next to the formal version in the mechanized proof:

Theorem 13

(Logical characterization theorem III) For every LTL formula ${\mathbf {F}}{\mathbf {G}}\varphi$ and every word w: $w \models {\mathbf {F}}{\mathbf {G}}\varphi$ iff there exists a closed set $\mathcal {G}\subseteq {\mathbb {G}}({\mathbf {F}}{\mathbf {G}}\varphi )$ for w containing ${\mathbf {G}}\varphi$.

Table 10 Location of definitions, lemmas and theorems

Note that there are several differences between the formulation of the theorem in the paper and in the formalized theories.

• Unbounded variables such as w and $\varphi$ are implicitly universally quantified.

• The type system automatically deduces the types of w, which is an $\omega$-word, and $\varphi$, which is an LTL formula, using the signature of the operator $\models$. Thus the type annotations are omitted.

• Since we cannot use the whole range of mathematical symbols and notation due to technical constraints, alternative notation is used. In this instance ${\mathbb {G}}$ is replaced by $\mathbf {G}$, and $\mathcal {G}_{w}(\varphi )$ by $\mathcal {G}_{FG}~\varphi ~w$.

The theorem declaration is then followed by the proof body, which is written in the proof language Isar. In every proof step facts are established using the keywords have, hence, show, and thus. These claims then have to be proven using a proof method, such as blast, metis, and auto. Furthermore, we can pass additional facts to these methods using parameters such as intro, dest or via the using keyword. All remaining proof goals, in this case that the right hand side implies the left, are proven with the method behind qed. A detailed explanation of the language is given in [44], while the whole specification can be found in [45].

Note that some definitions and claims, like for instance Proposition 1 and Theorem 3, have no counterpart in the formalisation, as they only illustrate different aspects of the construction, but are not an essential part of it. In the first case, we directly define LTL in negation normal form and do not include a translation method, while in the second case the theorem is just a special case of Theorem 7 and thus left out.

10.2 Merits of the mechanization

While the effort invested in the mechanization of the proof has been very considerable (about 8 person-months of a master student who had taken an introductory course on Isabelle), it has helped to identify several bugs in the construction we presented in [20], the conference paper preceding this one. All but one concerned corner cases that were arguably not very relevant. For example, the translation from a Mojmir to a Rabin automaton was incorrect for the case in which the Mojmir automaton has one single state, which is at the same time an accepting state. However, one bug was more serious. Lemma C of our conference paper was wrong, due to a mistake in the proof. The proof was carried out by induction over the structure of LTL formulae. Since our attempts at mechanizing the proof obviously failed, we repeatedly tried to correct the argument by nesting induction proofs. This process eventually lead to the smallest to us known formula for which the lemma fails: ${\mathbf {G}}({\mathbf {X}}a \vee {\mathbf {G}}{\mathbf {X}}b)$. Observe that the formula is already long enough to have a good chance of surviving random testing. Moreover, testing can only be performed with respect to another tool producing DRAs from formulae, which could itself have a bug, and the test requires to check equivalence of deterministic Rabin automata, which is a complicated task. Finally, we do not know of any reasonable way of certifying an LTL to DRA translation, that is, of making the tool produce a certificate of correctness that can be checked by independent means.

After these experiences, we consider automata-theoretic constructions used in model checking tools to be an area in which mechanized proofs are highly desirable, if not necessary. Many of the constructions are very clever and involved. Moreover, while they often rely on relatively simple intuitions, their correctness proofs often involve detailed case analyses. Since the constructions become part of model checkers, which for the most part are used to find bugs in other systems, bugs in the construction itself can have a multiplying effect. Finally, as mentioned above, there is no simple direct way to test the tools. However, we can take the following indirect approach. Firstly, given a formula $\varphi$, we construct the corresponding automaton ${\mathcal {A}}$. Secondly, we model check the transition system of ${\mathcal {A}}$ against the formula $\phi \longleftrightarrow \rho$ where the LTL formula $\rho$ encodes the acceptance condition of ${\mathcal {A}}$. The translation is correct if and only if the model checking procedure does not find any violation. This approach relies on a verified model checker (for non-probabilistic systems).

11 Conclusions

We have presented the first direct translation from LTL formulae to deterministic Rabin automata able to handle arbitrary formulae. The construction is compositional. Given $\varphi$, we compute (1) a transition system for $\varphi$, automata for each ${\mathbf {G}}$-subformula of $\varphi$, and their parallel composition, and (2) the acceptance condition: we first guess a set of ${\mathbf {G}}$-subformulae that are true (this yields the accepting states of automata for ${\mathbf {G}}$-subformulae), and then guess the ranks (this yields the information for a co-Büchi acceptance condition of the whole product).

The compositional approach together with the logical structure of states open the door to many possible optimizations. Since the automata for ${\mathbf {G}}$-subformulae are typically very small, we can aggressively try to optimize them, knowing that each reduced state in one potentially leads to large savings in the final number of states of the product. So far we have only implemented a few simple optimizations, and we think there is still much room for improvement.

We have provided a mechanized proof of the construction, which has also led to discovery of a serious bug in the original construction [20].

We have conducted a detailed experimental comparison. Our construction outperforms two-step approaches that first translate the formula into a Büchi automaton and then apply Safra’s construction. Finally, we produce a (often much smaller) generalized Rabin automaton, which can be directly used for probabilistic verification, without further translation into a standard Rabin automaton.

Appendix: Technical proofs

Lemma

1 For every formula $\varphi$ and every finite word $w \in (2^{Ap})^*$:

• (1) ${ af}(\varphi , w)$ is a boolean combination of proper subformulae of $\varphi$.

• (2) If ${ af}(\varphi , w) = {\mathbf {tt}}$, then ${ af}(\varphi , ww') = {\mathbf {tt}}$ for every $w' \in (2^{Ap})^*$, and analogously for ${\mathbf {ff}}$.

• (3) If $\varphi _1 \equiv _P \varphi _2$, then ${ af}(\varphi _1, w) \equiv _P { af}(\varphi _2, w)$.

• (4) If $\varphi$ has n proper subformulae, then the set of formulae reachable from $\varphi$ has at most $2^{2^n}$ equivalence classes of formulae with respect to propositional equivalence.

Proof

• (1) By structural induction on $\varphi$.

• (2) Follows immediately from ${ af}({\mathbf {tt}},\nu ) = {\mathbf {tt}}$ and ${ af}({\mathbf {ff}},\nu ) = {\mathbf {ff}}$.

• (3) By (1) every formula $\varphi$ is a positive boolean combination of proper formulae. Since ${ af}$ distributes over $\wedge$ and $\vee$, the formula ${ af}(\varphi , \nu )$ is obtained by applying a simultaneous substitution to the proper formulae. (For example, a proper formula ${\mathbf {G}}\psi$ is substituted by ${ af}(\psi ,\nu ) \wedge {\mathbf {G}}\psi$.) Let $\varphi [S]$ be the result of the substitution. Consider two equivalent formulae $\varphi _1 \equiv _P \varphi _2$. Since we apply the same substitution to both sides, the substitution lemma of propositional logic guarantees $\varphi _1[S] \equiv _P \varphi _2[S]$. So ${ af}(\varphi _1, \nu ) \equiv _P { af}(\varphi _2, \nu )$ for a letter $\nu$. The general case ${ af}(\varphi _1, w) \equiv _P { af}(\varphi _2, w)$ follows by induction on the length of w.

• (4) Follows from (1) and the fact that there are $2^{2^n}$ equivalence classes of boolean formulae with n variables.

$\square$

Proposition

2 Let $\varphi$ be a formula, and let $ww' \in (2^{Ap})^\omega$ be an arbitrary word. Then $ww' \models \varphi$ iff $w' \models { af}(\varphi ,w)$.

Proof

First we prove the property when w is a single letter $\nu$:

$$\begin{aligned} \nu w' \models \varphi \quad \text { if{}f } \quad w' \models { af}(\varphi , \nu ) \end{aligned}$$

(2)

We prove (2) by structural induction on $\varphi$. We only consider two representative cases.

• $\varphi = a$. Then

  $$\begin{aligned} \begin{array}{ll} &{} \nu w' \models a \\ \text{ hence } &{} a \in \nu \\ \text{ hence } &{} { af}(a, \nu ) = {\mathbf {tt}}\\ \text{ hence } &{} w' \models { af}(a, \nu ) \\ \end{array} \quad \begin{array}{llr} &{} \nu w' \not \models a \\ \text{ hence } &{} a \notin \nu &{} \text {(semantics of LTL)} \\ \text{ hence } &{} { af}(a, \nu ) = {\mathbf {ff}}&{} \text {(def. of }{ af}) \\ \text{ hence } &{} w' \not \models { af}(a, \nu ) \\ \end{array} \end{aligned}$$

• $\varphi = {\mathbf {F}}\varphi '$. Then

  $$\begin{aligned} \begin{array}{llr} &{} \nu w' \models {\mathbf {F}}\varphi ' \\ \text{ iff } &{} \nu w' \models ({\mathbf {X}}{\mathbf {F}}\varphi ') \vee \varphi ' &{} ({\mathbf {F}}\varphi ' \equiv {\mathbf {X}}{\mathbf {F}}\varphi ' \vee \varphi ')\\ \text{ iff } &{} \big (w' \models {\mathbf {F}}\varphi '\big ) \vee \big (\nu w' \models \varphi '\big ) &{} \text {(semantics of LTL)}\\ \text{ iff } &{} \big (w' \models {\mathbf {F}}\varphi '\big ) \vee \big ( w' \models { af}(\varphi ',\nu )\big ) &{} \text {(ind. hyp.)}\\ \text{ iff } &{} w' \models {\mathbf {F}}\varphi ' \vee { af}(\varphi ',\nu ) &{} \text {(def. of }{ af})\\ \text{ iff } &{} w' \models { af}({\mathbf {F}}\varphi ',\nu ) &{} \text {(def. of } { af}) \end{array} \end{aligned}$$

Now we prove the property for every word w by induction on the length of w. If $w = \epsilon$ then ${ af}(\varphi ,w)=\varphi$, and so $ww' \models \varphi$ iff $w' \models \varphi$ iff $w' \models { af}(\varphi ,w)$. If $w = \nu w''$ for some $\nu \in 2^{Ap}$, then we have

$$\begin{aligned} \begin{array}{llr} &{} w' \models { af}(\varphi , w) \\ \text{ iff } &{} w' \models { af}(\varphi , \nu w'') \\ \text{ iff } &{} w' \models { af}({ af}(\varphi , \nu ), w'') &{} \text {(def. of } { af})\\ \text{ iff } &{} w'' w' \models { af}(\varphi , \nu ) &{} \text {(ind. hyp.)} \\ \text{ iff } &{} \nu w'' w' \models \varphi &{} (2) \\ \text{ iff } &{} w w' \models \varphi \end{array} \end{aligned}$$

$\square$

Lemma

5 Let $\mathbf {i}$ be the rank of condition (2) in Theorem 5. If the rank of $\tau$ stabilizes, then ${ strk}_w(\tau ) < \mathbf {i}$.

Proof

We first prove the following two claims, where $\mathbf {i}$ is the rank of condition (2):

• (a) If $\tau$ succeeds at rank $\mathbf {i}$, then ${ strk}_w(\tau ) < \mathbf {i}$.

  Since $\tau$ has rank $\mathbf {i}$ when it reaches the accepting states, we clearly have ${ strk}_w(\tau ) \le \mathbf {i}$. We show ${ strk}_w(\tau ) < \mathbf {i}$. Assume the contrary. With the previous observation, we have ${ strk}_w(\tau ) = \mathbf {i}$. Let t be some time at which $\tau$ has already entered the accepting states, and its rank has stabilized. By (2.1), some token $\tau '$ born after time t (i.e., $\tau ' > t$) also succeeds at rank $\mathbf {i}$. Let $t' \ge t$ be the time immediately before $\tau '$ enters the accepting states. Then we have ${ rk}_w(\tau , t') = \mathbf {i}$, because at time $t'$ token $\tau$ has already stabilized, and ${ rk}_w(\tau ', t') = \mathbf {i}$ by definition. But at time $t'$ token $\tau$ is in some accepting state, while $\tau '$ is not. So we have two tokens in different states with the same rank, contradicting the definition of rank.

• (b) If ${ rk}_w(\tau , t) \le { rk}_w(\tau ', t) ={ strk}_w(\tau ') \in {\mathbb {N}}$, then ${ rk}_w(\tau , t) ={ strk}_w(\tau )$.

  (If a token has reached its stable rank at some time t, then so have all tokens of older rank.)

  Assume ${ rk}_w(\tau , t) \ne { strk}_w(\tau )$. Then at some time $t' > t$ the rank of $\tau$ either becomes $\bot$ (because $\tau$ reaches a sink) or improves (because $\tau$’s firm merges with a firm of older rank). In both cases, the rank of ${ rk}_w(\tau ', t)$ also improves (because the rank of $\tau$ becomes vacant), contradicting the assumption that at time t token $\tau$ has already reached its stable rank.

Assume now that the rank of $\tau$ stabilizes but ${ strk}_w(\tau ) \ge \mathbf {i}$. By (2.1), some token $\tau '$ born after the rank of $\tau$ stabilizes succeeds at rank $\mathbf {i}$. Since $q_0 \notin F$, this token eventually enters the accepting states. Let t be the time immediately before $\tau '$ enters the accepting states. We have ${ rk}_w(\tau ', t) = \mathbf {i}$. Since ${ strk}_w(\tau ) \ge \mathbf {i}$, we have ${ rk}_w(\tau , t) \ge \mathbf {i} = { rk}_w(\tau ', t)$. By (b) (with the roles of $\tau$ and $\tau$ reversed), we get ${ rk}_w(\tau ', t) ={ strk}_w(\tau ')$, and so ${ strk}_w(\tau ')=\mathbf {i}$. But, since $\tau '$ succeeds at rank $\mathbf {i}$, this contradicts (a). $\square$

Proposition

5 Let $\mathcal {M}_1=(Q_1,\varSigma ,q_{01},\delta _1, F_1)$ and $\mathcal {M}_2=(Q_2,\varSigma ,q_{02},\delta _2, F_2)$. Let $Q=Q_1 \times Q_2$, let $q_0 = (q_{01},q_{02})$, and let $\delta :Q \times \varSigma \rightarrow Q$ be the function given by $\delta (q_1,q_2, \nu ) = (\delta _1(q_1, \nu ), \delta _2(q_2, \nu ))$ Then the tuples

$$\begin{aligned} \mathcal {M}_1 \cap \mathcal {M}_2= & {} \big (Q,\varSigma ,q_0,\delta , F_1 \times F_2 \big ) \\ \mathcal {M}_1 \cup \mathcal {M}_2= & {} \big (Q,\varSigma ,q_0,\delta , (F_1 \times Q_2) \cup (Q_1 \times F_2) \big ) \end{aligned}$$

are also Mojmir automata, and moreover $\mathsf {L}(\mathcal {M}_1 \cap \mathcal {M}_2) = \mathsf {L}(K_1) \cap \mathsf {L}(K_2)$ and $\mathsf {L}(\mathcal {M}_1 \cup \mathcal {M}_2) = \mathsf {L}(K_1) \cup \mathsf {L}(K_2)$.

Proof

We have to show that states reachable from an accepting state of $\mathcal {M}_1 \cap \mathcal {M}_2$ or $\mathcal {M}_1 \cup \mathcal {M}_2$ are again accepting. If $(q_1, q_2)$ is an accepting state of $\mathcal {M}_1 \cap \mathcal {M}_2$ or $\mathcal {M}_1 \cup \mathcal {M}_2$, then by definition $\delta ((q_1,q_2),\nu ) = (\delta _1(q_1, \nu ), \delta _2(q_2, \nu ))$.

• If $(q_1, q_2) \in F_1 \times F_2$, then, since $\mathcal {M}_1$ and $\mathcal {M}_2$ are $\mathcal {M}$ automata, we have $\delta _1(q_1, \nu ) \in F_1$ and $\delta _2(q_2, \nu ) \in F_2$, and so $\delta ((q_1,q_2),\nu ) \in F_1 \times F_2$.

• If $(q_1, q_2) \in (F_1 \times Q_2) \cup (Q_1 \times F_2)$, then, since $\mathcal {M}_1$ and $\mathcal {M}_2$ are $\mathcal {M}$ automata, we have $\delta (q_1, \nu ) \in F_1$ or $\delta (q_2, \nu ) \in F_2$, and so $\delta ((q_1,q_2),\nu ) \in (F_1 \times Q_2) \cup (Q_1 \times F_2)$.

We now prove $\mathsf {L}(\mathcal {M}_1 \cap \mathcal {M}_2) = \mathsf {L}(K_1) \cap \mathsf {L}(K_2)$ and $\mathsf {L}(\mathcal {M}_1 \cup \mathcal {M}_2) = \mathsf {L}(K_1) \cup \mathsf {L}(K_2)$. Since $\mathcal {M}_1 \cap \mathcal {M}_2$ and $\mathcal {M}_1 \cup \mathcal {M}_2$ only differ in their accepting states, they have the same function $run_w(\tau , t)$ describing the position of token $\tau$ at time t. Moreover, by the definition of $q_0$ and $\delta$ we easily get

$$\begin{aligned} run_w(\tau , t) = \big ( run1_w(\tau , t), run2_w(\tau , t)\big ) \end{aligned}$$

where run1 and run2 are the corresponding functions for $\mathcal {M}_1$ and $\mathcal {M}_2$. So we have

• (a) Token $\tau$ of $\mathcal {M}_1 \cap \mathcal {M}_2$ eventually reaches $F_1 \times F_2$ iff the token $\tau$ of $\mathcal {M}_1$ eventually reaches $F_1$ and the token $\tau$ of $\mathcal {M}_2$ eventually reaches $F_2$.

• (b) Token $\tau$ of $\mathcal {M}_1 \cup \mathcal {M}_2$ eventually reaches $(F_1 \times Q_2) \cup (Q_1 \times F_2)$ iff the token $\tau$ of $\mathcal {M}_1$ eventually reaches $F_1$, or the token $\tau$ of $\mathcal {M}_2$ eventually reach $F_2$.

By (a), almost every token of $\mathcal {M}_1 \cap \mathcal {M}_2$ eventually reaches $F_1 \times F_2$ iff almost every token of $\mathcal {M}_1$ eventually reaches $F_1$, and almost every token of $\mathcal {M}_2$ eventually reaches $F_2$. So $\mathsf {L}(\mathcal {M}_1 \cap \mathcal {M}_2) = \mathsf {L}(K_1) \cap \mathsf {L}(K_2)$. By (b), almost every token of $\mathcal {M}_1 \cap \mathcal {M}_2$ eventually reaches $(F_1 \times Q_2) \cup (Q_1 \times F_2)$ iff almost every token of $\mathcal {M}_1$ eventually reaches $F_1$, or almost every token of $\mathcal {M}_2$ eventually reaches $F_2$. So $\mathsf {L}(\mathcal {M}_1 \cup \mathcal {M}_2) = \mathsf {L}(K_1) \cup \mathsf {L}(K_2)$ $\square$

Lemma

7 Let $\varphi$ be a formula and let w be a word.

• (a) Every set $\mathcal {G}\subseteq {\mathbb {G}}{\varphi }$ closed for w is included in $\mathcal {G}_{w}(\varphi )$.

• (b) $\mathcal {G}_{w}(\varphi )$ is closed for w.

Proof

• (a) Given $\mathcal {G}\subseteq {\mathbb {G}}{\varphi }$, we inductively assign to every ${\mathbf {G}}\psi \in \mathcal {G}$ an index as follows. If $\psi$ has no ${\mathbf {G}}$-subformulae, then ${\mathbf {G}}\psi$ has index 0; if $\psi$ has ${\mathbf {G}}$-subformulae, then its index is the maximum of the indices of its subformulae plus 1. Assume $\mathcal {G}\subseteq {\mathbb {G}}(\varphi )$ is closed for w, and let ${\mathbf {G}}\psi \in \mathcal {G}$. We prove $w \models {\mathbf {F}}{\mathbf {G}}\psi$ by induction on the index n of ${\mathbf {G}}\psi$.

  • $n = 0$. Since $\mathcal {G}$ is closed for w, we have $\mathcal {G}\models _P { af}_{\mathbf {G}}(\psi , w_{ij})$ for almost every $i \in \mathbb {N}$ and almost every $j \ge i$. Let $j > i$ be such that $\mathcal {G}\models _P { af}_{\mathbf {G}}(\psi , w_{ij})$ holds. Since $\psi$ has no ${\mathbf {G}}$-subformulae (because $n=0$), the formulae of $\mathcal {G}$ occur neither in $\psi$ nor, by the definition of ${ af}_{\mathbf {G}}$, in ${ af}_{\mathbf {G}}(\psi , w_{ij})$. So we get $\emptyset \models _P { af}_{\mathbf {G}}(\psi , w_{ij})$, which implies ${ af}_{\mathbf {G}}(\psi , w_{ij}) \equiv _P {\mathbf {tt}}$. Moreover, since $\psi$ has no subformulae and ${ af}_{\mathbf {G}}$ and ${ af}$ only differ on ${\mathbf {G}}$-formulae, we have ${ af}_{\mathbf {G}}(\psi , w_{ij}) = { af}(\psi , w_{ij})$. So we finally obtain ${ af}(\psi , w_{ij})\equiv _P {\mathbf {tt}}$ for almost every $i \in \mathbb {N}$ and almost every $j \ge i$. Apply now Theorem 3.

  • $n > 0$. Let $\mathcal {G}'$ be the set of formulae of $\mathcal {G}$ that are subformulae of $\psi$. For every ${\mathbf {G}}\psi ' \in \mathcal {G}'$ the index of ${\mathbf {G}}\psi '$ is at most $n-1$ and so, by induction hypothesis, we have $w \models {\mathbf {F}}{\mathbf {G}}\psi '$. So there exists $k_1$ such that $w_i \models \mathcal {G}'$ for every $i \ge k_1$. Moreover, since $\mathcal {G}$ is closed for w, we have $\mathcal {G}\models _P { af}_{\mathbf {G}}(\psi , w_{ij})$ for almost every $i \in \mathbb {N}$ and almost every $j \ge i$. Further, since the formulae of $\mathcal {G}\setminus \mathcal {G}'$ do not appear in any ${ af}_{\mathbf {G}}(\psi , w_{ij})$, there exists $k_2$ such that $\mathcal {G}' \models _P { af}_{\mathbf {G}}(\psi , w_{i j})$ for every $i \ge k_2$ and almost every $j \ge i$. Taking $k = \max \{k_1, k_2\}$, we obtain:

    • (i) $w_i \models \mathcal {G}'$ for every $i \ge k$, and

    • (ii) $\mathcal {G}' \models _P { af}_{\mathbf {G}}(\psi , w_{i j})$ for every $i \ge k$ and almost every $j \ge i$.

    We show that (i) and (ii) imply $w_i \models \psi$ for almost every $i \ge k$. We proceed by an structural induction on $\psi$, very similar to the one in the proof of Proposition 2, except for the case $\psi = {\mathbf {G}}\psi '$. We omit some cases, and only sketch the proof of others.

    • $\psi = a$. Let $i \ge k$ such that (i) holds. By (ii) we have $\mathcal {G}' \models _P { af}_{\mathbf {G}}(a, w_{i j})$ for almost every $j \ge i$, and so ${ af}_{\mathbf {G}}(a, w_{ij}) = {\mathbf {tt}}$ for almost every $j \ge i$. But ${ af}_{\mathbf {G}}(a, w_{ij}) = {\mathbf {tt}}$ implies $w_{i(i+1)}=a$, and so $w_i \models a$.

    • $\psi = \psi _1 \wedge \psi _2$ and $\psi =\psi _1 \vee \psi _2$. Both cases follow immediately from the induction hypothesis.

    • $\psi = {\mathbf {G}}\psi '$. By the definition of ${ af}_{\mathbf {G}}$, we have ${ af}_{\mathbf {G}}(\psi , w_{i j})={\mathbf {G}}\psi '=\psi$ for every $j \ge i$. So, by (ii), we have $\mathcal {G}' \models _P \psi$ which, together with (i), implies $w_i \models \psi$ for every $i \ge k$.

• (b) We first prove a preliminary result: if $w \models \varphi$, then $\mathcal {G}_{w}(\varphi ) \models { af}_{\mathbf {G}}(\varphi , w_{0i})$ for almost every $i \in \mathbb {N}$. The proof is very similar to that of Theorem 1. It suffices to say that we proceed by structural induction on $\varphi$, using the same arguments as in Theorem 1, with two minor adjustments:

  • ${ af}_{\mathbf {G}}(\varphi , w_{0i}) \equiv _P {\mathbf {tt}}$ is replaced by $\mathcal {G}_{w}(\varphi ) \models { af}_{\mathbf {G}}(\varphi , w_{0i})$.

  • The ${\mathbf {G}}$-case, i.e., $\varphi = {\mathbf {G}}\varphi '$, is proved differently. It follows immediately from the fact that, since $w \models {\mathbf {G}}\varphi '$ by assumption, we have ${\mathbf {G}}\varphi ' \in \mathcal {G}_{w}({\mathbf {G}}\varphi ')$.

Now we proceed to prove (b), also by structural induction on $\varphi$. If $\varphi$ is not a ${\mathbf {G}}$-formula, then the result follows either directly from the definitions or directly from the induction hypothesis. So consider the case $\varphi = {\mathbf {G}}\varphi ^\prime$. By definition we have $\mathcal {G}_{w}(\varphi ') \subseteq \mathcal {G}_{w}(\varphi )$, and by induction hypothesis $\mathcal {G}_{w}(\varphi ')$ is closed for w. If $w \not \models {\mathbf {F}}{\mathbf {G}}\varphi ^\prime$ then $\mathcal {G}_{w}(\varphi ') = \mathcal {G}_{w}(\varphi )$, and so $\mathcal {G}_{w}(\varphi )$ is closed for w. If $w \models {\mathbf {F}}{\mathbf {G}}\varphi ^\prime$ then $\mathcal {G}_{w}(\varphi ) = \mathcal {G}_{w}(\varphi ') \cup \{{\mathbf {G}}\varphi '\}$. Since $\mathcal {G}_{w}(\varphi ')$ is closed for w, we have $\mathcal {G}_{w}(\varphi ') \models _P { af}_{\mathbf {G}}(\psi , w_{ij})$ for almost every $i\in \mathbb {N}$, almost every $j \ge i$, and for every ${\mathbf {G}}\psi \in \mathcal {G}_{w}(\varphi ')$. So it suffices to show $\mathcal {G}_{w}(\varphi ) \models _P { af}_{\mathbf {G}}(\varphi ', w_{ij})$ for almost all every $i \in \mathbb {N}$ and almost every $j \ge i$. Since $w \models {\mathbf {F}}{\mathbf {G}}\varphi ^\prime$, we have $w_i \models \varphi '$ for almost all $i\in \mathbb {N}$. Applying the preliminary result above to every $w_i$, we obtain $\mathcal {G}_{w}(\varphi ') \models _P { af}_{\mathbf {G}}(\varphi ', w_{ij})$ for almost every $i \in \mathbb {N}$ and almost every $j \ge i$, and we are done. $\square$

Lemma

8 Let $\varphi$ be a formula and let $\mathcal {G}\subseteq {\mathbb {G}}(\varphi )$. For every $\psi \in { Reach}_{\mathbf {G}}(\varphi )$ and every $\nu \in 2^{Ap}$, if $\mathcal {G}\models _P \psi$ then $\mathcal {G}\models _P { af}_{\mathbf {G}}(\psi ,\nu )$.

Proof

We proceed by induction on the structure of $\psi$. Since $\mathcal {G}\models _P \psi$, by the definition of propositional implication, the formula $\psi$ must be either ${\mathbf {tt}}$, a conjunction, a disjunction, or a ${\mathbf {G}}$-formula. If $\psi ={\mathbf {tt}}$ then ${ af}_{\mathbf {G}}(\psi ,\nu )={\mathbf {tt}}$ and we are done. If $\psi =\psi _1 \wedge \psi _2$ then ${ af}_{\mathbf {G}}(\psi ,\nu )={ af}_{\mathbf {G}}(\psi _1, \nu ) \wedge { af}_{\mathbf {G}}(\psi _2,\nu )$ and $\mathcal {G}\models _P { af}_{\mathbf {G}}(\psi ,\nu )$ follows immediately from the induction hypothesis. The case $\psi =\psi _1 \vee \psi _2$ is analogous. Finally, if $\psi = {\mathbf {G}}\psi '$ for some formula $\psi '$ then ${ af}_{\mathbf {G}}({\mathbf {G}}\psi ') = {\mathbf {G}}\psi '$, and we are done. $\square$

Lemma

11 Let $\mathcal {M}(\psi ,\mathcal {G})$ be the Mojmir automaton for a formula $\psi$. Assume $\mathcal {M}(\psi , \mathcal {G})$ accepts a word w at the smallest accepting rank ${\mathbf {r}}$. For almost every $t \in \mathbb {N}$ and for every token $\tau$ of the run of $\mathcal {M}(\psi ,\mathcal {G})$ on w, the token succeeds iff

• 1. $\tau > t$, or

• 2. ${ sr}_w({ run}_w(\tau ,t),t) \ge r$, or

• 3. ${ run}_w(\tau ,t) \in F$.

Proof

Consider the accepting run of $\mathcal {M}(\psi ,\mathcal {G})$ on w. Let $k'$ be large enough such that at time $t' \ge k'$: all tokens $\tau$ born after $k'$ eventually succeed; the finitely many tokens that fail have already reached a sink; and the finitely many tokens that succeed with rank smaller than ${\mathbf {r}}$ have already already reached an accepting state. Notice that such a $k'$ only exists for the smallest accepting rank, since infinitely many tokens enter the accepting states with this rank and for all larger accepting ranks this constant does not exist. Furthermore let $k \ge k'$ be large enough so that all squatting tokens born before or at time $k'$ have already reached their stable rank at time k. We show that the lemma holds for every $t \ge k$.

Let $\tau$ be an arbitrary token.

• Assume $\tau$ succeeds. We show that if (1) and (3) do not hold, then (2) holds. By (3), $\tau$ has not yet reached the accepting states. By our choice of $k'$, by the time $\tau$ enters the accepting states it will have rank ${\mathbf {r}}$ or larger. Since the rank of a token can only decrease, its current rank is also equal to the accepting rank r or larger. So ${ sr}_w({ run}_w(\tau ,t),t) \ge r$.

• Assume (1), (2), or (3) hold. If (3) holds, then $\tau$ succeeds by the definition of success. If (1) holds, then $\tau$ succeeds by our choice of $k'$. Assume now that (2) holds. We show that (2) neither fails nor squats outside the accepting states, and so necessarily succeeds. Since $\tau$ has a rank at time t, it is not in a sink, and so, by our choice of $k'$, the token does not fail. To show that $\tau$ does not squat outside the accepting states, we recall part (c) in the proof of Theorem 5: the stable rank of a token is bounded from above by accepting ranks, thus also by the smallest. So, by (2), the rank of $\tau$ has not stabilized yet, and therefore, by our choice of k, it does not squat outside the accepting states. $\square$