Backward deterministic and weak alternating $\omega$-automata

TL;DR

This paper introduces a direct method to convert weak alternating omega-automata into backward deterministic automata, improving transformations from nondeterministic B"uchi automata and LTL formulas with optimal results.

Contribution

It provides the first direct transformation from weak alternating omega-automata to backward deterministic automata, enabling efficient conversions for automata and temporal logic.

Findings

Enables transformation of nondeterministic B"uchi automata into backward deterministic automata

Achieves optimal backward deterministic automata for LTL formulas

Uses a novel direct transformation approach

Abstract

We present a direct transformation of weak alternating $\omega$-automata into equivalent backward deterministic $\omega$-automata and show (1) how it can be used to obtain a transformation of non-deterministic B\"uchi automata into equivalent backward deterministic automata and (2) that it yields optimal equivalent backward deterministic automata when applied to linear-time temporal logic formulas. (1) uses the alternation-free fragment of the linear-time $\mu$-calculus as an intermediate step; (2) is based on the straightforward translation of linear-time temporal logic into weak alternating $\omega$-automata.

Equations

$$\text{compl}(B)$$

$$\text{compl}(\text{medcircle}q)$$

$$\text{compl}({\tau }_0\vee {\tau }_1)$$

$$\text{compl}({\tau }_0\wedge {\tau }_1)$$

$$\text{compl}(\delta )(q)=\text{compl}(\delta (q)),\text{for every q∈Q.}$$

$$e[B]$$

$$e[\text{medcircle}q]$$

$$e[{\tau }_0\vee {\tau }_1]$$

$$e[{\tau }_0\wedge {\tau }_1]$$

$$e^{\prime }[B]$$

$$e^{\prime }[\text{medcircle}{q}^{\prime }]$$

$$e^{\prime }[{\tau }_0\vee {\tau }_1]$$

$$e^{\prime }[{\tau }_0\wedge {\tau }_1]$$

$$v_q^{\prime }=\text{if v~q>m then v~q else v~q+1.}$$

$$e^{\prime \prime }[B]$$

$$e^{\prime \prime }[\text{medcircle}{q}^{\prime }]$$

$$e^{\prime \prime }[{\tau }_0\vee {\tau }_1]$$

$$e^{\prime \prime }[{\tau }_0\wedge {\tau }_1]$$

$$e^{\prime \prime }[B]$$

$$e^{\prime \prime }[\text{medcircle}{q}^{\prime }]$$

$$e^{\prime \prime }[{\tau }_0\vee {\tau }_1]$$

$$e^{\prime \prime }[{\tau }_0\wedge {\tau }_1]$$

$$\lambda (\{v_q{\}}_{q\in Q})=\{q\in N\mid v_q<\infty \}\cup \{q\in R\mid v_q=\infty \}.$$

$$\delta (a)$$

$$\delta (\neg a)$$

$$\delta (q_{\psi \vee {\psi }^{\prime }})$$

$$\delta (q_{\psi \wedge {\psi }^{\prime }})$$

$$\delta (q_{\mathsf{X}\psi })$$

$$\delta (q_{\mathsf{F}\psi })$$

$$\delta (q_{\mathsf{G}\psi })$$

$$\delta (q_{\psi \mathsf{U}{\psi }^{\prime }})$$

$$\delta (q_{\psi \mathsf{R}{\psi }^{\prime }})$$

$$\delta (q_a)$$

$$\delta (q_{\neg a})$$

$$\delta (q_{\text{medcircle}\psi })$$

$$\delta (q_{\psi \vee {\psi }^{\prime }})$$

$$\delta (q_{\psi \wedge {\psi }^{\prime }})$$

$$\delta (q_{{\mu }_i\vec{X}.\vec{\psi }})$$

$$\delta (q_X)$$

$$f_{\vec{\phi }}(u)(i)=\{j<k\mid \text{φj is true for the suffix u[i,ω)}\}$$

$${\chi }_i^j={\sigma }_i⟨X_i^0,\dots ,X_i^{n-1}⟩.⟨{\phi }_i^0,\dots ,{\phi }_i^{n-1}⟩,$$

$${\phi }_0^j=\underset{a\in A}{\bigvee }\left(a\wedge \underset{⟨q_j,a,q_k⟩\in \Delta }{\bigwedge }\text{medcircle}{X}_0^k\right).$$

$${\phi }_{2i^{\prime }+1}^j$$

$${\phi }_{2i^{\prime }}^j={\chi }_{2i^{\prime }-1}^j\vee \underset{a\in A}{\bigvee }\left(a\wedge \underset{⟨q_j,a,q_k⟩\in \Delta }{\bigwedge }\text{medcircle}{X}_{2i^{\prime }}^k\right),$$

Full text

1 Introduction

It is only natural to read $\omega$-words from left to right: they have a definite start, but no end, so one reads one letter after the other, starting with the letter in the first position. This is probably why we typically envision an $\omega$-automaton as a device that when running over an $\omega$-word starts by consuming the letter in the first position, then goes over to the letter in the second position, then to the letter in the third position, and so on. We call this the forward approach. Almost all of $\omega$-automata theory is based on the forward approach, in particular, there is a huge body of work on the determinization of $\omega$-automata, where—if one wanted to be precise—determinization means the process of constructing automata which are deterministic when following the forward approach.

There is essentially one fundamental result in the theory of $\omega$-automata with regard to the backward approach, where automata start in the infinite and run until they reach the beginning of the word: Olivier Carton and Max Michel [5] proved that every regular $\omega$-language is recognized by a backward deterministic Büchi automaton. In other words, in the backward approach—unlike in the forward approach—all types of acceptance conditions classically considered (Büchi, generalized Büchi, parity, Rabin, Streett, Muller) give rise to the same class of $\omega$-languages and this class is the same as the class of $\omega$-languages recognized by non-deterministic automata (expressive completeness). Technically, the main contribution of Carton and Michel are two different constructions that turn a given non-deterministic Büchi automaton into an equivalent backward deterministic generalized transition Büchi automaton (which they show can be transformed into an equivalent backward deterministic Büchi automaton). The main contribution of the present paper is a direct transformation of a given forward weak alternating $\omega$-automaton into an equivalent backward deterministic generalized transition Büchi automaton.

Weak alternating automata can be viewed as alternation-free formulas of the modal $\mu$-calculus, and vice versa. This was first demonstrated by André Arnold and Damian Niwiński for sets of infinite trees [2] and carries over to $\omega$-words directly. For $\omega$-words, it is moreover true that weak alternating automata and the alternation-free fragment of the modal $\mu$-calculus—often referred to as $\nu\text{TL}$ [3, 18] or $\mu\text{TL}$ [11]—are expressively complete in the sense that they both describe exactly the class of all regular $\omega$-languages. (Note that the alternation hierarchy of $\nu\text{TL}$ collapses on the second level [1], whereas on trees it is strict [4, 12].) Expressive completeness follows from [2] and work by Kupferman and Vardi on weak alternating $\omega$-automata [9] and was also proved by Kaivola [7].

Based on all this we describe a new way to convert a given non-deterministic Büchi automaton into an equivalent backward deterministic Büchi automaton: we go from a Büchi automaton to a $\nu\text{TL}$-formula, then from $\nu\text{TL}$ to weak alternating automata (immediate), and finally apply our construction. In some sense, we break down the construction from [5] into simpler constructions at the expense of complexity. The automata we construct are somewhat larger than the ones constructed by Carton and Michel.

Formulas of linear-time temporal logic (LTL) are typically translated into non-deterministic Büchi automata [20]; a standard translation will actually produce a backward deterministic automaton [17]. There is, however, also a straightforward way to translate an LTL formula into a weak alternating automaton [6, 14]. So our construction can serve to obtain a backward deterministic automaton for a given LTL formula: simply apply the construction to the weak alternating automaton obtained from a given LTL formula. We show that the automaton thus obtained has the same size as the “standard automaton”.

2 From weak alternating to backward deterministic automata

In this section, we present our main result, a transformation from weak alternating to backward deterministic $\omega$-automata. We begin with basic definitions and results we draw on.

2.1 Weak alternating $\omega$-automata

There are different ways of formalizing weak alternating automata; the variant used in this paper works with transition conditions rather than a partition of the state space into existential and universal states.

Given a set $Q$ of states and an alphabet $A$, the transition conditions over $Q$ and $A$ are formulas built from

• •

$B$, for $B\subseteq A$, and

• •

${\medcircle}q$, for $q\in Q$,

using the boolean connectives $\vee$ and $\wedge$. The set of all these conditions is denoted by $\text{TC}(Q,A)$.

A weak alternating automaton [13] over an alphabet $A$ is given by

• •

a finite set $Q$ of states,

• •

a transition function $\delta\colon Q\to\text{TC}(Q,A)$, and

• •

a partition of the state set $Q$ into a set $R$ of recurring and a set $N$ of non-recurring states. (More formally, a pair $\langle R,N\rangle$ is given such that $R\cup N=Q$ and $R\cap N=\emptyset$ hold. The elements of the first component are called recurring states and the elements of the second component are called non-recurring states.)

In addition, there is a requirement on recurring and non-recurring states with regard to the transition graph. This graph is the directed graph with vertex set $Q$ and an edge from $q$ to $q^{\prime}$ if ${\medcircle}q^{\prime}$ occurs in $\delta(q)$.

The requirement is that either $S\cap Q\subseteq R$ or $S\cap Q\subseteq N$ holds for every strongly connected component $S$ of the transition graph, that is, all states of any strongly connected component (SCC) must be recurring or else non-recurring.

A very weak alternating automaton is one where the SCC’s of the transition graph are singleton sets (which immediately implies that very weak alternating automata are weak alternating automata).

In general, runs of alternating automata are labeled trees satisfying certain conditions, but since the recurrence condition we work with can be viewed as a Büchi or parity condition, it is sufficient to consider graphs, as described in what follows, see [9].

A run graph of an automaton as described above on a word $u$ is a directed graph where the vertices are pairs of the form $\langle i,\tau\rangle$ with $i\in\omega$ and $\tau$ is a state or a subformula (including the formula itself) of any of the transition conditions $\delta(q)$.

The following conditions must be satisfied for every vertex $\langle i,\tau\rangle$:

• •

If $\tau\in Q$, then $\langle i,\tau\rangle$ has exactly one outgoing edge and this leads to $\langle i,\delta(\tau)\rangle$.

• •

If $\tau={\medcircle}q$, then $\langle i,\tau\rangle$ has exactly one outgoing edge and this leads to $\langle i+1,q\rangle$.

• •

If $\tau=\tau_{0}\vee\tau_{1}$, then $\langle i,\tau\rangle$ has outgoing edges only to $\langle i,\tau_{0}\rangle$ and $\langle i,\tau_{1}\rangle$ and at least one such edge exists.

• •

If $\tau=\tau_{0}\wedge\tau_{1}$, then $\langle i,\tau\rangle$ has outgoing edges exactly to $\langle i,\tau_{0}\rangle$ and $\langle i,\tau_{1}\rangle$.

In addition, vertices $\langle i,\tau\rangle$ with $\tau=B$ and $u(i)\notin B$ must not exist.

A good way to envision these graphs is to imagine the vertices arranged in levels numbered 0, 1, 2, …, where on level $i$ the vertices of the form $\langle i,q\rangle$ are grouped together and between level $i$ and level $i+1$ the vertices $\langle i,\tau\rangle$ with $\tau$ being a transition condition are located. Then the edges only go from vertices on level $i$ through intermediate vertices to vertices on level $i+1$.

For every infinite path through the run graph, the set $Q^{\prime}$ of states occurring infinitely often in it is a subset of an SCC of the transition graph, which means $Q^{\prime}\subseteq R$ or $Q^{\prime}\subseteq N$. If $Q^{\prime}\subseteq R$, the path is said to be final. The run graph is said to be final if all infinite paths through it are final.

For every $i$, the suffix $u[i,\omega)$ is said to be accepted from $q$ in a run graph if the graph is final and $\langle i,q\rangle$ is a vertex of it; it is accepted from $q$ by the automaton if there exists a final run graph that accepts it from $q$.

In Subsection 2.4 we use a result on complementing alternating automata. To state it, we first define, for every transition condition, the complementary transition condition by an appropriate set of equations:

[TABLE]

The automaton complementary to a given automaton $\mathscr{A}$, denoted $\text{compl}(\mathscr{A})$, is determined as follows:

• •

It has the same set of states as $\mathscr{A}$.

• •

Its transition function, denoted $\text{compl}(\delta)$, is defined by

[TABLE]

• •

The sets of recurring and non-recurring states are exchanged.

The fact we need is the following one.

Fact 1** (complementation of alternating automata, [15]).**

Let $\mathscr{A}$ be a weak alternating automaton over some alphabet $A$ and $q$ some state of it. For every $u\in A^{\omega}$ and $i<\omega$, the suffix $u[i,\omega)$ is accepted by $\mathscr{A}$ from state $q$ if, and only if, $u[i,\omega)$ is not accepted by $\text{compl}(\mathscr{A})$ from state $q$.

2.2 Backward deterministic $\omega$-automata

In general, a backward deterministic automaton is given by

• •

a finite set $Q$ of states,

• •

a transition function $\rho\colon A\times Q\to Q$, and

• •

a recurrence condition $\Omega$, which can be any acceptance condition such as a Büchi or a Muller condition, state-based or transition-based (see below).

A run of such an automaton on a word $u\in A^{\omega}$ is a word $r\in Q^{\omega}$ such that $r(i)=\rho(u(i),r(i+1))$ holds true for every $i\in\omega$. A run $r$ is final if it satisfies the recurrence condition. For instance, if $\Omega\subseteq Q$ is a (state-based) Büchi condition, then $r$ is final if there exist infinitely many $i$ such that $r(i)\in\Omega$. For a backward deterministic automaton, it is required that for every $u\in A^{\omega}$ there is exactly one final run!

In the following fundamental theorem, automata are viewed as defining sets of $\omega$-words: an automaton is augmented by a set $I\subseteq Q$ of initial states and then defines the set of all $u\in A^{\omega}$ where $u$ is accepted from some state $q\in I$ (for weak alternating automata) or where $r(0)\in I$ is true for the unique final run of the automaton on $u$ (for backward deterministic automata).

Fact 2** (completeness, [5]).**

For every Büchi automaton with $n$ states there exists an equivalent backward deterministic generalized transition Büchi automaton with at most $(3n)^{n}$ states and an equivalent backward deterministic Büchi automaton with at most $(12n)^{n}$ states.

2.3 Main result

To describe our main result we view weak alternating automata and backward deterministic automata as devices defining functions rather than languages. This is more general and gives a clearer result.

Let $\mathscr{A}$ be a weak alternating automaton over some alphabet $A$ and with state set $Q$. The function computed by $\mathscr{A}$, denoted $f_{\mathscr{A}}$, is the function $A^{\omega}\to(2^{Q})^{\omega}$ where $f(u)(i)$ is the set of all $q$ such that the suffix $u[i,\omega)$ is accepted from $q$.

Let $\mathscr{A}$ be a backward deterministic automaton, $B$ some alphabet, and $\lambda\colon Q\to B$ an output function. The function computed by $\mathscr{A}$ with respect to $\lambda$, denoted $f_{\mathscr{A},\lambda}$, is the function $A^{\omega}\to B^{\omega}$ defined by $f(u)=\lambda(r(0))\lambda(r(1))\dots$ where $r$ is the unique final run of $\mathscr{A}$ on $u$.

Main Theorem**.**

For every weak alternating automaton $\mathscr{A}$ there exists a backward deterministic automaton $\mathscr{B}$ and an output function $\lambda$ for $\mathscr{B}$ such that the function computed by $\mathscr{A}$ is the same as the function computed by $\mathscr{B}$ with respect to $\lambda$, that is, $f_{\mathscr{A}}=f_{\mathscr{B},\lambda}$. The automaton $\mathscr{B}$ has the following properties.

Let $S_{0},\dots,S_{k-1}$ be an enumeration of all SCC’s of the transition graph of $\mathscr{A}$ and $m_{i}=S_{i}\cap Q$ for $i<k$. Then the number of states of $\mathscr{B}$ is at most $\prod_{i<k}(m_{i}+1)^{m_{i}}$, in particular, $(n+1)^{n}$ is an upper bound for the number of states of $\mathscr{B}$ when $n$ is the number of states of $\mathscr{A}$. 2. 2.

The automaton $\mathscr{B}$ has a generalized transition Büchi condition with as many Büchi sets as $\mathscr{A}$ has states. 3. 3.

The automaton $\mathscr{B}$ has at most $2^{n}$ states when $\mathscr{A}$ is a very weak alternating automaton with $n$ states.

2.4 The construction

In this section, we describe how the automaton $\mathscr{B}$ from the Main Theorem is constructed. We proceed in three steps, starting with a basic automaton and refining it twice. The first refinement takes care of problems with non-recurring states; the second refinement takes care of problems with recurring states.

In general, given an $\omega$-word $u$, the automaton $\mathscr{B}$ tries to determine, for each position $i$, the states from which the suffix $u[i,\omega)$ is accepted by $\mathscr{A}$. This is why we model a state of $\mathscr{B}$ as assigning an appropriate value $v_{q}$ to each state $q\in Q$, indicating the “degree” of accepting (or non-accepting) $u[i,\omega)$ from $q$. Formally, a state is a family $\{v_{q}\}_{q\in Q}$.

2.4.1 Basic approach

In the basic approach the “variables” $v_{1}$ are boolean variables, more precisely, $v_{q}\in\{1,\infty\}$, where $1$ stands for true and $\infty$ for false.

The rules from the definition of a run graph as given in Subsection 2.1 can be turned immediately into rules describing how the variables must be updated when a letter is read. To describe this precisely, we assume a state $\{v_{q}\}_{q\in Q}$ is given. We want to define $\rho(a,\{v_{q}\}_{q\in Q})$, which we write as $\{v^{\prime}_{q}\}_{q\in Q}$.

With every transition condition $\tau$, we associate a corresponding expression $e[\tau]$, defined by the following set of equations:

[TABLE]

Then $v^{\prime}_{q}$ is obtained by evaluating $e[\delta(q)]$.

Shortcomings of the basic approach.

The transition function defined above has several shortcomings, as described in what follows.

Consider a weak alternating automaton $\mathscr{A}$ with a single state $q$ which is non-recurring and where $\delta$ is defined by $\delta(q)={\medcircle}q$. First, there are two runs of $\mathscr{B}$, namely one in which $v_{q}=1$ holds all the time and another one where $v_{1}=\infty$ holds all the time. Second, in the run graph of $\mathscr{A}$ corresponding to the first run of $\mathscr{B}$, the state $q$ occurs infinitely often on a path, which means the run graph is not final and must be ruled out.

One way to approach these two problems is to introduce an appropriate recurrence condition in $\mathscr{B}$, corresponding to the partition of the state space of $\mathscr{A}$ in recurring and non-recurring states. In fact, when, for instance, we require that $v_{1}=\infty$ holds infinitely often, the problems just mentioned disappear. But if there is more than just one state in an SCC of $\mathscr{A}$, a recurrence condition does no longer help by itself, as explained in what follows.

Example 1*.*

Imagine a weak alternating automaton $\mathscr{A}$ which has one SCC $S$ consisting of two non-recurring states, $q_{0}$ and $q_{1}$. There could be two words, $u$ and $u^{\prime}$, such that the graphs $G$ and $G^{\prime}$ depicted in Figure 1 are the run graphs of $\mathscr{A}$ on $u$ and $u^{\prime}$, respectively. (Note that $G$ and $G^{\prime}$ are two infinite graphs which are the results of repeating a finite graph infinitely often.)

The graph $G$ is not final, while $G^{\prime}$ is. The two graphs can, however, not be distinguished by any recurrence condition. The two states occur infinitely often in $G$ and in $G^{\prime}$, so there is no state-based recurrence condition that works. Moreover, for $G$ and $G^{\prime}$ the sets of all subgraphs induced by two consecutive levels and occurring infinitely often coincide. This means that no recurrence condition based on transitions works either.∎

2.4.2 Non-recurring states—first improvement

In Example 1 we have seen that a run of $\mathscr{B}$ may correspond to a run graph in $\mathscr{A}$ which is not final, because there may exist paths through this run graph with infinitely many non-recurring states. The idea for solving this problem is explained in what follows, where we ignore recurring states for the moment; they are dealt with in a dual fashion in the second improvement below.

Assume $v$ is a vertex of a final run graph $G$ of $\mathscr{A}$, say $v=\langle i,q\rangle$, and $q$ is non-recurring. Then the subgraph $H$ of $G$ consisting of the vertices reachable from $v$ and with second component in $\text{SCC}(q)$ is finite (because we are dealing with weak alternating automata). Let $v^{\prime}$ be a successor of $v$ in $G$. Either $v^{\prime}$ does not belong to $H$ anymore or we can consider the subgraph $H^{\prime}$ of $H$ consisting of the vertices reachable from $v^{\prime}$. The graph $H^{\prime}$ is a proper subgraph of $H$, that is, its size is smaller. Now we can pass from $H^{\prime}$ to $H^{\prime\prime}$ in the same way we passed from $H$ to $H^{\prime}$ (or stop because no vertices are left) arriving at an even smaller subgraph. This process must eventually terminate because $H$ was finite and the size of the subgraphs decreases in every step.

This is why in our construction, we measure the “size” of the subgraphs $H$, $H^{\prime}$, $H^{\prime\prime}$, … and make sure that the size decreases along any path until another SCC or the end of the path is reached. Here, “size” does not simply mean number of vertices, because this could be unbounded. The notion of size we use is coarser. So, to be precise, the size may also stay the same from one vertex of a path to the next, but we enforce it to to decrease eventually, which is obviously enough for the construction to be correct.

What size exactly means can be deduced from the proof of correctness of our construction in Subsection 2.4.4. Here, we only describe the construction.

Let $S$ be an SCC of the transition graph and assume $S\subseteq N$. The variables $v_{q}$, for $q\in S$, now have values in $\{1,\dots,|S|,\infty\}$. The values $v^{\prime}_{q}$ are determined in two steps:

Values $\tilde{v}_{q}$ are determined where also [math] is allowed as a value. 2. 2.

These values are “lifted” so as to obtain values in the above range.

The details are spelled out further below, after some more terminology.

We use a normalization function when passing from one SCC to another one, in order to make sure that the values do not become to large. This function is denoted norm and defined by $\text{norm}(\infty)=\infty$ and $\text{norm}(i)=0$ for $i\in\omega$. We also use $q\leftrightsquigarrow q^{\prime}$ to denote that $q$ and $q^{\prime}$ belong to the same SCC of the transition graph.

To determine $\tilde{v}_{q}$ we adapt the expressions from above:

[TABLE]

We let $\tilde{v}_{q}$ be the value obtained by evaluating $e^{\prime}[\delta(q)]$.

The above equations are the same as the ones used in the basic approach, but there are two differences. First, for atomic formulas of the form $B$, the value [math] is used to model that a formula is true immediately, see (10). Second, the normalization is incorporated to make sure the automaton starts all over again when passing from SCC to another one, see (11).

The lifting works as follows. Let $m$ be the minimal value $\geq 0$ such that $m$ does not occur as a value of one of the $\tilde{v}_{q}$’s for $q\in S$. If $m=0$, then $v^{\prime}_{q}=\tilde{v}_{q}$ for all $q\in Q^{\prime}$. Otherwise, for every $q\in Q^{\prime}$,

[TABLE]

We say that $m$ is the critical value of the transition with respect to the SCC $S$.

Observe, firstly, that the lifting ensures that all values $v^{\prime}_{q}$ are greater than [math] and that the order of the $v_{q}$’s is the same as the order of the $\tilde{v}_{q}$’s. Observe, secondly, that no finite value greater than $|S|$ can occur by the above definition—the worst case is when $\infty$ does not occur but every value between $1$ and $|S|$. Observe, thirdly, that the else branch in (14) is the one (and only one) place where finite values greater than $1$ are generated.

Example 2* (Example 1 continued).*

In Figure 2, the graph $G^{\prime}$ from Figure 1 is decorated according to the improved transition function.∎

The recurrence condition we use is a generalized transition Büchi condition that makes sure every finite value $v_{q}$ originates from another SCC or a transition condition of the form $B$ for some $B\subseteq A$. Using the above terminology it makes sure that the graph $H$ is indeed finite. Technically, this means the values of the variables decrease down to $1$ and then “disappear” at some point.

For every $i$ with $0<i\leq|S|$, there is a transition Büchi set $B_{S,i}$ containing all transitions satisfying at least one of the following two conditions.

• •

The number $i$ is the critical value of the transition with respect to $S$.

• •

There is no $q\in S$ such that $v^{\prime}_{q}\geq i$.

Example 3* (Example 1 continued).*

In Figure 2, the first transition does not belong to any Büchi set, the second belongs to $B_{\{q_{0},q_{1}\},1}$, the third does not belong to any, the fourth belongs to $B_{\{q_{0},q_{1}\},2}$, … . This indicates a final run graph.∎

Recurring states—second improvement

With recurring states, there are similar problems as with non-recurring states.

Example 4* (Example 1 reused).*

Assume that in Example 1 the states $q_{0}$ and $q_{1}$ would be recurring. In the run graph $G$ the automaton could guess that all states on the infinite path are states from which the respective suffixes are not accepted, which is not true. But no recurrence condition, neither state- nor transition-based, could rule this out.∎

To deal with these problems, we use the same approach as with non-recurring states but interpret the values of the variables complementary. That is, $\infty$ means the respective suffix is accepted, a finite value means it is not. To implement this, we make use of duality as stated in Fact 1.

Technically, this means that we have two sets of defining rules, which are dual to each other, depending on whether the respective state is non-recurring or recurring.

The equations determining the value of the variable $\tilde{v}_{q}$ for a non-recurring state $q$ are:

[TABLE]

The ones for a recurring state $q$ are completely dual:

[TABLE]

Observe that indeed the roles of [math] and $\infty$, of $N$ and $R$, as well as of $\min$ and $\max$ are exchanged.

As above, there are generalized transition Büchi conditions for every SCC.

2.4.3 Output function

To complete the description of how we “implement” the Main Theorem, we need to specify an appropriate output function $\lambda$. For every state $\{v_{q}\}_{p\in Q}$ we set

[TABLE]

This is consistent with interpretation of the variables $v_{q}$ as explained in the previous subsections.

2.4.4 Proof of correctness

First of all, it is easy to see that the automaton $\mathscr{B}$ has the properties 1., 2., and 3. stated in the Main Theorem.

For the rest, it is enough to show the following for every word $u$:

1. (i)

If there is a final run $r$ of $\mathscr{B}$ on $u$, then $\lambda(r(i))=f_{\mathscr{A}}(u)$ for every $i\in\omega$. 2. (ii)

There is a final run of $\mathscr{B}$ on $u$. 3. (iii)

There is only one final run of $\mathscr{B}$ on $u$.

This is best proved by an induction on the SCC’s of the transition graph of $\mathscr{A}$, starting in the base case with the “lowest” SCC’s, that is, the ones without outgoing edges.

We show how the inductive step goes for a non-recurring SCC; the base cases and the inductive step for recurring SCC’s can be dealt with in a similar fashion, using duality where appropriate. In fact, the base cases are instances of the inductive step.

So in the following, $S$ is a non-recurring SCC. We refer to the SCC’s reachable from $S$ as the other SCC’s, excluding $S$ itself, and denote the set of states of the other SCC’s by $T$. We assume that (i)–(iii) hold for the other SCC’s (induction hypothesis).

Proof of (i).

Let $r$ be a final run of $\mathscr{B}$ on $u$ and write $\{v_{q,i}\}_{q\in Q}$ for $r(i)$. It is sufficient to show that for every $i$ and $q\in S$ the following hold.

• •

If $q\in N$ and $v_{q,i}<\infty$, then $u[i,\omega)$ is accepted from $q$.

• •

If $q\in N$ and $v_{q,i}=\infty$, then $u[i,\omega)$ is not accepted from $q$.

We show how the proof goes for the case of the first item; the other case can be dealt with in a similar fashion, using duality.

We construct a suitable part of a final run graph, which connects with the final run graph for the other SCC’s, known to exist by induction hypothesis. To this end, we assign to each vertex of the graph to be constructed a value. For each variable $v_{q,i}$ with $q\in S$ we have the vertex $\langle i,q\rangle$ and the value assigned to it is $v_{q,i}$. The other vertices are intermediate vertices and constructed as follows, for each $v_{q,i}$ with $v_{q,i}<\infty$ and $q\in S$ separately, by an induction on $\delta(q)$. So the formulas $\tau$ dealt with in the following are all assumed to be subformulas of $\delta(q)$.

There are three base cases:

• •

If $\tau=B$ and $u(i)\in B$, then $\langle i,B\rangle$ belongs to the run graph and is assigned [math].

• •

If $\tau={\medcircle}q^{\prime}$ and $q^{\prime}\in S$, then $\langle i+1,q^{\prime}\rangle$ belongs to the run graph being constructed and has already been assigned $v_{q^{\prime},i+1}$ (see above). No vertex is added.

• •

If $\tau={\medcircle}q^{\prime}$ and $q^{\prime}\notin S$, then $\langle i+1,q^{\prime}\rangle$ belongs to the run graph known to exist by the induction hypothesis, provided

• –

$q^{\prime}$ is non-recurring and $v_{q^{\prime},i+1}$ is finite or

• –

$q^{\prime}$ is recurring and $v_{q^{\prime},i+1}$ is infinite.

No vertex is added.

And there are two cases in the inductive step:

• •

If $\tau=\tau_{0}\vee\tau_{1}$ and $\langle i,\tau_{0}\rangle$ or $\langle i^{\prime},\tau_{1}\rangle$ is part of the run graph, then $\langle i,\tau\rangle$ is part of the run graph. It has an edge to the vertex with the smaller value assigned to it or to both vertices if they have the same value. The vertex $\langle i,\tau\rangle$ is assigned the same value as its successor(s).

• •

If $\tau=\tau_{0}\wedge\tau_{1}$ and $\langle i,\tau_{0}\rangle$ and $\langle i,\tau_{1}\rangle$ are part of the run graph, then $\langle i,\tau\rangle$ is part of the run graph. It has an edge to both vertices and is assigned the maximum of the value of its successors.

Observe that this construction mimics the mechanics of the transition function. In particular, $\langle i,\delta(q)\rangle$ is part of the run graph, the value assigned to this vertex is less than or equal to $v_{q,i}$, depending on the lifting, and the values along the paths do not increase. We can add the edges from $\langle i,q\rangle$ to $\langle i,\delta(q)\rangle$, for each $q\in S$ and each $i$.

Finally, observe that, by construction, if there is an infinite path through the part of the run graph just constructed, then one of the Büchi transition conditions of $\mathscr{B}$ for the SCC $S$ is violated. This concludes the proof for the inductive step.

Proof of (ii).

The induction hypothesis is that we already have a run $r$ on the other SCC’s. So when we write $v_{q,i}$ for $r(i)$, then every $v_{q,i}$ for $q\in T$ has already been defined. We need to extend $r$ to $S$ in the sense that we need to determine values $v_{q,i}$ for $q\in S$.

The key step is to define a monotone operation $F$ on families $\{v_{q,i}\}_{q\in S,i\in\omega}$ as follows. First, we write $\{v^{\prime}_{q,i}\}_{q\in S,i\in\omega}$ for $F(\{v_{q,i}\}_{q\in S,i\in\omega})$. Second, we stipulate that $\{v^{\prime}_{q,i}\}_{q\in S,i\in\omega}$ is obtained from $\{v_{q,i}\}_{q\in S\cup T,i\in\omega}$ by applying the transition function.

Clearly, the operation $F$ is monotone when we view the families $\{v_{q,i}\}_{q\in S,i\in\omega}$ as being ordered point-wise. This means that when we start from the family with $v_{q,i}=\infty$ for $q\in S$ and $i\in\omega$, then we eventually reach a fixed point. This fixed point satisfies the transition function (restricted to $S$ and the other SCC’s), just as any other fixed point does, but the least fixed point also satisfies the Büchi transition conditions for $S$. So it is a final run for $S$ and the other SCC’s, which concludes the proof for the inductive step.

Proof of (iii).

Let $r$ be the run defined by the fixed point construction in the proof of (ii). By way of contradiction, let $r^{\prime}$ be any other final run. We write $r(i)$ as $\{v_{q,i}\}_{q\in S\cup T}$ and $r^{\prime}(i)$ as $\{v^{\prime}_{q,i}\}_{q\in S\cup T}$.

By induction hypothesis, the two runs can only differ for some $q\in S$. Since any run can be viewed as a fixed point (see the proof of (ii)) and $r$ is the least fixed point, there must be $q\in Q$ and $i\in\omega$ such that $v_{q,i}<v^{\prime}_{q,i}$. Since the transition function is deterministic (and because of monotonicity), for every $j>i$ there must be some $q_{j}$ such that $v_{q_{j},j}<v^{\prime}_{q_{j},j}$. Moreover, the corresponding pairs $\langle j,q_{j}\rangle$ can be assumed to be vertices of the graph constructed in the proof of (i). Because $q$ is assumed to be non-recurring, there is some $j^{\prime}$ such that $q_{j^{\prime}}\in S$ and

• •

$\langle j^{\prime},q_{j^{\prime}}\rangle$ is a dead end or

• •

all successors of $\langle j^{\prime},q_{j^{\prime}}\rangle$ belong to $T$.

In both cases, the transition function would set $v_{q_{j^{\prime}},j^{\prime}}$ and $v^{\prime}_{q_{j^{\prime}},j^{\prime}}$ to the same value—the desired contradiction.

3 Applications

We present three applications of the Main Theorem in what follows. First, we use it to translate linear-time temporal formulas into backward deterministic $\omega$-automata. Second, we use it to translate alternation-free modal/temporal fixed-point formulas into backward deterministic $\omega$-automata. Third, we use it to transform a given Büchi automaton into an equivalent backward deterministic automaton.

3.1 Linear-time temporal logic

In this section, we explain that our construction is “optimal” with regard to converting linear-time temporal formulas into equivalent Büchi automata in the sense that first transforming a given formula of size $n$ into a weak alternating automaton and then applying our construction yields a backward deterministic generalized Büchi automaton with $2^{n}$ states, which is what one typically gets, see, for instance, [19].

In the variant of linear-time temporal logic (LTL) we consider, formulas are built from letters over a given alphabet using boolean connectives and future temporal operators such as “next” (${\mathsf{X}}$), “eventually” ($\mathsf{F}$), “always” ($\mathsf{G}$), “until” ($\mathsf{U}$), and “release” ($\mathsf{R}$). As usual, we interpret such formulas in $\omega$-words over the given alphabet. All operators except “next” are interpreted non-strict, but what we describe works with minor modifications also for the strict variants.

Without loss of generality, we assume formulas are in negation normal form, that is, negation only occurs in front of letters of the alphabet.

We next recall the transformation of LTL formulas into equivalent weak alternating automata, see, for instance, [6]. A weak alternating automaton equivalent to a given formula $\varphi$ has a state $q_{\psi}$ for every subformula $\psi$ of $\varphi$; its transition function is defined by induction by the following equations:

[TABLE]

The states for eventually and until formulas are non-recurring; the states for always and release formulas are recurring. For the other states, it does not matter whether they are recurring or non-recurring, because they do not belong to any cycle in the transition graph.

Obviously, the automaton is a very weak alternating $\omega$-automaton. So the Main Theorem yields:

Corollary 1**.**

The transformation of an LTL formula of size $n$ into an equivalent backward deterministic generalized Büchi automaton via weak alternating automata results in an automaton with $2^{n}$ states.

3.2 The alternation-free linear-time $\mu$-calculus

To begin with, we briefly describe the dialect of the linear-time $\mu$-calculus [18, 3] we use. Given an alphabet $A$, the set of all linear-time $\mu$-calculus formulas (expressions), denoted $\nu\text{TL}$, is the smallest set consisting of

• •

$a$ and $\neg a$, for $a\in A$,

• •

$X$, for $X\in\mathcal{V}$, where $\mathcal{V}$ is a supply of variables,

• •

${\medcircle}\varphi$, if $\varphi$ belongs to the set,

• •

$\varphi_{0}\vee\varphi_{1}$ and $\varphi_{0}\wedge\varphi_{1}$, if $\varphi_{0}$ and $\varphi_{1}$ belong to the set,

• •

$\mu_{i}\vec{X}.\vec{\varphi}$ and $\nu_{i}\vec{X}.\vec{\varphi}$, if $\vec{X}=\langle X_{0},\dots,X_{r-1}\rangle$ is a vector of distinct variables from $\mathcal{V}$, $\varphi_{0},\dots,\varphi_{r-1}$ belong to the set, and $i<r$.

In our vectorial fixed point dialect the formula $\sigma_{i}\vec{X}.\vec{\varphi}$ refers to the $i$-th component of the least/greatest vectorial fixed point of $\vec{\varphi}$.

Without loss of generality, we assume every variable is bound only once in every formula. As a consequence, every subformula $\sigma_{i}\vec{X}.\vec{\psi}$ of a given formula $\varphi$ can then be referred to by $\varphi_{X_{i}}$.

The vertex set of the dependence graph of a formula $\varphi$ is the set of subformulas of $\varphi$. Edges go

• •

from ${\medcircle}\psi$ to $\psi$,

• •

from $\psi_{0}\vee\psi_{1}$ and $\psi_{0}\wedge\psi_{1}$ to $\psi_{0}$ and to $\psi_{1}$, and

• •

from $\sigma_{i}\vec{X}.\vec{\psi}$ to $\psi_{i}$.

A formula $\varphi$ has an alternation [16] if in its dependence graph there is a cycle with a $\mu$- and a $\nu$-subformula. We may assume that the formulas are such that the resulting automaton is guarded, that is, we only consider guarded formulas [3]: in every cycle in the dependence graph there is a ${\medcircle}$-subformula.

Just as for LTL, there is a straightforward inductive translation from alternation-free closed $\nu\text{TL}$ formulas into weak alternating automata, where, again, for each subformula $\psi$ there is a corresponding state $q_{\psi}$, see, for instance, [10, 11]:

[TABLE]

The states $q_{\psi}$ where $\psi$ is part of some cycle of a least fixed point formula in the dependence graph are non-recurring; the states $q_{\psi}$ where $\psi$ is part of some cycle with a greatest fixed point formula are recurring. For the other states, it does not matter whether they are recurring or non-recurring, because they do not belong to any cycle.

As every closed $\nu\text{TL}$-formula over some alphabet $A$ is true or not in a position of a given $\omega$-word, a tuple $\vec{\varphi}=\langle\varphi_{0},\dots,\varphi_{k-1}\rangle$ of closed-$\nu\text{TL}$ formulas $\varphi_{0},\dots,\varphi_{k-1}$ over $A$ defines a function $f_{\vec{\varphi}}\colon A^{\omega}\to(2^{\{0,\dots,k-1\}})^{\omega}$ by

[TABLE]

for every $u\in A^{\omega}$.

We obtain as an immediate consequence of the Main Theorem:

Corollary 2**.**

For every tuple $\vec{\varphi}$ of closed alternation-free $\nu\text{TL}$-formula $\varphi_{i}$ there exists a backward deterministic automaton $\mathscr{B}$ and an output function $\lambda$ for $\mathscr{B}$ such that the function defined by $\vec{\varphi}$ is the same as the function computed by $\mathscr{B}$ with respect to $\lambda$, that is, $f_{\vec{\varphi}}=f_{\mathscr{B},\lambda}$. The automaton $\mathscr{B}$ has the following properties.

Let $S_{0},\dots,S_{k-1}$ be an enumeration of all SCC’s of the dependence graph of $\vec{\varphi}$ and $m_{i}=S_{i}\cap Q$ for $i<k$. Then the number of states of $\mathscr{B}$ is less than $\prod_{i<k}(m_{i}+1)^{m_{i}}$, in particular, $(n+1)^{n}$ is an upper bound for the number of states of $\mathscr{B}$ when $n$ is the number of states of $\mathscr{A}$. 2. 2.

The automaton $\mathscr{B}$ has a generalized transition Büchi condition with as many Büchi sets as $\vec{\varphi}$ has subformulas.

3.3 From Büchi-automata to backward deterministic automata

In this section, we show how our construction can be combined with rank functions to obtain a transformation from non-deterministic Büchi automata to equivalent backward deterministic automata. The main idea is to first describe the canonical rank functions by Kupferman and Vardi in the alternation-free linear-time $\mu$-calculus and then use Corollary 2.

Background on canonical rank functions

Let $\mathscr{A}$ be a Büchi automaton given by some alphabet $A$, a finite set $Q$ of states, a set of initial states $I\subseteq Q$, a transition relation $\Delta\subseteq Q\times A\times Q$, and a Büchi set $B\subseteq Q$. Further, let $u\in A^{\omega}$.

We consider the run DAG of $\mathscr{A}$ on $u$, which is the graph with vertex set $\omega\times Q$ and an edges as follows. For every $i$, the graph contains all edges from $\langle i,q\rangle$ to $\langle i+1,q^{\prime}\rangle$ for $\langle q,u(i),q^{\prime}\rangle\in\Delta$, and no other edges.

In general, a leveled DAG is a graph with vertex set $\subseteq\omega\times Q$ and where every edge is from some vertex $\langle i,q\rangle$ to some vertex $\langle i+1,q^{\prime}\rangle$. Vertices in leveled DAG’s are classified as follows. A vertex is called

• •

finitary if it has only a finite number of descendants,

• •

$B$-tagged if its second component belongs to $B$,

• •

$B$-free if none of its descendants (including itself) is $B$-tagged,

• •

$B$-recurring if there is an infinite path with infinitely many $B$-tagged vertices and starting in the vertex.

The ultimate width of such a DAG is the limes inferior of the number of non-$B$-recurring infinitary vertices on a given level.

Consider a non-$B$-recurring infinitary vertex. By König’s lemma, there is an infinite path starting in it. Assume that every $B$-tagged strict descendant of the vertex is finitary. Then, after removing the finitary vertices, each successor of the vertex is $B$-free, but the infinite path is still there and all of its vertices (except, maybe, the first one) are removed in the second step, decreasing the ultimate width by one. If there is a $B$-tagged infinitary strict descendant of the vertex, apply the same argument to it. This cannot go ad infinitum, because a path with an infinite number of $B$-tagged vertices would be constructed.

So leveled DAG’s is that they can be decomposed in a simple fashion by repeating the following operation, here called peeling: first, remove all finitary vertices; second, remove all $B$-free vertices.

Fact 3**.**

[9]** For every Büchi automaton with $n$ states, peeling the run DAG of any $\omega$-word $n$ times yields the subgraph induced by the $B$-recurring vertices.

By the above, each vertex $v$ in a run DAG can be assigned a value in $\omega\cup\{\infty\}$ according to when the vertex is removed by peeling the DAG successively. More precisely, when $i$ is a natural number and all vertices with value $<2i$ are removed from the given DAG, the finitary vertices in the remaining DAG get assigned $2i$; when all vertices with value $<2i+1$ are removed, the $B$-free vertices in the remaining DAG get assigned $2i+1$. The $B$-recurring vertices get assigned $\infty$. The number assigned to a vertex $v$ is called its canonical rank, it is denoted $c(v)$, and, according to the above, it is $\infty$ or $<2n$, when $n$ is the width of the DAG started with.

Fact 4**.**

[5*]**

For a Büchi automaton with $n$ states, let $c$ be the canonical rank function of the run DAG of some $\omega$-word. The word is accepted from some state $q$ if, and only if, $c(\langle 0,q\rangle)=\infty$.*

Defining the canonical rank function in $\nu\text{TL}$

We next present $\nu\text{TL}$-formulas which define the canonical rank function for a given Büchi automaton $\mathscr{A}$ and any $\omega$-word.

Assume $\mathscr{A}$ has $n$ states, say $Q=\{q_{0},\dots,q_{n-1}\}$. For every $i<2n$ and $j<n$, we define a formula $\chi_{i}^{j}$ such that if $\chi_{i}^{j}$ is interpreted in some $\omega$-word $u$, then the value of $\chi_{i}^{j}$ is the set $\{k\in\omega\mid c(\langle k,q_{j}\rangle)\leq i\}$, where $c$ is the canonical rank function for the run DAG of $\mathscr{A}$ on $u$. In view of Fact 4, the tuple $\vec{\chi}$ defined by $\vec{\chi}=\langle\chi_{2n-1}^{0},\dots,\chi_{2n-1}^{n-1}\rangle$ defines the function we are interested in, more precisely, when each $\chi_{2n-1}^{j}$ is replaced by a formula denoting the negation of $\chi_{2n-1}^{j}$, which can easily be achieved.

We set

[TABLE]

where the $X_{i}^{j}$’s are distinct variables and the $\sigma_{i}$’s and $\varphi_{i}^{j}$’s are specified in what follows, by induction on $i$.

The formulas of the base case, $i=0$, are defined by

[TABLE]

The formulas essentially say that every vertex without successors has rank [math], and every vertex whose successors have rank [math] does so, too.

In the inductive step, we use $\vec{X_{i}}$ to denote the tuple $\langle X_{i}^{0},\dots,X_{i}^{n-1}\rangle$. We distinguish between $i$ odd and $i$ even. For odd $i$, say $i=2i^{\prime}+1$, we set $\sigma_{2i^{\prime}+1}=\nu$ and

[TABLE]

So the $\chi_{2i^{\prime}+1}^{j}$’s are to be read as follows: a $B$-tagged vertex has rank $\leq 2i^{\prime}+1$ only if its rank is $\leq 2i^{\prime}$; a non-$B$-tagged vertex has rank $\leq 2i^{\prime}+1$ if it has rank $\leq 2i^{\prime}$ or all its descendants have rank $\leq 2i^{\prime}+1$.

For even $i$, say $i=2i^{\prime}$ and $i^{\prime}>0$, we set $\sigma_{2i^{\prime}}=\mu$ and

[TABLE]

which is very similar to the formulas to the formulas in the base case.

A straightforward application of Corollary 2 to the above formulas leads to an upper bound of $O(n^{2})^{O(n^{2})}$, because $\vec{\chi}$ is of size quadratic in $n$ and has $2n^{2}$ variables. Observe, however, the following.

• •

Assume a fixed point formula is such that its dependence graph has the property that every path from a next subformula to another next subformula passes through a fixed point subformula. Then an optimized transformation into a weak alternating automaton results in as many states as there are fixed point variables. That is, we obtain only $2n^{2}$ states for the automaton corresponding to $\vec{\chi}$.

• •

The size of each SCC in such an automaton for $\vec{\chi}$ is $n$, because we have $n$ variables in every vectorial fixed point subformula.

• •

For a fixed $j$, the values of the fixed point expressions $\chi_{i}^{j}$ are pairwise disjoint sets.

This all implies:

Corollary 3**.**

The transformation of a non-deterministic Büchi automaton with $n$ states into a backward deterministic generalized transition Büchi automaton via $\nu\text{TL}$ and weak alternating automata results in a backward deterministic generalized transition Büchi automaton with $O((2n(n+1))^{n})$ states.

4 Conclusion

The translation from weak alternating to backward deterministic automata presented in the Main Theorem is indeed a general construction in the sense that from it other translations into backward deterministic $\omega$-automata can be derived. It remains open whether the Main Theorem and the translation presented in the section on applications can be fine-tuned (or improved) in such a way that the best known bounds can be met.