A Quasi-Linear Time Algorithm Deciding Whether Weak B\"uchi Automata Reading Vectors of Reals Recognize Saturated Languages

TL;DR

This paper presents a quasi-linear time algorithm to determine if weak deterministic B"uchi automata recognize saturated languages of real vectors, improving efficiency for standard and parallel encodings.

Contribution

It introduces a novel quasi-linear time decision procedure for recognizing saturated languages by weak B"uchi automata, applicable to multiple encoding schemes.

Findings

Algorithm runs in quasi-linear time for minimal automata.

Decides recognition of saturated languages for both sequential and parallel encodings.

Applicable to automata reading vectors of relative reals.

Abstract

This work considers weak deterministic B\"uchi automata reading encodings of non-negative $d$-vectors of reals in a fixed base. A saturated language is a language which contains all encoding of elements belonging to a set of $d$-vectors of reals. A Real Vector Automaton is an automaton which recognizes a saturated language. It is explained how to decide in quasi-linear time whether a minimal weak deterministic B\"uchi automaton is a Real Vector Automaton. The problem is solved both for the two standard encodings of vectors of numbers: the sequential encoding and the parallel encoding. This algorithm runs in linear time for minimal weak B\"uchi automata accepting set of reals. Finally, the same problem is also solved for parallel encoding of automata reading vectors of relative reals.

Equations

$$\displaystyle\begin{array}[]{lllllllllll c lllllllllllll}u=&0&\dots&0&\star&0&\dots&0&1&0&\dots&\text{ or }&u=&0&\dots&0&1&0&\dots&0&\star&0&\dots\\ x=&&\dots&&\star&&\dots&&k&&\dots&&x=&&\dots&&k&&\dots&&\star&&\dots&\end{array}$$

$$\displaystyle\mathopen{}\mathclose{{}\left[{v}}\right]_{b}^{I}=\sum_{i=0}^{\mathopen{}\mathclose{{}\left|{v}}\right|-1}b^{\mathopen{}\mathclose{{}\left|{v}}\right|-1-i}v[i]\text{ and }\mathopen{}\mathclose{{}\left[{w}}\right]_{b}^{F}=\sum_{i=0}^{\infty}b^{-i-1}w[i].$$

$$\mathopen{}\mathclose{{}\left[{w_{I}\star w_{F}}}\right]_{b}^{\mathbb{R}}=\mathopen{}\mathclose{{}\left[{w_{I}}}\right]_{b}^{I}+\mathopen{}\mathclose{{}\left[{w_{F}}}\right]_{b}^{F}.$$

$$\begin{array}[]{rclp{2mm}rclp{2mm}rclp{2mm}rclp{2mm}rcl}\mathopen{}\mathclose{{}\left[{(10)^{\omega}}}\right]_{2}^{F}&=&\frac{2}{3}&&\mathopen{}\mathclose{{}\left[{(01)^{\omega}}}\right]_{2}^{F}&=&\frac{1}{3}&&\mathopen{}\mathclose{{}\left[{0(10)^{\omega}}}\right]_{2}^{F}&=&\frac{1}{3}&&\mathopen{}\mathclose{{}\left[{0(1)^{\omega}}}\right]_{2}^{F}&=&\frac{1}{2}&&\mathopen{}\mathclose{{}\left[{1(0)^{\omega}}}\right]_{2}^{F}&=&\frac{1}{2}\\ \mathopen{}\mathclose{{}\left[{10}}\right]_{2}^{I}&=&2&&\mathopen{}\mathclose{{}\left[{1}}\right]_{2}^{I}&=&1&&\mathopen{}\mathclose{{}\left[{01}}\right]_{2}^{I}&=&1&&\mathopen{}\mathclose{{}\left[{\epsilon}}\right]_{2}^{I}&=&0&&\mathopen{}\mathclose{{}\left[{00000}}\right]_{2}^{I}&=&0\\ \lx@intercol\hfil\mathopen{}\mathclose{{}\left[{10\star(10)^{\omega}}}\right]_{2}^{\mathbb{R}}\lx@intercol&=&\frac{8}{3}&&\mathopen{}\mathclose{{}\left[{\star 0(1)^{\omega}}}\right]_{2}^{\mathbb{R}}&=&\frac{1}{2}&&\lx@intercol\hfil\mathopen{}\mathclose{{}\left[{00000\star 1(0)^{\omega}}}\right]_{2}^{\mathbb{R}}\lx@intercol&=&\frac{1}{2}.\end{array}$$

$$(va(b-1)^{\omega},\mathopen{}\mathclose{{}\left\{i}\right\})\text{ and }(v(a+1)0^{\omega},\mathopen{}\mathclose{{}\left\{i}\right\}),$$

$$\mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left({1\choose 0}{0\choose 0}{1\choose 0}^{\omega},\mathopen{}\mathclose{{}\left\{2}\right\}}\right)}}\right]_{b}^{\mathbb{R}}=\mathopen{}\mathclose{{}\left[{{1\choose 0}{0\choose 0}}}\right]_{b}^{I}+\mathopen{}\mathclose{{}\left[{{1\choose 0}^{\omega}}}\right]_{b}^{F}=\mathopen{}\mathclose{{}\left(2,0}\right)+\mathopen{}\mathclose{{}\left(\frac{2}{3},\frac{2}{3}}\right)=\mathopen{}\mathclose{{}\left(\frac{8}{3},\frac{2}{3}}\right).$$

$$\mathcal{A}^{\text{par}}=\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\{q_{\infty,\mathcal{A}},q_{[0,1],\mathcal{A}},q_{\emptyset,\mathcal{A}}}\right\},\Sigma_{2,d}\cup\mathopen{}\mathclose{{}\left\{\star}\right\},\delta,q_{\infty,\mathcal{A}},\mathopen{}\mathclose{{}\left\{q_{[0,1],\mathcal{A}}}\right\}}\right),$$

$$\mathcal{A}^{\text{seq}}=\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\{q_{\emptyset,\mathcal{A}},q_{[0,1],\mathcal{A}}}\right\}\cup\mathopen{}\mathclose{{}\left\{q_{i}\mid{i\in[d-1]}}\right\},\Sigma_{2}\cup\mathopen{}\mathclose{{}\left\{\star}\right\},\delta,q_{0},\mathopen{}\mathclose{{}\left\{q_{[0,1],\mathcal{A}}}\right\}}\right),$$

$$\mathcal{A}^{z\MVAt{}f}=\mathopen{}\mathclose{{}\left(Q,\Sigma_{b,d}^{\square\MVAt{}f}\cup\mathopen{}\mathclose{{}\left\{\star}\right\},\delta^{z\MVAt{}f},q_{0},F}\right),$$

$$\mathcal{A}^{z}=\mathopen{}\mathclose{{}\left(Q^{\prime},\Sigma_{b}\cup\mathopen{}\mathclose{{}\left\{\star,\square}\right\},\delta^{z},(q_{0},0),F}\right),$$

$$L_{\omega}\mathopen{}\mathclose{{}\left({\mathopen{}\mathclose{{}\left(\mathcal{A}^{(b-1)\MVAt{}f}}\right)_{\delta(q,\boldsymbol{a})}}}\right)=L_{\omega}\mathopen{}\mathclose{{}\left({\mathopen{}\mathclose{{}\left(\mathcal{A}^{0\MVAt{}f}}\right)_{\delta(q,\boldsymbol{a}^{\prime})}}}\right),$$

$$\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},S}\right\rangle\boldsymbol{a}\operatorname{fix}^{b-1\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},T}\right\rangle}\right)}\right)_{i}=\mathopen{}\mathclose{{}\left\langle v_{i},S}\right\rangle a_{i}\mathopen{}\mathclose{{}\left\langle w_{i},T}\right\rangle=\mathopen{}\mathclose{{}\left\langle v_{i},S}\right\rangle a^{\prime}_{i}\mathopen{}\mathclose{{}\left\langle w_{i},T}\right\rangle=\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},S}\right\rangle\boldsymbol{a}^{\prime}\operatorname{fix}^{0\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},T}\right\rangle}\right)}\right)_{i}.$$

$$\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},S}\right\rangle\boldsymbol{a}\operatorname{fix}^{b-1\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},T}\right\rangle}\right)}\right)_{f}=\mathopen{}\mathclose{{}\left\langle v_{f},S}\right\rangle a_{f}\mathopen{}\mathclose{{}\left\langle(b-1)^{\omega},T}\right\rangle$$

$$\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},S}\right\rangle\boldsymbol{a}^{\prime}\operatorname{fix}^{0\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},T}\right\rangle}\right)}\right)_{f}=\mathopen{}\mathclose{{}\left\langle v_{f},S}\right\rangle a^{\prime}_{f}\mathopen{}\mathclose{{}\left\langle 0^{\omega},T}\right\rangle=\mathopen{}\mathclose{{}\left\langle v_{f},S}\right\rangle(a_{f}+1)\mathopen{}\mathclose{{}\left\langle 0^{\omega},T}\right\rangle.$$

$$L_{\omega}\mathopen{}\mathclose{{}\left({\mathopen{}\mathclose{{}\left(\mathcal{A}^{(b-1)\MVAt{}f}}\right)_{\delta(q,\boldsymbol{a})}}}\right)=L_{\omega}\mathopen{}\mathclose{{}\left({\mathopen{}\mathclose{{}\left(\mathcal{A}^{0\MVAt{}f}}\right)_{\delta(q,\boldsymbol{a}^{\prime})}}}\right),$$

$$L_{\omega}\mathopen{}\mathclose{{}\left({\mathopen{}\mathclose{{}\left(\mathcal{A}^{(b-1)\MVAt{}f}}\right)}}\right)=L_{\omega}\mathopen{}\mathclose{{}\left({\mathopen{}\mathclose{{}\left(\mathcal{A}^{0\MVAt{}f}}\right)}}\right),$$

Full text

1 Introduction

This paper deals with logically defined sets of vector of numbers encoded by Büchi deterministic automata. The sets of vectors of integers whose encodings in base $b$ are recognized by a finite automaton are called the $b$-recognizable sets. By [BHMV94], the $b$-recognizable sets are exactly the sets which are \FO\mathopen{}\mathclose{{}\left[\mathbb{Z}{};+,<,V_{b}}\right]-definable, where $V_{b}(n)$ is the greatest power of $b$ dividing $n$. It was proven in [Sem77, Cob69] that the \FO\mathopen{}\mathclose{{}\left[\mathbb{N}{};+}\right]-definable sets are exactly the sets which are $b$- and $b^{\prime}$-recognizable for every $b\geq 2$.

Those results have then been extended to results about sets of vectors of reals recognized by a Büchi automata. The notion of Büchi automata is a formalism which describes languages of infinite words, also called $\omega$-words. The Büchi automata are similar to the finite automata. The main difference between the two kinds of automata is that a finite automaton accepts a finite word if it admits a run ending on accepting states, while a Büchi automaton accepts an infinite word it it admits a run in which an accepting state appears infinitely often.

One of the main differences between finite and Büchi automata is that finite automata can be determinized while deterministic Büchi automata are less expressive than Büchi automata. For example, the language $L_{\text{fin }a}$ of words containing a finite number of times the letter $a$ is recognized by a Büchi automaton, but is not recognized by any deterministic Büchi automaton. This statement implies, for example, that no deterministic Büchi automaton recognizes the set of reals of the form $nb^{p}$ with $n\in\mathbb{N}{}$ and $p\in\mathbb{Z}{}$, that is, the reals which admits no encoding in base $b$ with a finite number of non-0 digits.

Another main difference between the two classes of automata is that the class of languages recognized by finite automata is closed under complement while the class of languages recognized by deterministic Büchi automata is not closed under complement. For example, $L_{\text{inf }a}$, the complement of $L_{\text{fin }a}$, is recognized by a deterministic Büchi automaton.

Real numbers are naturally encoded, in a base $b>1$, as a sequence of digits in \mathopen{}\mathclose{{}\left\{0,\dots,b-1}\right\} and a separator symbol $\star$. That is, as a word over the alphabet \mathopen{}\mathclose{{}\left\{0,\dots,b-1,\star}\right\}. Similarly, a $d$-vector of real numbers can be encoded as a word over alphabet \mathopen{}\mathclose{{}\left\{0,\dots,b-1}\right\}^{d}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}, where $d$ digits are read simultaneously, one for each element of the vector. This is call the $d$-parallel encoding of the vector. A $d$-vector can also be encoded as a word over alphabet \mathopen{}\mathclose{{}\left\{0,\dots,b-1,\star}\right\}, assuming that the digits in position $i$ modulo $d$ corresponds to the digits of the $i$-th element of the vector. This is call the sequential encoding of the vector of digits. The cardinality of the alphabet of parallel encoding is exponentially bigger than the cardinality of the alphabet of sequential encodings, thus, sequential encodings may be preferred for practical purposes. Parallel encoding leads to simpler notation, hence, most of the litterature consider parallel encodings. We consider both encodings in this paper.

A language $L$ is said to be saturated if, given a vector $\mathbf{r}\in\mathbb{R}^{d}$, the set of its encoding in base $b$ is either included in $L$ or disjoint from $L$. A Real Vector Automaton (RVA, See e.g. [BBL09]) is an automaton of alphabet \mathopen{}\mathclose{{}\left\{0,\dots,b-1}\right\}^{d}\cup\mathopen{}\mathclose{{}\left\{\star}\right\} which recognizes a saturated language. Here $d$ is the dimension of the vector that the automata read. In the case where the dimension $d$ is 1, those automata are called Real Number Automata (RNA, See e.g. [BBB10]).

The sets of vectors of reals whose encodings in base $b$ is recognized by a RVA are called the $b$-recognizable sets. By [WB00], they are exactly the \FO\mathopen{}\mathclose{{}\left[\mathbb{R},\mathbb{Z}{};+,<,X_{b},1}\right]-definable sets. The logic \FO\mathopen{}\mathclose{{}\left[\mathbb{R},\mathbb{Z}{};+,<,X_{b},1}\right] is the first-order logic over reals with a unary predicate which holds over integers, addition, order, the constant one, and the function $X_{b}(x,u,k)$. The function $X_{b}(x,u,k)$ holds if and only if $u$ is equal to some $b^{n}$ with $n\in\mathbb{Z}{}$ and there exists a encoding in base $b$ of $x$ whose digit in position $n$ is $k$. That is, $u$ and $x$ are of the form:

[TABLE]

A weak deterministic Büchi automaton is a deterministic Büchi automaton whose set of accepting states is a union of strongly connected components. A set is said to be weakly $b$-recognizable if it is recognized by a weak automaton in base $b$. By [BBL09], a set is \FO\mathopen{}\mathclose{{}\left[\mathbb{R},\mathbb{Z}{};+,<}\right]-definable if and only if its set of encodings is weakly $b$-recognizable for all $b\geq 2$. The weak deterministic Büchi automata are less expressive than the deterministic Büchi automata. For example, the language $L_{\text{inf }a}$ of words containing an infinite number of $a$ is recognized by a deterministic Büchi automaton but is not recognized by any weak deterministic Büchi automaton. This implies that, for example, no weak deterministic Büchi automaton recognizes the set of reals which are not of the form $nb^{p}$ with $n\in\mathbb{N}{}$ and $p\in\mathbb{Z}{}$, since those reals are the ones whose encodings in base $b$ contains an infinite number of non-[math] digits. Furthermore, by [Lö01], weak deterministic Büchi automata can be efficiently minimized.

In this paper, we show that we can efficiently decide whether a weak Büchi automaton accept a saturated set of vectors of integers. Furthermore, we give an algorithm for automata reading parallel encoding and for automata reading sequential encoding.

We recall standard definition in Section 2. We introduce encoding of sets of vectors of numbers in Section 3. We introduce Büchi automata in Section 4. We formalize how we compute the complexity of an algorithm in Section 5. We study automata reading vectors of numbers in Section 6. We study how to transform words and automata in Section 7. We characterize the parallel RVA in Section 8 and the sequential RVA in Section 9. We explain how to decide whether an automaton is a RVA in Section 10. The case of sets containing negative reals is discussed in Section 11.

2 Standard definitions

We now give the standard definitions used in this paper.

Numbers.

Let $\mathbb{N}{}$ and $\mathbb{R}$ denote the set of non-negative integers and the set of reals, respectively. For $R\subseteq\mathbb{R}$, let $R^{\geq 0}$ denote the set of non-negative elements of $R$. For $n\in\mathbb{N}{}$, let $[n]$ represent \mathopen{}\mathclose{{}\left\{0,\dots,n}\right\}. For $m\in\mathbb{N}{}^{>0}$, let $(n\mod m)$ represents the only integer $i\in[m-1]$ such that $n\equiv i\mod m$.

Sets.

For $S$ and $T$ two sets, let S\otimes T=\mathopen{}\mathclose{{}\left\{(s,t)\mid s\in S,t\in T}\right\} be the set of ordered pair containing an element of $S$ and an element of $T$. Let $|S|$ be the cardinality of $S$. For $d\in\mathbb{N}$, let $S^{d}$ be the set of $d$-vectors of elements of $S$ for $d\in\mathbb{N}$. The $d$-vectors are denoted $\boldsymbol{s}=(s_{0},\dots,s_{d-1})$ with each $s_{i}\in S$. The $d$-vector $(0,\dots,0)$ is denoted $\boldsymbol{0}$.

Finite and infinite words.

An alphabet is a finite set, its elements are called letters. A finite word over the alphabet $A$ is a finite sequence of letters of $A$. An $\omega$-word over the alphabet $A$ is an infinite sequence of letters of $A$. The empty word is denoted $\epsilon$. A set of finite (respectively $\omega-$) words of alphabet $A$ is called a language (respectively, an $\omega$-language) over alphabet $A$.

Let $w$ be a word, its length is denoted \mathopen{}\mathclose{{}\left|{w}}\right|, it is either a non-negative integer or the cardinality of $\mathbb{N}{}$. For n\in[\mathopen{}\mathclose{{}\left|{w}}\right|-1], let $w[n]$ denote the $n$-th letter of $w$. For $v$ a finite word, let $u=vw$ be the concatenation of $v$ and of $w$, that is, the word of length \mathopen{}\mathclose{{}\left|{v}}\right|+\mathopen{}\mathclose{{}\left|{w}}\right| such that $u[i]=v[i]$ for i\in[\mathopen{}\mathclose{{}\left|{v}}\right|-1] and u[\mathopen{}\mathclose{{}\left|{v}}\right|+i]=w[i] for i\in[\mathopen{}\mathclose{{}\left|{w}}\right|-1]. Let w\mathopen{}\mathclose{{}\left[<n}\right] denote the prefix of $w$ of length $n$, that is, the word $u$ of length $n$ such that $w[i]=u[i]$ for all $i\in[n-1]$. Similarly, let w\mathopen{}\mathclose{{}\left[\geq{}n}\right] denote the suffix of $w$ without its $n$-th first letters, that is, the word $u$ such that $u[i]=w[i+n]$ for all i\in[\mathopen{}\mathclose{{}\left|{w}}\right|-n]. Note that w=w\mathopen{}\mathclose{{}\left[<i}\right]w\mathopen{}\mathclose{{}\left[\geq{}i}\right] for all i\in[\mathopen{}\mathclose{{}\left|{w}}\right|-1].

Languages

A language is a set of words. Let $L$ be a language of finite words and let $L^{\prime}$ be either an $\omega$-languages or a language of finite words. Let $LL^{\prime}$ be the set of concatenations of the words of $L$ and of $L$. For $i\in\mathbb{N}{}$, let $L^{i}$ be the concatenations of $i$ words of $L$. Let $L^{*}=\bigcup_{i\in\mathbb{N}{}}L^{i}$, more generally, for $d,j\in\mathbb{N}{}$, let $L^{d\mathbb{N}{}+j}=\bigcup_{i\in\mathbb{N}{}}L^{di+j}$ and $L^{+}=\bigcup_{i>0}L^{i}$. If $L$ is a set of non-empty word, let $L^{\omega}$ be the set of infinite sequences of elements of $L$. Finally, let $L^{\infty}=L^{*}\cup L^{\omega}$.

3 Encoding of set of vectors of numbers

In this section we explain how to encode sets of vectors of numbers using languages. We consider natural and real numbers in Section 3.1. We consider the special case of rationals in Section 3.2. We then consider vectors of reals in Section 3.3. Finally, we consider sets of vectors of reals in Section 3.4.

3.1 Encoding of numbers

Let us now consider the encoding of numbers in an integer base $b\geq 2$. Let $\Sigma_{b}$ be equal to $[b-1]$, it is the set of digits. The base $b>1$ is fixed for the remaining of this paper. Formally, for $v\in\Sigma_{b}^{*}$ and $w\in\Sigma_{b}^{\omega}$:

[TABLE]

Let $w$ be an $\omega$-word with exactly one $\star$. It is of the form $w=w_{I}\star w_{F}$, with $w_{I}\in\Sigma_{b}^{*}$ and $w_{F}\in\Sigma_{b}^{\omega}$. The word $w_{I}$ is called the natural part of $w$ and the $\omega$-word $w_{F}$ is called its fractional part. We then define:

[TABLE]

Examples of representation of numbers are now given.

[TABLE]

Pair-encoding

A word w\in\Sigma_{b}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}^{\infty} can equivalently be encoded as a pair \mathopen{}\mathclose{{}\left\langle w,S}\right\rangle where $w\in\Sigma_{b}^{\infty}$ and $S\subseteq\mathbb{N}{}$. This pair represents the word of length \mathopen{}\mathclose{{}\left|{w}}\right|+|S|, such that \mathopen{}\mathclose{{}\left\langle w,S}\right\rangle[i] is $\star$ if $i\in S$, otherwise it is w\mathopen{}\mathclose{{}\left[i-|\mathopen{}\mathclose{{}\left\{s\in S\mid s<i}\right\}|}\right]. Intuitively, for $i\not\in S$, the $i$-th letter of \mathopen{}\mathclose{{}\left\langle w,S}\right\rangle[i] is the letter of $w$ at a position $j$ such that $j+k=i$, where $k$ is the number of $\star$’s before $i$. For example \mathopen{}\mathclose{{}\left\langle(10)^{\omega},\mathopen{}\mathclose{{}\left\{2}\right\}}\right\rangle=10\star(10)^{\omega}, \mathopen{}\mathclose{{}\left\langle 01,\mathopen{}\mathclose{{}\left\{0}\right\}}\right\rangle=\star 01 and \mathopen{}\mathclose{{}\left\langle(01)^{\omega},\emptyset}\right\rangle=(01)^{\omega}. The representation \mathopen{}\mathclose{{}\left\langle w,S}\right\rangle is called a pair-encoding.

If \mathopen{}\mathclose{{}\left\langle w,S}\right\rangle is an encoding of a real, or an encoding of a factor of a real, $S$’s cardinality is at most 1. In particular, the pair encoding of a word of $\Sigma_{b}^{*}\star\Sigma_{b}^{\omega}$ is of the form \mathopen{}\mathclose{{}\left\langle w,\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle with $w\in\Sigma_{b}^{\omega}$ and $s\in\mathbb{N}{}$. Note however that in order to check whether an automaton is a RVA, it must be checked that it rejects every words whose number of $\star$’s is not 1. Therefore, the cases where $S$ is not a singleton must be considered.

3.2 Encoding of rationals

We now recall a basic fact about encoding of rationals.

Theorem 3.1** ([HW60]).**

Let $q\geq 0$ a real. Let l=\mathopen{}\mathclose{{}\left\lceil{\log_{b}(q+1)}}\right\rceil and $l^{\prime}\in\mathbb{N}{}$.

The number of encoding of $q$ with a natural part of length $l^{\prime}$ is:

• •

[math]* if $l^{\prime}<l$,*

• •

$2$* if $l^{\prime}\geq l$ and if $q$ admits a decomposotion of the form $nb^{p}$ with $p\in\mathbb{Z}$ and $n\in\mathbb{N}$ such that $n\not\equiv 0\mod b$, and*

• •

$1$* otherwise.*

In the seconde case, the two encodings are of the form:

[TABLE]

with $v\in\Sigma_{b}^{*}$ and a\in\Sigma_{b}\setminus\mathopen{}\mathclose{{}\left\{b-1}\right\}.

This theorem illustrates that pair-encoding leads to shorter statements. Indeed, with the standard-encoding, Equation (2) would require to consider three cases, depending on whether $p<0$, $p=0$ or $p>0$. Note that the condition $n\not\equiv 0\mod b$ ensures that $q\neq 0$.

3.3 Encoding of vectors of reals.

It is now explained how to encode $d$-vectors of real numbers. In this paper, we fix a positive integer constant $d$. In the remaining of this paper, we only consider sets of dimension 1 or $d$.

There exists two standard encodings of vectors of numbers. The parallel one and the sequential one. A parallel encoding consists in a sequence of $d$-vector of digits. A sequential encoding consists in a sequence of digits. This sequence contains alternatively a digit of the zeroth number, a digit of the first number, up to a digit of the $(d-1)$-th number. In both cases, exactly one dot appear in the sequence, to separate the natural part from the fractional part.

The alphabet of sequential encoding contains $(b+1)$ letters while the alphabet of parallel encodings contains $(b^{d})+1$ letters. Thus, sequential encoding allow to create smaller automata, as shown in Example 6.1. However, parallel encoding leads to notations which are more compact. Since parallel encoding are more standards and lead to simpler proofs.

Parallel encodings

We now introduce the notion of parallel encoding of a $d$-vector of numbers. Let $\Sigma_{b,d}=\Sigma_{b}^{d}$, be the set of $d$-vectors of digits. For $\boldsymbol{w}\in\Sigma_{b,d}^{\infty}$, and $0\leq i<d$, $w_{i}$ denote the unique word such that \mathopen{}\mathclose{{}\left|{w_{i}}}\right|=\mathopen{}\mathclose{{}\left|{\boldsymbol{w}}}\right| and such that for 0\leq k<\mathopen{}\mathclose{{}\left|{\boldsymbol{w}}}\right|, $(w_{i})[k]=(\boldsymbol{w}[k])_{i}$. Similarly, for \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle\in\mathopen{}\mathclose{{}\left(\Sigma_{b,d}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}}\right)^{\infty}, \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle_{i} denote \mathopen{}\mathclose{{}\left\langle w_{i},S}\right\rangle.

For $\boldsymbol{v}\in\Sigma_{b,d}^{*}$ and $\boldsymbol{w}\in\Sigma_{b,d}^{\omega}$, we define \mathopen{}\mathclose{{}\left[{\boldsymbol{v}}}\right]_{b}^{I} as \mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left[{v_{0}}}\right]_{b}^{I},\dots,\mathopen{}\mathclose{{}\left[{v_{d-1}}}\right]_{b}^{I}}\right) and \mathopen{}\mathclose{{}\left[{\boldsymbol{w}}}\right]_{b}^{F} as \mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left[{w_{0}}}\right]_{b}^{F},\dots,\mathopen{}\mathclose{{}\left[{w_{d-1}}}\right]_{b}^{F}}\right). Similarly, we define \mathopen{}\mathclose{{}\left[{\boldsymbol{v\star w}}}\right]_{b}^{\mathbb{R}} as \mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left[{v_{0}\star w_{0}}}\right]_{b}^{\mathbb{R}},\dots,\mathopen{}\mathclose{{}\left[{v_{d-1}\star w_{d-1}}}\right]_{b}^{\mathbb{R}}}\right)=\mathopen{}\mathclose{{}\left[{\boldsymbol{v}}}\right]_{b}^{I}+\mathopen{}\mathclose{{}\left[{\boldsymbol{w}}}\right]_{b}^{F} where addition is defined component by component. For example:

[TABLE]

Sequential encodings

We now introduce the notion of sequential encodings of a $d$-vector of numbers. Let $w\in\Sigma_{b}^{\infty}$ whose length is either a multiple of $d$ or infinite. Let \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(w}\right)\in\Sigma_{b,d} be the only word of length \mathopen{}\mathclose{{}\left|{w}}\right|/d, whose $i$-th letter is \mathopen{}\mathclose{{}\left(w_{di+0},\dots,w_{di+(d-1)}}\right) for i<\mathopen{}\mathclose{{}\left|{w}}\right|/d. For \mathopen{}\mathclose{{}\left\langle w,S}\right\rangle, with $S$ a set of multiple of $d$, let \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle w,S}\right\rangle}\right)=\mathopen{}\mathclose{{}\left\langle\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(w}\right),\mathopen{}\mathclose{{}\left\{s/d\mid s\in S}\right\}}\right\rangle. Let \operatorname{seq}_{d}\mathopen{}\mathclose{{}\left(\boldsymbol{w}}\right) be the inverse of the function \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(w}\right). Given a word $w$, \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(w}\right) is called the parallelization of $w$ and \operatorname{seq}_{d}\mathopen{}\mathclose{{}\left(w}\right) is called its sequentialization. For example, the parallelization of \mathopen{}\mathclose{{}\left(100(01)^{\omega},\mathopen{}\mathclose{{}\left\{4}\right\}}\right) is \mathopen{}\mathclose{{}\left({1\choose 0}{0\choose 0}{1\choose 0}^{\omega},\mathopen{}\mathclose{{}\left\{2}\right\}}\right). As seen in Equation (3), it encodes the pair of reals $(8/3,2/3)$.

3.4 Encoding of sets of vectors of reals

We now explain how to encode sets of tuples of reals as a language.

$d$-parallel languages

The subsets of $\Sigma_{b,d}^{*}\star\Sigma_{b,d}^{\omega}$ are called $d$-parallel language. Given a $d$-parallel language $L$, let \mathopen{}\mathclose{{}\left[{L}}\right]_{b}^{\mathbb{R}} be the set of vectors of reals admitting an encoding in $L$. Formally, \mathopen{}\mathclose{{}\left[{L}}\right]_{b}^{\mathbb{R}}=\mathopen{}\mathclose{{}\left\{\mathopen{}\mathclose{{}\left[{\boldsymbol{w}}}\right]_{b}^{\mathbb{R}}\mid\boldsymbol{w}\in L}\right\}. The language $L$ is said to be a $d$-parallel encoding of the set of reals \mathopen{}\mathclose{{}\left[{L}}\right]_{b}^{\mathbb{R}}. A $d$-parallel language $L\subseteq\Sigma_{b,d}^{*}\star\Sigma_{b,d}^{\omega}$ is said to be saturated if, for any $d$-vector of numbers \mathbf{r}\in\mathopen{}\mathclose{{}\left[{L}}\right]_{b}^{\mathbb{R}}, all encodings in base $b$ of $\mathbf{r}$ belongs to $L$.

In general, a set of reals may have infinitely many encodings in base $b$. For example, for $I\subseteq\mathbb{N}$ an arbitrary set, the languagse \mathopen{}\mathclose{{}\left\{0,1}\right\}^{*}\star\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\{0,1}\right\}^{\omega}\setminus\mathopen{}\mathclose{{}\left\{0^{i}1^{\omega}\mid i\in I}\right\}}\right) is an encoding in base 2 of $\mathbb{R}^{\geq 0}$. It is saturated only for $I=\emptyset$.

$d$-sequential languages

The case of $d$-sequential encodings of vectors of reals is now considered. The subsets of $\Sigma_{b}^{d\mathbb{N}{}}\star\Sigma_{b}^{\omega}$ are called $d$-sequential languages. The parallelization of a $d$-sequential language $L$, denoted \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(L}\right) is \mathopen{}\mathclose{{}\left\{\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(w}\right)\mid w\in L}\right\}. A $d$-sequential language $L$ is said to be a $d$-sequential encoding of the set \mathopen{}\mathclose{{}\left[{\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(L}\right)}}\right]_{b}^{\mathbb{R}}. This language is said to be saturated if \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(L}\right) is saturated.

4 Deterministic Büchi automata

This paper deals with deterministic Büchi automata. We define this notion in Section 4.1. We consider the notion of quotient and morphism of Büchi automata in Section 4.2.

4.1 Definition

A deterministic Büchi automaton is a 5-tuple \mathopen{}\mathclose{{}\left(Q,A,\delta,q_{0},F}\right), with $Q$ a finite set of states, $A$ an alphabet, $\delta:Q\otimes A\to{}Q$ is the transition function, $q_{0}\in Q$ is the initial state and $F\subseteq Q$ is the set of accepting states. For each $q\in Q$ and $a\in A$, $q$ is said to be a predecessor of $\delta(q,a)$. For $q\in Q$, let $\mathcal{A}_{q}$ be the automaton \mathopen{}\mathclose{{}\left(Q,A,\delta,q,F}\right), that is $\mathcal{A}$ with $q$ as initial state. A state $q\in Q$ is said to be accessible from a state $q^{\prime}\in Q$ if there exists a finite non-empty word $w\in A^{+}$ such that $\delta(q^{\prime},w)={q}$. The strongly connected component of a state $q$ is the set of states $q^{\prime}$ such that $q^{\prime}$ is accessible from $q$ and $q$ is accessible from $q^{\prime}$.

From now on in this paper, all Büchi automata are assumed to be deterministic. The function $\delta$ is implicitly extended on $Q\otimes A^{*}$ by $\delta(q,\epsilon)=q$ and $\delta(q,aw)=\delta(\delta(q,a),w)$ for $a\in A$ and $w\in A^{*}$. An example of Büchi automaton is now given.

Example \theexample.

Let $\mathcal{A}$ be the automaton pictured in Figure 1. Its alphabet is \Sigma_{3}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}.

Let $\mathcal{A}$ be an automaton and $w$ be an infinite word. A run $\pi$ of $\mathcal{A}$ on $w$ is a mapping $\pi:\mathbb{N}{}\mapsto Q$ such that $\pi(0)=q_{0}$ and $\delta(\pi(i),w[i])={\pi(i+1)}$ for all i<\mathopen{}\mathclose{{}\left|{w}}\right|. The run is accepting if there exists a state $q\in F$ such that there is an infinite number of $i\in\mathbb{N}{}$ such that $\pi(i)=q$. Section 4.1 is now resumed. Note that, if $\mathcal{A}$ is an automaton, for all $w\in A^{*}$ and $w^{\prime}\in A^{\omega}$, the word $w^{\prime}$ is accepted by $\mathcal{A}_{\delta(q_{0},w)}$ if and only if $ww^{\prime}$ is accepted by $\mathcal{A}$. It is said that $\mathcal{A}$ recognize the language of words $w$ such that $\mathcal{A}$ accepts $w$. This language is denoted L_{\omega}\mathopen{}\mathclose{{}\left({\mathcal{A}}}\right).

Example \theexample.

Let $\mathcal{A}$ be the automaton pictured in Figure 1. The run of $\mathcal{A}$ on $01^{\omega}$ is \mathopen{}\mathclose{{}\left(q_{0},q_{1},q_{3},\dots}\right), with the last state repeated infinitely often. The Büchi automaton $\mathcal{A}$ does not accept $01^{\omega}$ since this run contains exactly one accepting state.

The run of $\mathcal{A}$ on $2\star 1^{\omega}$ is \mathopen{}\mathclose{{}\left(q_{0},q_{3},q_{5},\dots}\right) with the last state repeated infinitely often. The Büchi automaton $\mathcal{A}$ accepts $2\star 1^{\omega}$ since the accepting state $q_{5}$ appears infinitely often in the run.

This automaton recognizes the language $(00)^{*}(01,2)\Sigma_{3}^{*}\star\Sigma_{3}^{\omega}$.

4.2 Quotients, Morphisms and Weak Büchi Automata

Let \mathcal{A}=\mathopen{}\mathclose{{}\left(Q,A,\delta,q_{0},F}\right) and \mathcal{A}^{\prime}=\mathopen{}\mathclose{{}\left(Q^{\prime},A,\delta^{\prime},q_{0}^{\prime},F^{\prime}}\right) be two Büchi automata. The Büchi automaton $\mathcal{A}$ is said to be minimal if, for each distinct states $q$ and $q^{\prime}$ of $\mathcal{A}$, L_{\omega}\mathopen{}\mathclose{{}\left({\mathcal{A}_{q}}}\right)\neq L_{\omega}\mathopen{}\mathclose{{}\left({\mathcal{A}_{q^{\prime}}}}\right). If $\mathcal{A}^{\prime}$ is minimal, a surjective function $\mu:Q\to Q^{\prime}$ is a morphism of Büchi automata if $\mu(q_{0})=q_{0}^{\prime}$ and if, for each $q\in Q$, L_{\omega}\mathopen{}\mathclose{{}\left({\mathcal{A}_{q}}}\right)=L_{\omega}\mathopen{}\mathclose{{}\left({Aut^{\prime}_{\mu(q)}}}\right). Note that if $\mu$ is a morphism of Büchi automaton from $\mathcal{A}$ to $\mathcal{A}^{\prime}$, if $q$ is a state of $\mathcal{A}$, then $\mu$ is a morphism of Büchi automaton from $\mathcal{A}_{q}$ to $Aut^{\prime}_{\mu(q)}$.

The Büchi automaton $\mathcal{A}$ is said to be weak if $F$ is a union of strongly connected components. The main theorem concerning quotient of weak Büchi automata is now recalled.

Theorem 4.1** ([Lö01]).**

Let $\mathcal{A}$ be a weak Büchi automaton with $n$ states such that all states of $\mathcal{A}$ are accessible from its initial state. Let $c$ be the cardinality of $A$. There exists a minimal weak Büchi automaton $\mathcal{A}^{\prime}$ such that there exists a morphism of automaton $\mu$ from $\mathcal{A}$ to $\mathcal{A}^{\prime}$. The automaton $\mathcal{A}^{\prime}$ and the morphism $\mu$ are computable in time O\mathopen{}\mathclose{{}\left(n\log(n)c}\right) and space O\mathopen{}\mathclose{{}\left(nc}\right).

Example 4.1 is now resumed.

Example \theexample.

Let $\mathcal{A}_{R}$ be the Büchi automaton pictured in Figure 1. The automaton $\mathcal{A}_{R}$ is weak. Its minimal quotient is pictured in Figure 2. Note that this quotient is not a quotient of finite automata since the accepting state $q_{0}$ is sent to a non-accepting state.

We now explain how to decide efficiently whether two states of two automata recognize the same language.

Corollary \thecorollary.

Let $A$ an alphabet with $c>1$ letters. Let \mathcal{A}^{0}=\mathopen{}\mathclose{{}\left(Q^{0},A,\delta^{0},q^{0}_{0},F^{0}}\right), \mathcal{A}^{1}=\mathopen{}\mathclose{{}\left(Q^{1},A,\delta^{1},q^{1}_{0},F^{1}}\right) be weak Büchi automata. Let $n=|Q^{0}|+|Q^{1}|$.

We can compute in time O\mathopen{}\mathclose{{}\left(n\log(n)c}\right) and space O\mathopen{}\mathclose{{}\left(nc}\right) a data-structure of size O\mathopen{}\mathclose{{}\left(nc}\right) such that, for each pair $(q^{0},q^{1})\in Q^{0}\otimes Q^{1}$, we can check in constant time and space whether $\mathcal{A}^{0}_{q^{0}}$ and $\mathcal{A}^{1}_{q^{1}}$ accepts the same language.

Proof.

Up to changing the name of the states, we can assume that $Q^{0}$ and $Q^{1}$ are disjoint. Let $\alpha\in A$. Let \mathcal{A}^{\prime}=\mathopen{}\mathclose{{}\left(Q^{0}\cup Q^{1}\cup\mathopen{}\mathclose{{}\left\{q_{0}}\right\},A,\delta^{\prime},q_{0}^{\prime},F^{0}\cup F^{1}}\right), where $\delta^{\prime}(q_{0},\alpha)=q_{0}^{0}$, $\delta^{\prime}(q_{0},a)=q_{0}^{1}$ for each a\in A\setminus\mathopen{}\mathclose{{}\left\{a}\right\}, and $\delta^{\prime}(q,a)=\delta^{i}(q,a)$ for i\in\mathopen{}\mathclose{{}\left\{0,1}\right\}, $a\in A$ and $q\in Q^{i}$. Clearly $\mathcal{A}^{i}_{q}$ accepts the same language than $\mathcal{A}^{\prime}_{q}$, for each $q\in Q^{i}$. The automaton $\mathcal{A}^{\prime}$ is clearly weak, thus it admits a minimal quotient and a morphism $\mu$ to this minimal quotient. By Theorem 4.1, this morphism is computable in time O\mathopen{}\mathclose{{}\left(n\log(n)c}\right) and takes space O\mathopen{}\mathclose{{}\left(nc}\right). This morphism is the data structure mentionned above.

Let $(q^{0},q^{1})\in Q^{0}\otimes Q^{1}$. Remark that $\mathcal{A}^{0}_{q^{0}}$ and $\mathcal{A}^{1}_{q^{1}}$ accepts the same language if and only if $\mu(q^{0})=\mu(q^{1})$. Given $\mu,$ this equality can be checked in constant time and space. ∎

In practice, the algorithm of [Lö01] could be directly applied to multiple Büchi automata simultaneously. Indeed, the initial state is not considered differently than any other state in this algorithm. Furtherrmore, this algorithm does not require all states of the automata to be accessible from the initial state.

5 Time and space analysis

We now state our assumption above the time and space complexity of in this paper. We first consider the size of the object we use.

All integers and Booleans takes constant space. The size of an automata is the product of the cardinalities of its alphabet and of its set of states. An array of $n$ elements takes size $n$, plus the size of its elements. For a set $S$ of cardinality $n$, a subset of $S$ is an array of $n$ Boolean values.

For the sake of simplicity, it is assumed that all basic arithmetic operations over integers, such as addition, multiplication, subtraction, comparison of integers, can be computed in constant time and space. The transition functions of automata return in constant time and space. Creating an array and editing one of its position takes constant time.

6 Automata reading set of vectors of reals

We consider automata reading set of vectors of reals in this section. Those automata are formally introduced in Section 6.1. We explain in Section 6.2 how to decide whether an automaton accept a $d$-parallel or a $d$-sequential language.

6.1 Definition

The notion of Büchi automata recognizing a set of vector of reals is now introduced.

A Büchi automaton accepting a $d$-parallel or a $d$-sequential language is said to be a $d$-parallel or a $d$-sequential automaton respectively. The set of weak $d$-parallel and of weak $d$-sequential Büchi automata are closed under taking quotient. The set of $d$-vectors of automata associated to an automaton is now introduced.

Notation \thenotation (\mathopen{}\mathclose{{}\left[{\mathcal{A}}}\right]_{b}^{\mathbb{R}}).

For $\mathcal{A}$ a $d$-parallel or a $d$-sequential automaton, let \mathopen{}\mathclose{{}\left[{\mathcal{A}}}\right]_{b}^{\mathbb{R}} be \mathopen{}\mathclose{{}\left[{L_{\omega}\mathopen{}\mathclose{{}\left({\mathcal{A}}}\right)}}\right]_{b}^{\mathbb{R}}.

The following example show that the minimal $d$-sequential automaton accepting a set R\subseteq\mathopen{}\mathclose{{}\left(\mathbb{R}^{\geq 0}}\right)^{d} can be exponentially smaller than the minimal $d$-parallel automaton accepting it.

Example \theexample.

The minimal $d$-parallel automaton accepting $(\mathbb{R}^{\geq 0})^{d}$ is:

[TABLE]

where $\delta(q,\boldsymbol{a})=q$ for each state $q$, and each letter $\boldsymbol{a}\in\Sigma_{2,d}$ and where $\delta(q_{\infty,\mathcal{A}},\star)=q_{[0,1],\mathcal{A}}$. If $\delta(q,a)$ is not defined above, it is equal to $q_{\emptyset,\mathcal{A}}$. This Büchi automaton has $3$ states and its alphabet has $2^{d}+1$ letters, hence its size is O\mathopen{}\mathclose{{}\left(2^{d}}\right). The automaton $\mathcal{A}^{\text{par}}$ is pictured in 3(a), without its state $q_{\emptyset,\mathcal{A}}$.

The minimal $d$-sequential Büchi automaton accepting \mathopen{}\mathclose{{}\left(\mathbb{R}^{\geq 0}}\right)^{d} is:

[TABLE]

where, $\delta(q_{i},a)=q_{i+1}$ for each $a\in\Sigma_{2}$, where $\delta(q_{[0,1],\mathcal{A}},a)=q_{[0,1],\mathcal{A}}$ for each $a\in\Sigma_{2}$ and where $\delta(q_{0},\star)=q_{[0,1],\mathcal{A}}$. If $\delta(q,a)$ is not defined above, it is equal to $q_{\emptyset,\mathcal{A}}$. This Büchi automaton has $d+2$ states and its alphabet has $2$ letters, hence its size is O\mathopen{}\mathclose{{}\left(d}\right). The automaton $\mathcal{A}^{\text{par}}$ is pictured in 3(b) without its state $q_{\emptyset,\mathcal{A}}$.

Note that the size of the minimal $d$-parallel automaton is exponential in the size of the minimal $d$-sequential automaton.

We now explain how to transform a sequential automaton into a parallel one.

Definition \thedefinition (\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathcal{A}}\right)).

Let \mathcal{A}=\mathopen{}\mathclose{{}\left(Q,\Sigma_{b}\cup\mathopen{}\mathclose{{}\left\{\star}\right\},\delta,q_{0},F}\right) be a $d$-sequential automaton. Let \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\delta}\right):\mathopen{}\mathclose{{}\left(Q\otimes\mathopen{}\mathclose{{}\left(\Sigma_{b,d}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}}\right)}\right)\to Q such that \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\delta}\right)\mathopen{}\mathclose{{}\left(q,\star}\right)=\delta(q,\star) and such that, \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\delta}\right)\mathopen{}\mathclose{{}\left(q,\boldsymbol{a}}\right)=\delta(q,a_{0}\dots a_{d-1}) for each $\boldsymbol{a}\in\Sigma_{b,d}$. Then let \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathcal{A}}\right)=\mathopen{}\mathclose{{}\left(Q,\Sigma_{b,d}\cup\mathopen{}\mathclose{{}\left\{\star}\right\},\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\delta}\right),q_{0},F}\right).

This operation is called the parallelization of $\mathcal{A}$. The parallelization of the automaton pictured in 3(b) is pictured in Figure 4.

We now state two lemmas whose proofs are simple applications of the definitions. Those lemmas show that this notion of parallelization is coherent with the parallelization of words.

Lemma \thelemma.

Let $w\in\Sigma_{b}^{d\mathbb{N}{}}\star\Sigma_{b}^{\omega}$ and $\mathcal{A}$ a $d$-sequential automaton. The automaton $\mathcal{A}$ accepts $w$ if and only if \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathcal{A}}\right) accepts \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(w}\right).

Lemma \thelemma.

Let $\boldsymbol{w}\in\Sigma_{b,d}^{*}\star\Sigma_{b,d}^{\omega}$ and $\mathcal{A}$ a $d$-sequential automaton. The automaton \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathcal{A}}\right) accepts $\boldsymbol{w}$ if and only if $\mathcal{A}$ accepts \operatorname{seq}_{d}\mathopen{}\mathclose{{}\left(w}\right).

Finally, we state that changing the initial state commute with parallelization.

Lemma \thelemma.

Let $\mathcal{A}$ be a $d$-sequential automaton and $q$ a state of $\mathcal{A}$. The automaton \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathcal{A}}\right)_{q} is equal to the automaton \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathcal{A}_{q}}\right).

6.2 Algorithm

We now consider the problem of deciding whether a Büchi automaton is $d$-parallel or $d$-sequential. We now state the two main results of this section.

Theorem 6.1**.**

Let $\mathcal{A}$ be an automaton over alphabet \Sigma_{b,d}\cup\mathopen{}\mathclose{{}\left\{\star}\right\} with $n$ states. It is decidable in time O\mathopen{}\mathclose{{}\left(nb^{d}}\right) and space O\mathopen{}\mathclose{{}\left(n}\right) whether $\mathcal{A}$ is a $d$-parallel automaton.

Theorem 6.2**.**

Let $\mathcal{A}$ be an automaton over alphabet \Sigma_{b}\cup\mathopen{}\mathclose{{}\left\{\star}\right\} with $n$ states. It is decidable in time O\mathopen{}\mathclose{{}\left(nbd}\right) and space O\mathopen{}\mathclose{{}\left(nd}\right) whether $\mathcal{A}$ is a $d$-sequential automaton.

We prove both theorems simultaneously. More precisely, we prove the following proposition:

Proposition \theproposition.

Let $d_{\text{par}},d_{\text{seq}}>0$. Let $\mathcal{A}$ be an automaton over alphabet \Sigma_{b,d_{\text{par}}}\cup\mathopen{}\mathclose{{}\left\{\star}\right\} with $n$ states. It is decidable in time O\mathopen{}\mathclose{{}\left(nb^{d_{\text{par}}}d_{\text{seq}}}\right) and space O\mathopen{}\mathclose{{}\left(nd_{\text{seq}}}\right) whether $\mathcal{A}$ recognize a subset of $\Sigma_{b,d_{\text{par}}}^{d_{\text{seq}}\mathbb{N}{}}\star\Sigma_{b,d_{\text{par}}}^{d-1}$.

When $d_{\text{par}}=d$ and $d_{\text{seq}}=1$, this proposition implies Theorem 6.1, and when $d_{\text{par}}=1$ and $d_{\text{seq}}=d$, this proposition implies Theorem 6.2. In order to prove this proposition, we introduce the following sets of states.

Definition \thedefinition.

[$Q_{\emptyset}$, $Q_{F}$ and $Q_{i}$] Let $\mathcal{A}$ be an automaton over alphabet \Sigma_{b,d_{\text{par}}}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}.

• •

Let $Q_{\emptyset}$ be the set of states $q$ such that $\mathcal{A}_{q}$ recognizes the empty language.

• •

For $i\in[d_{\text{seq}}-1]$, let $Q_{i}$ be the set of states $\delta(q,\boldsymbol{w})$ with $\boldsymbol{w}\in\Sigma_{b,d_{\text{par}}}^{d_{\text{seq}}\mathbb{N}{}+i}$.

• •

Let $Q_{F}$ be the set of states $\delta(q,\boldsymbol{w})$ with $\boldsymbol{w}\in\Sigma_{b,d_{\text{par}}}^{*}\star\Sigma_{b,d_{\text{par}}}^{*}$

Intuitively, while the automaton reads the natural part of a vector, it visits successively a state of $Q_{0}$, a state of $Q_{1}$, …, a state of $Q_{d}-1$, and then, again a state of $Q_{0}$ and so on. Similarly, while the automaton read the fractional part of the word, it visits states of $Q_{F}$. We could prove that, if $\mathcal{A}$ accepts a subset of $\Sigma_{b,d_{\text{par}}}^{d_{\text{seq}}\mathbb{N}{}}\star\Sigma_{b,d_{\text{par}}}^{\omega}$, then the intersection of two of those sets is included in $Q_{\emptyset}$. We now give example of those set of states.

Example \theexample.

Let $\mathcal{A}$ be the automaton pictured in 3(a), $d_{\text{par}}=d$ and $d_{\text{seq}}=1$. Then Q_{\emptyset}=\mathopen{}\mathclose{{}\left\{q_{\emptyset,\mathcal{A}}}\right\}, Q_{0}=\mathopen{}\mathclose{{}\left\{q_{0}}\right\} and Q_{F}=\mathopen{}\mathclose{{}\left\{q_{[0,1],\mathcal{A}}}\right\}.

Let $\mathcal{A}$ be the automaton pictured in 3(b), $d_{\text{par}}=1$ and $d_{\text{seq}}=2$. Then Q_{\emptyset}=\mathopen{}\mathclose{{}\left\{q_{\emptyset,\mathcal{A}}}\right\}, Q_{i}=\mathopen{}\mathclose{{}\left\{q_{i}}\right\} and Q_{F}=\mathopen{}\mathclose{{}\left\{q_{[0,1],\mathcal{A}},q_{\emptyset,\mathcal{A}}}\right\}.

We now characterize the automata accepting a subset of $\Sigma_{b,d_{\text{par}}}^{d_{\text{seq}}\mathbb{N}{}}\star\Sigma_{b,d_{\text{par}}}^{\omega}$ using sets introduced in Section 6.2. We then characterize those sets of states. All characterizations of those objects are straightforward from their definitions.

Proposition \theproposition.

Let $\mathcal{A}$ be an automaton over alphabet \Sigma_{b,d_{\text{par}}}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}. It accepts a subset of $\Sigma_{b,d_{\text{par}}}^{d_{\text{seq}}\mathbb{N}{}}\star\Sigma_{b,d_{\text{par}}}^{d-1}$ if and only if, $\delta(q,\star)\in Q_{\emptyset}$ for each state $q\in Q_{F}\cup\bigcup_{i=1}^{d-1}Q_{i}$.

Lemma \thelemma.

The set $Q_{\emptyset}$ is the greatest set of states included in $Q$, which does not contain the accepting recurrent states and which is closed under taking predecessor.

Lemma \thelemma.

The sets $Q_{0},\dots,Q_{d_{\text{seq}}-1}$ is the smallest family of sets such that $q_{0}\in Q_{0}$ and for each $i\in[d_{\text{seq}}-1]$, for each $q\in Q_{i}$ and for each $\boldsymbol{a}\in\Sigma_{b,d_{\text{par}}}$, the state $\delta(q,\boldsymbol{a})$ belongs to $Q_{i+1}$.

Lemma \thelemma.

The set $Q_{F}$ is the smallest set containing all sets of the form $\delta(q,\star)$ for $q\in\bigcup_{i=0}^{d-1}Q_{i}$ and $\delta(q,\boldsymbol{a})$ for $q\in Q_{F}$ and $\boldsymbol{a}\in\Sigma_{b,d_{\text{par}}}$.

It is now explained how to compute efficiently those sets.

Lemma \thelemma.

All sets of Section 6.2 are computable in time O\mathopen{}\mathclose{{}\left(nb^{d_{\text{par}}}d_{\text{seq}}}\right) and space O\mathopen{}\mathclose{{}\left(nd_{\text{seq}}}\right).

Proof.

Let us first consider the set $Q_{\emptyset}$. The algorithms is a straightforward application of the characterization given in Lemma 6.2. Tarjan’s algorithm [Tar72] can be used to compute the set of strongly connected component in time O\mathopen{}\mathclose{{}\left(nb^{d_{\text{par}}}}\right), and therefore the set of recurrent states. Furthermore, it is easy to associate in linear time to each state its set of predecessors. Let $p_{q}$ be the number of predecessors of a state $q$.

Two sets PotentiallyEmpty and ToProcess are used by the algorithm. The algorithm initializes the set PotentiallyEmpty to $Q$ and initializes the set ToProcess to the empty set. The algorithm runs on each recurrent state $q$. For each state $q$, if $q$ is accepting, then $q$ is removed from PotentiallyEmpty and added to ToProcess. The algorithm then runs on each element $q$ of ToProcess. For each state $q$, the algorithm removes $q$ from ToProcess and runs on each predecessors $q^{\prime}$ of $q$. For each $q^{\prime}$, if $q^{\prime}$ is in PotentiallyEmpty, then $q^{\prime}$ is removed from PotentiallyEmpty and added to ToProcess. Finally, when ToProcess is empty, the algorithm halts and $Q_{\emptyset}$ is the value of PotentiallyEmpty.

Let us now consider the complexity of this algorithm. At most $n$ states are added to ToProcess, and each state is added at most once. For each state $q$ added to ToProcess, each of its $p_{q}$ predecessor is considered in constant time. Thus the algorithm runs in time O\mathopen{}\mathclose{{}\left(n+\sum_{q\in Q}p_{q}}\right)=O\mathopen{}\mathclose{{}\left(nb^{d_{\text{par}}}}\right).

The $d_{\text{seq}}$-sets $Q_{i}$ are computed simultaneously, using the characterization given in Section 6.2. The computation of the state $Q_{F}$ is similar. The $d$ sets $Q_{i}$ are initialized to the empty set, and ToProcess is initialized to \mathopen{}\mathclose{{}\left\{(q_{0},0)}\right\}. The algorithm runs on each $(q,i)\in\texttt{ToProcess}$. For each $(q,i)$, the pair $(q,i)$ is removed from ToProcess and added into $Q_{i}$. The algorithm runs on each $\boldsymbol{a}\in\Sigma_{b,d_{\text{par}}}$. For each $\boldsymbol{a}$, if \delta(q,\boldsymbol{a})\not\in Q_{\mathopen{}\mathclose{{}\left(i+1\mod d_{\text{seq}}}\right)}, then $\delta(q,\boldsymbol{a})$ is added into ToProcess. When ToProcess is empty, all states of $Q_{i}$ are indeed added to this set.

Let us consider the complexity. Each pair $(q,i)$ is removed at most once from ToProcess, thus the outer loop is executed at moste O\mathopen{}\mathclose{{}\left(nd_{\text{seq}}}\right) times. Each execution of this loop clearly runs in time O\mathopen{}\mathclose{{}\left(b^{d_{\text{par}}}}\right). This algorithm stores a number, a state, and $d_{\text{seq}}$ set of states, thus it clearly takes space O\mathopen{}\mathclose{{}\left(nd_{\text{seq}}}\right).

∎ We now prove Section 6.2.

Proof.

The algorithm computes the sets of Section 6.2. The algorithm runs on each $q\in Q_{F}\cup\bigcup_{i=1}^{d-1}Q_{i}$ and rejects if $\delta(q,\star)\not\in Q_{\emptyset}$. By Section 6.2, this algorithm accepts if an only if $\mathcal{A}$ accepts a subset of $\Sigma_{b,d_{\text{par}}}^{d_{\text{seq}}\mathbb{N}{}}\star\Sigma_{b,d_{\text{par}}}^{d-1}$. By Section 6.2, those sets can be computed in time O\mathopen{}\mathclose{{}\left(nb^{d_{\text{par}}}d_{\text{seq}}}\right) and space O\mathopen{}\mathclose{{}\left(nd_{\text{seq}}}\right), and the loops clearly runs in time O\mathopen{}\mathclose{{}\left(n}\right) and constant space. Thus, the whole algorithm runs in time O\mathopen{}\mathclose{{}\left(nb^{d_{\text{par}}}d_{\text{seq}}}\right) and space O\mathopen{}\mathclose{{}\left(nd_{\text{seq}}}\right). ∎

7 Fixing a component

In order to consider the two encodings of rational numbers, we must consider the vector of words \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle such that a suffix of some component $w_{f}$ belongs to $0^{\omega}$ or $(b-1)^{\omega}$. More precisely, at some points of the run, the automaton will only have to $0^{\omega}$ or $(b-1)^{\omega}$ in some component $f$. Since a component is fixed, we may change the alphabet to fix this letter. We do it by replacing this $f$-th component by an atomic symbol $\square$.

We define a function which remove some component of a word in Section 7.1. We introduce the automata which reads those new words in Section 7.2.

7.1 Vector of words

We now introduced a new alphabet. Letters of this alphabet correspond to letters of $\Sigma_{b,d}$ with some component fixed. We could have considered $\Sigma_{b,d-1}$, but this would lead to trouble when $d=1$. Indeed, a word would then be an element of $()^{*}\star()^{\omega}$, where $()$ is the unique 0 tuple, and it would not be clear what the sequentialization of such a word would be. Instead of removing a component, we choose to replace it with an atomic symbol $\square$. The formal definition is now given.

Definition \thedefinition ($\Sigma_{b,d}^{\square\MVAt{}f}$).

For $f\in[d-1]$, let \Sigma_{b,d}^{\square\MVAt{}f}=\mathopen{}\mathclose{{}\left(\Sigma_{b,f-1}\otimes\mathopen{}\mathclose{{}\left\{\square}\right\}\otimes\Sigma_{d,b-f}}\right).

We now introduce a notation to change a word by fixing one of its component.

Definition \thedefinition (\operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right)).

We first consider $d$-parallel words. Let $f\in[d-1]$, z\in\Sigma_{b}\cup\mathopen{}\mathclose{{}\left\{\square}\right\}, $\boldsymbol{w}$ a word whose alphabet is a set of $d$-tuples. Let $S\subseteq\mathbb{N}$. Let \operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right) be \mathopen{}\mathclose{{}\left\langle\boldsymbol{w}^{\prime},S}\right\rangle, where \mathopen{}\mathclose{{}\left|{\boldsymbol{w}^{\prime}}}\right|=\mathopen{}\mathclose{{}\left|{\boldsymbol{w}}}\right|, $w^{\prime}_{f}\in z^{\infty}$, and $w^{\prime}_{i}=w_{i}$ for each $i\neq f$.

We now consider $d$-sequential words. Let \mathopen{}\mathclose{{}\left\langle w,S}\right\rangle\in\mathopen{}\mathclose{{}\left(\Sigma_{b}\cup\mathopen{}\mathclose{{}\left\{\star,\square}\right\}}\right)^{\infty}, then \operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle w,S}\right\rangle}\right) is \mathopen{}\mathclose{{}\left\langle\operatorname{seq}_{d}\mathopen{}\mathclose{{}\left(\operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(w}\right)}\right)}\right),S}\right\rangle. Equivalently, this transformation consists in replacing each letter whose position is equivalent to $f$ modulo $d$ - not counting the $\star$’s - by the letter $z$.

The following three lemmas about $\operatorname{fix}^{z@f}$ are straightforward consequences from its definition.

Lemma \thelemma.

Let $0\leq i<f<d$ integers, z\in\Sigma_{b}\cup\mathopen{}\mathclose{{}\left\{\square}\right\}, v\in\mathopen{}\mathclose{{}\left(\Sigma_{b}\cup\mathopen{}\mathclose{{}\left\{\square}\right\}}\right)^{i} and w\in\mathopen{}\mathclose{{}\left(\Sigma_{b}\cup\mathopen{}\mathclose{{}\left\{\star,\square}\right\}}\right)^{\infty}, then \operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(vw}\right)=v\operatorname{fix}^{z\MVAt{}f-i}\mathopen{}\mathclose{{}\left(w}\right).

Note that the letter $\star$ does not belongs to $v$. We now state that, if $w_{f}\in z^{\infty}$, then changing twice position $f$ is equivalent to doing only the last change.

Lemma \thelemma.

Let $f\in[d-1]$, z,z^{\prime}\in\Sigma_{b}\cup\mathopen{}\mathclose{{}\left\{\square}\right\}, let $w$ a $d$-parallel or a $d$-sequential word. We have \operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\operatorname{fix}^{z^{\prime}\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right)}\right)=\operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right).

We now state that, if $w_{f}\in z^{\infty}$, then $\boldsymbol{w}$ is a fixpoint of the function.

Lemma \thelemma.

*Let $f\in[d-1]$. Let z\in\Sigma_{b}\cup\mathopen{}\mathclose{{}\left\{\square}\right\}. Let $\boldsymbol{w}$ be a $d$-parallel word. If $w_{f}\in z^{\infty}$ then \operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right)=\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle. *

7.2 Automata

A notation is now introduced, in order to fix the digit read in some position of an automaton. In this section, we fix $f\in[d-1]$, $z\in\Sigma_{b}$.

Definition \thedefinition ($\mathcal{A}^{z\MVAt{}f}$).

Let \mathcal{A}=\mathopen{}\mathclose{{}\left(Q,\Sigma_{b,d}\cup\mathopen{}\mathclose{{}\left\{\star}\right\},\delta,q_{0},F}\right) be a $d$-parallel Büchi automaton, then let:

[TABLE]

where \delta^{z\MVAt{}f}(q,\boldsymbol{a})=\delta(q,\operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\boldsymbol{a}}\right)) for all \boldsymbol{a}\in\Sigma_{b,d}^{\square\MVAt{}f}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}.

Definition \thedefinition ($\mathcal{A}^{z}$).

Let \mathcal{A}=\mathopen{}\mathclose{{}\left(Q,\Sigma_{b}\cup\mathopen{}\mathclose{{}\left\{\star}\right\},\delta,q_{0},F}\right) be a $d$-sequential Büchi automaton. Let:

[TABLE]

where Q^{\prime}=\mathopen{}\mathclose{{}\left(Q\otimes[d-1]}\right)\cup\mathopen{}\mathclose{{}\left\{q_{\emptyset,\mathcal{A}}}\right\} and where, for each state $q\in Q$, $\delta^{z}((q,i),\star)=(\delta(q,\star),i)$, \delta^{z}((q,i),a)=\mathopen{}\mathclose{{}\left(\delta(q,a),i+1}\right) for each $a\in\Sigma_{b}$ and i\in\mathopen{}\mathclose{{}\left\{0,\dots,d-2}\right\}, \delta^{z}((q,d-1),\square)=\mathopen{}\mathclose{{}\left(\delta(q,z),0}\right). For each state $q\in Q^{\prime}$ and each letter a\in\Sigma_{b}\cup\mathopen{}\mathclose{{}\left\{\star,\square}\right\} such that $\delta^{z}(q,a)$ is not yet defined, it is set to $q_{\emptyset,\mathcal{A}}$.

It is now stated that the two transformations introduced above preserve weakness.

Lemma \thelemma.

Let $\mathcal{A}$ be a weak $d$-parallel automaton, then the automaton $\mathcal{A}^{z\MVAt{}f}$ is weak. Let $\mathcal{A}$ be a weak $d$-sequential automaton, then the automaton $\mathcal{A}^{z}$ is weak.

Proof.

For the case of $d$-parallel automata, it suffices to remark that each strongly connected component of $\mathcal{A}^{z\MVAt{}f}$ is a subset of a strongly connected component of $\mathcal{A}$. For the case of $d$-sequential automata, it suffices to remark that a strongly connected component of $\mathcal{A}^{z}$ is either \mathopen{}\mathclose{{}\left\{q_{\emptyset,\mathcal{A}}}\right\}, or a set $S$ such that \mathopen{}\mathclose{{}\left\{q\mid(q,i)\in S}\right\} is a strongly connected component of $\mathcal{A}$. ∎

We also state that changing the initial state of a $d$-parallel automaton commute with the transformation introduced above.

Lemma \thelemma.

Let $\mathcal{A}$ be a $d$-parallel automaton and $q$ a state of $\mathcal{A}$. Then \mathopen{}\mathclose{{}\left(\mathcal{A}^{z\MVAt{}f}}\right)_{q}=\mathopen{}\mathclose{{}\left(\mathcal{A}_{q}}\right)^{z\MVAt{}f}.

Lemma \thelemma.

Let $\mathcal{A}$ be a $d$-sequential automaton and $q$ a state of $\mathcal{A}$. Then \mathopen{}\mathclose{{}\left(\mathcal{A}^{z}}\right)_{(q,0)}=\mathopen{}\mathclose{{}\left(\mathcal{A}_{q}}\right)^{z}.

Words and automata

We show, in this section, how the notations introduced in the two preceding sections interact. The first two lemmas deal with replacing a component with a $\square$.

Lemma \thelemma.

Let $\mathcal{A}$ be a $d$-parallel automaton. Let \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle\in\mathopen{}\mathclose{{}\left(\Sigma_{b,d}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}}\right)^{\omega} such that $w_{f}=z^{\omega}$. The automaton $\mathcal{A}$ accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle if and only if $\mathcal{A}^{z\MVAt{}f}$ accepts \operatorname{fix}^{\square\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right).

Lemma \thelemma.

Let $\mathcal{A}$ be a $d$-sequential automaton. Let \mathopen{}\mathclose{{}\left\langle w,S}\right\rangle\in\Sigma_{b}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}^{\omega} such that \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(w}\right)_{d-1}=z^{\omega}. The automaton $\mathcal{A}$ accepts \mathopen{}\mathclose{{}\left\langle w,S}\right\rangle if and only if $\mathcal{A}^{z}$ accepts \operatorname{fix}^{\square\MVAt{}d-1}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle w,S}\right\rangle}\right).

The following lemma deals with replacing a component of a vector by a single letter.

Lemma \thelemma.

Let $\mathcal{A}$ be a $d$-parallel automaton. Let \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle\in\mathopen{}\mathclose{{}\left(\Sigma_{b,d}^{\square\MVAt{}f}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}}\right)^{\omega}. The automaton $\mathcal{A}^{z\MVAt{}f}$ accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle if and only if $\mathcal{A}$ accepts \operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right).

The following lemma illustrates how the notation introduced above behaves on a word with a component whose suffix is $z^{\omega}$.

Lemma \thelemma.

Let \mathcal{A}=\mathopen{}\mathclose{{}\left(Q,\Sigma_{b}\cup\mathopen{}\mathclose{{}\left\{\star}\right\},\delta,q_{0},F}\right), $q\in Q$, \mathopen{}\mathclose{{}\left\langle\boldsymbol{v},V}\right\rangle\in\mathopen{}\mathclose{{}\left(\Sigma_{b,d}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}}\right)^{*} and \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},W}\right\rangle\in\mathopen{}\mathclose{{}\left(\Sigma_{b,d}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}}\right)^{\omega} with $w_{f}=z^{\omega}$. Then $\mathcal{A}$ accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{v},V}\right\rangle\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},W}\right\rangle if and only if \mathopen{}\mathclose{{}\left(\mathcal{A}^{z\MVAt{}f}}\right)_{\delta(q,\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},V}\right\rangle)} accepts \operatorname{fix}^{\square\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},W}\right\rangle}\right).

Note that, in the last term, the function $\delta$ is still the transition function of $\mathcal{A}$ and not the one of $\mathcal{A}^{z\MVAt{}f}$.

Proof.

The fact “$\mathcal{A}$ accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{v},V}\right\rangle\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},W}\right\rangle” is equivalent to “\mathcal{A}_{\delta(q_{0},\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},V}\right\rangle)} accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},W}\right\rangle”. By Section 7.2, since $w_{f}=z^{\omega}$, those statements are equivalent to “\mathopen{}\mathclose{{}\left(\mathcal{A}_{\delta(q_{0},\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},V}\right\rangle)}}\right)^{z\MVAt{}f} accepts \operatorname{fix}^{\square\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},W}\right\rangle}\right)”. By Section 7.2, they are also equivalent to: “\mathopen{}\mathclose{{}\left(\mathcal{A}^{z\MVAt{}f}}\right)_{\delta(q,\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},V}\right\rangle)} accepts \operatorname{fix}^{\square\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},W}\right\rangle}\right)”. ∎

8 Characterizations of $d$-parallel

RVA

Recall from the introduction that a RVA is a Büchi automaton accepting a saturated language. In this section, we give some characterizations of the $d$-parallel RVAs. The last of those characterization allows us to give in Section 10 an algorithm which decides whether an automaton over alphabet \Sigma_{b,d}\cup\mathopen{}\mathclose{{}\left\{\star}\right\} is a RVA. We use the other characterizations to prove the last one. We first prove a property of minimal RVA.

Lemma \thelemma.

Let \mathcal{A}=\mathopen{}\mathclose{{}\left(Q,A,\delta,q_{0},F}\right) a minimal $d$-parallel RVA, then $\delta(q_{0},\boldsymbol{0})=q_{0}$.

Proof.

Since $\mathcal{A}$ is minimal, it suffices to prove L_{\omega}\mathopen{}\mathclose{{}\left({\mathcal{A}_{\delta(q_{0},\boldsymbol{0})}}}\right)=L_{\omega}\mathopen{}\mathclose{{}\left({\mathcal{A}}}\right), hence it suffices to prove that $\mathcal{A}$ accepts $\boldsymbol{w}$ if and only if $\mathcal{A}_{\delta(q_{0},\boldsymbol{0})}$ for all \boldsymbol{w}\in\mathopen{}\mathclose{{}\left(\Sigma_{b,d}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}}\right)^{\omega}.

Let \boldsymbol{w}\in\mathopen{}\mathclose{{}\left(\Sigma_{b,d}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}}\right)^{\omega}. The automaton $\mathcal{A}_{\delta(q,\boldsymbol{0})}$ accepts $\boldsymbol{w}$ if and only if $\mathcal{A}$ accepts $\boldsymbol{0}\boldsymbol{w}$. Since $\mathcal{A}$ is saturated and \mathopen{}\mathclose{{}\left[{\boldsymbol{0}\boldsymbol{w}}}\right]_{b}^{\mathbb{R}}=\mathopen{}\mathclose{{}\left[{\boldsymbol{w}}}\right]_{b}^{\mathbb{R}}, $\mathcal{A}$ accepts $\boldsymbol{0}\boldsymbol{w}$ if and only if it accepts $\boldsymbol{w}$. By transitivity of equivalence, $\mathcal{A}$ accepts $\boldsymbol{w}$ if and only if $\mathcal{A}_{\delta(q_{0},\boldsymbol{0})}$ accepts $\boldsymbol{w}$. ∎

We now state the characterizations.

Proposition \theproposition.

Let $\mathcal{A}$ be a minimal weak $d$-parallel Büchi automaton such that $\delta(q_{0},\boldsymbol{0})=q_{0}$. The following statement are equivalent:

The automaton $\mathcal{A}$ is a RVA. 2. 2.

For all \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle\mathopen{}\mathclose{{}\left\langle\boldsymbol{w}^{\prime},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle\in\Sigma_{b,d}^{*}\star\Sigma_{b,d}^{\omega} such that \mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle}}\right]_{b}^{\mathbb{R}}=\mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle\boldsymbol{w^{\prime}},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle}}\right]_{b}^{\mathbb{R}} and such that $\mathcal{A}$ accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle, $\mathcal{A}$ accepts (\boldsymbol{w}^{\prime},\mathopen{}\mathclose{{}\left\{s}\right\}). 3. 3.

for all \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle\mathopen{}\mathclose{{}\left\langle\boldsymbol{w}^{\prime},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle\in\Sigma_{b,d}^{*}\star\Sigma_{b,d}^{\omega} such that \mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle}}\right]_{b}^{\mathbb{R}}=\mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle\boldsymbol{w^{\prime}},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle}}\right]_{b}^{\mathbb{R}}, such that |\mathopen{}\mathclose{{}\left\{j\mid w_{j}\neq{}{w^{\prime}}_{j}}\right\}|=1, and such that $\mathcal{A}$ accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle, $\mathcal{A}$ accepts (\boldsymbol{w}^{\prime},\mathopen{}\mathclose{{}\left\{s}\right\}). 4. 4.

for each $f\in[d-1]$, for each $q\in Q$, accessible in $\mathcal{A}$ from $q_{0}$, for each $\boldsymbol{a}\in\Sigma_{b,d}$ with $a_{f}<b-1$,

[TABLE]

where $\boldsymbol{a}^{\prime}=a_{0}\dots a_{f-1}(a_{f}+1)a_{f+1}\dots a_{d-1}$.

Note that Property (1) requires to consider $d$-tuple of words, with $\star$’s in potentially different positions, while in Property (2), both words have a single $\star$’s at the same position. Property (2) requires to consider any pair of word whose natural part have the same length, while Property (3) restrict our study to the case where all but one components of the word are equal.

Proof.

The proof is done by the following sequence of implications. Property (1) implies Property (4), which implies Property (3), which implies Property (2), which implies Property (1).

Property (1) implies Property

(4)

Let $f,q,\boldsymbol{a},\boldsymbol{a}^{\prime}$ as in the hypothesis. Let us prove that L_{\omega}\mathopen{}\mathclose{{}\left({\mathopen{}\mathclose{{}\left(\mathcal{A}^{(b-1)\MVAt{}f}}\right)_{\delta(q,\boldsymbol{a})}}}\right)\subseteq L_{\omega}\mathopen{}\mathclose{{}\left({\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left(\mathcal{A}}\right)^{0\MVAt{}f}}\right)_{\delta(q,\boldsymbol{a^{\prime}})}}}\right), the proof of the reverse inclusion is similar. Let \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},T}\right\rangle\in\mathopen{}\mathclose{{}\left(\Sigma_{b,d}^{\square\MVAt{}f}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}}\right)^{\omega} accepted by \mathopen{}\mathclose{{}\left(\mathcal{A}^{(b-1)\MVAt{}f}}\right)_{\delta(q,\boldsymbol{a})}, let us prove that it is accepted by \mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left(\mathcal{A}}\right)^{0\MVAt{}f}}\right)_{\delta(q,\boldsymbol{a^{\prime}})}.

Since \mathopen{}\mathclose{{}\left(\mathcal{A}^{(b-1)\MVAt{}f}}\right)_{\delta(q,\boldsymbol{a})} accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},T}\right\rangle, by Lemma 7.2, $\mathcal{A}_{\delta(q,\boldsymbol{a})}$ accepts \operatorname{fix}^{b-1\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},T}\right\rangle}\right). Since $q$ is accessible from $q_{0}$, there exists \mathopen{}\mathclose{{}\left\langle\boldsymbol{v},S}\right\rangle\in\mathopen{}\mathclose{{}\left(\Sigma_{b,d}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}}\right)^{*} such that \delta(q_{0},\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},S}\right\rangle)=q. Since $\mathcal{A}_{\delta(q,\boldsymbol{a})}$ accepts \operatorname{fix}^{b-1\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},T}\right\rangle}\right) and \delta(q_{0},\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},S}\right\rangle)=q, it follows that $\mathcal{A}$ accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{v},S}\right\rangle\boldsymbol{a}\operatorname{fix}^{b-1\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},T}\right\rangle}\right). Let us prove that \mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},S}\right\rangle\boldsymbol{a}\operatorname{fix}^{b-1\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},T}\right\rangle}\right)}}\right]_{b}^{\mathbb{R}}=\mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},S}\right\rangle\boldsymbol{a}^{\prime}\operatorname{fix}^{0\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},T}\right\rangle}\right)}}\right]_{b}^{\mathbb{R}}. That is, for $j\in[d-1]$, we want to prove that \mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},S}\right\rangle\boldsymbol{a}\operatorname{fix}^{b-1\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},T}\right\rangle}\right)}\right)_{i}}}\right]_{b}^{\mathbb{R}}=\mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},S}\right\rangle\boldsymbol{a}^{\prime}\operatorname{fix}^{0\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},T}\right\rangle}\right)}\right)_{i}}}\right]_{b}^{\mathbb{R}}. For $i\in[d-1]\setminus f$, it suffices to remark that:

[TABLE]

It remains to consider the case $i=f$. Remark that

[TABLE]

and

[TABLE]

By Theorem 3.1, both of those words encode the same number.

Since $\mathcal{A}$ accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{v},S}\right\rangle\boldsymbol{a}\operatorname{fix}^{b-1\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},T}\right\rangle}\right), \mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},S}\right\rangle\boldsymbol{a}\operatorname{fix}^{b-1\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},T}\right\rangle}\right)}}\right]_{b}^{\mathbb{R}}=\mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},S}\right\rangle\boldsymbol{a}^{\prime}\operatorname{fix}^{0\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},T}\right\rangle}\right)}}\right]_{b}^{\mathbb{R}} and $\mathcal{A}$ is saturated, $\mathcal{A}$ accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{v},S}\right\rangle\boldsymbol{a}^{\prime}\operatorname{fix}^{0\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},T}\right\rangle}\right). It follows that $\mathcal{A}_{\delta(q,\boldsymbol{a}^{\prime})}$ accepts \operatorname{fix}^{0\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},T}\right\rangle}\right). Finally, since $\mathcal{A}_{\delta(q,\boldsymbol{a}^{\prime})}$ accepts \operatorname{fix}^{0\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},T}\right\rangle}\right), by Lemma 7.2, \mathopen{}\mathclose{{}\left(\mathcal{A}^{0\MVAt{}f}}\right)_{\delta(q,\boldsymbol{a^{\prime}})} accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},T}\right\rangle.

Property (4) implies Property

(3)

Let \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle and \mathopen{}\mathclose{{}\left\langle\boldsymbol{w}^{\prime},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle be two words as in Property (3). Let us prove that $\mathcal{A}$ accepts $\boldsymbol{w^{\prime}}$. Let $f\in[d-1]$ be the only integer such that $w_{f}\neq w^{\prime}_{f}$. As explained in Theorem 3.1, since \mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle w_{f},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle}}\right]_{b}^{F}=\mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle w^{\prime}_{f},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle}}\right]_{b}^{F}, since ${w}_{f}\neq{w^{\prime}}_{f}$, and since their natural parts have the same length, then \mathopen{}\mathclose{{}\left\{w_{f},w^{\prime}_{f}}\right\}=\mathopen{}\mathclose{{}\left\{u_{f}a_{f}(b-1)^{\omega},u_{f}(a_{f}+1)0^{\omega}}\right\}, for some $u_{f}\in\Sigma_{b}^{*}$ and a_{f}\in\Sigma_{b}\setminus\mathopen{}\mathclose{{}\left\{b-1}\right\}. Let us assume that $w_{f}$ is $u_{f}a_{f}(b-1)^{\omega}$, the case where $w_{f}$ is $u_{f}(a_{f}+1)0^{\omega}$ is similar. Note that $w^{\prime}_{f}=u_{f}(a_{f}+1)0^{\omega}$.

Let $l$ be the length of the prefix of (w_{f},\mathopen{}\mathclose{{}\left\{s}\right\}) before the occurrence of the letter $a_{f}$. It is \mathopen{}\mathclose{{}\left|{u_{f}}}\right| if s>\mathopen{}\mathclose{{}\left|{u_{f}}}\right|, and \mathopen{}\mathclose{{}\left|{u_{f}}}\right|+1 otherwise. Let \mathopen{}\mathclose{{}\left\langle\boldsymbol{u},U}\right\rangle=\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle\mathopen{}\mathclose{{}\left[<l}\right]=\mathopen{}\mathclose{{}\left\langle\boldsymbol{w}^{\prime},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle\mathopen{}\mathclose{{}\left[<l}\right] be this prefix. Let \boldsymbol{a}=\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle[l] and \boldsymbol{a}^{\prime}=(\boldsymbol{w}^{\prime},\mathopen{}\mathclose{{}\left\{s}\right\})[l]. Similarly, let \mathopen{}\mathclose{{}\left\langle\boldsymbol{v},V}\right\rangle=\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle\mathopen{}\mathclose{{}\left[\geq{}l+1}\right] and \mathopen{}\mathclose{{}\left\langle\boldsymbol{v}^{\prime},V}\right\rangle=(\boldsymbol{w}^{\prime},\mathopen{}\mathclose{{}\left\{s}\right\})\mathopen{}\mathclose{{}\left[\geq{}l+1}\right] be the suffixes of $\boldsymbol{w}$ and $\boldsymbol{w}^{\prime}$ after those occurrences of $\boldsymbol{a}$ and of $\boldsymbol{a}^{\prime}$ respectively. Note that the notations $u_{f}$, $a_{f}$ and $a^{\prime}_{f}$ introduced above are consistent with the notations $\boldsymbol{u}$, $\boldsymbol{a}$ and $\boldsymbol{a}^{\prime}$. Note also that ${v}_{f}=(b-1)^{\omega}$, that ${v^{\prime}}_{f}=0^{\omega}$, and that $v_{i}=v^{\prime}_{i}$ for all i\in[d-1]\setminus\mathopen{}\mathclose{{}\left\{f}\right\}. Hence \operatorname{fix}^{\square\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},V}\right\rangle}\right)=\operatorname{fix}^{\square\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{v}^{\prime},V}\right\rangle}\right). The notation $a_{f}$ introduced above is coherent with the notation $\boldsymbol{a}$. Since $a^{\prime}_{f}=a_{f}+1$, $\boldsymbol{a}$ and $\boldsymbol{a}^{\prime}$ satisfy the hypothesis of Property (4). It follows that L_{\omega}\mathopen{}\mathclose{{}\left({\mathopen{}\mathclose{{}\left(\mathcal{A}^{(b-1)\MVAt{}f}}\right)_{\delta(q,\boldsymbol{a})}}}\right)=L_{\omega}\mathopen{}\mathclose{{}\left({\mathopen{}\mathclose{{}\left(\mathcal{A}^{0\MVAt{}f}}\right)_{\delta(q,\boldsymbol{a}^{\prime})}}}\right).

We can now prove that \mathopen{}\mathclose{{}\left\langle\boldsymbol{w}^{\prime},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle is accepted by $\mathcal{A}$. Since \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle=\mathopen{}\mathclose{{}\left\langle\boldsymbol{u},U}\right\rangle\boldsymbol{a}\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},V}\right\rangle is accepted by $\mathcal{A}$ and $v_{f}=(b-1)^{\omega}$, by Section 7.2, \mathopen{}\mathclose{{}\left(\mathcal{A}^{(b-1)\MVAt{}f}}\right)_{\delta(q_{0},\mathopen{}\mathclose{{}\left\langle\boldsymbol{u},U}\right\rangle\boldsymbol{a})} accepts \operatorname{fix}^{\square\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},V}\right\rangle}\right). Since \mathopen{}\mathclose{{}\left(\mathcal{A}^{(b-1)\MVAt{}f}}\right)_{\delta(q_{0},\mathopen{}\mathclose{{}\left\langle\boldsymbol{u},U}\right\rangle\boldsymbol{a})} accepts \operatorname{fix}^{\square\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},V}\right\rangle}\right) and L_{\omega}\mathopen{}\mathclose{{}\left({\mathopen{}\mathclose{{}\left(\mathcal{A}^{(b-1)\MVAt{}f}}\right)_{\delta(q,\boldsymbol{a})}}}\right)=L_{\omega}\mathopen{}\mathclose{{}\left({\mathopen{}\mathclose{{}\left(\mathcal{A}^{0\MVAt{}f}}\right)_{\delta(q,\boldsymbol{a}^{\prime})}}}\right), \mathopen{}\mathclose{{}\left(\mathcal{A}^{0\MVAt{}f}}\right)_{\delta(q_{0},\mathopen{}\mathclose{{}\left\langle\boldsymbol{u},U}\right\rangle\boldsymbol{a}^{\prime})} accepts \operatorname{fix}^{\square\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},V}\right\rangle}\right). Since \operatorname{fix}^{\square\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},V}\right\rangle}\right)=\operatorname{fix}^{\square\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{v}^{\prime},V}\right\rangle}\right) and \mathopen{}\mathclose{{}\left(\mathcal{A}^{0\MVAt{}f}}\right)_{\delta(q_{0},\mathopen{}\mathclose{{}\left\langle\boldsymbol{u},U}\right\rangle\boldsymbol{a}^{\prime})} accepts \operatorname{fix}^{\square\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},V}\right\rangle}\right), \mathopen{}\mathclose{{}\left(\mathcal{A}^{0\MVAt{}f}}\right)_{\delta(q_{0},\mathopen{}\mathclose{{}\left\langle\boldsymbol{u},U}\right\rangle\boldsymbol{a}^{\prime})} accepts \operatorname{fix}^{\square\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{v}^{\prime},V}\right\rangle}\right). It follows from Section 7.2 that $\mathcal{A}$ accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{u},U}\right\rangle\boldsymbol{a}^{\prime}\mathopen{}\mathclose{{}\left\langle\boldsymbol{v},V}\right\rangle=(\boldsymbol{w}^{\prime},\mathopen{}\mathclose{{}\left\{s}\right\}).

Property (3) implies Property

(2)

We must prove that, for all \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle,\mathopen{}\mathclose{{}\left\langle\boldsymbol{w}^{\prime},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle\in\mathopen{}\mathclose{{}\left(\Sigma_{b,d}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}}\right)^{\omega}, if $\mathcal{A}$ accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle and \mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle}}\right]_{b}^{\mathbb{R}}=\mathopen{}\mathclose{{}\left[{(\boldsymbol{w}^{\prime},\mathopen{}\mathclose{{}\left\{s}\right\})}}\right]_{b}^{\mathbb{R}} then $\mathcal{A}$ accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{w}^{\prime},\mathopen{}\mathclose{{}\left\{s^{\prime}}\right\}}\right\rangle. The proof is by induction on i=|\mathopen{}\mathclose{{}\left\{j\mid w_{j}\neq{}w^{\prime}_{j}}\right\}|. The case $i=0$ is trivial, since it means that \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle=\mathopen{}\mathclose{{}\left\langle\boldsymbol{w^{\prime}},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle. Let us now assume that $i>1$ and that the induction hypothesis holds when |\mathopen{}\mathclose{{}\left\{j\mid w_{j}\neq{}w^{\prime}_{j}}\right\}|<i.

Since |\mathopen{}\mathclose{{}\left\{j\mid w_{j}\neq{}w^{\prime}_{j}}\right\}|=i and $i>1$, there exists $f\in[d-1]$ such that $w_{f}\neq w^{\prime}_{f}$. Let \mathopen{}\mathclose{{}\left\langle\boldsymbol{w}^{\prime\prime},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle\in\mathopen{}\mathclose{{}\left(\Sigma_{b,d}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}}\right)^{\omega} such that $w^{\prime\prime}_{f}=w_{f}$ and such that $w_{k}^{\prime\prime}=w^{\prime}_{k}$ for all k\in[b-1]\setminus\mathopen{}\mathclose{{}\left\{f}\right\}. Note that |\mathopen{}\mathclose{{}\left\{j\mid w_{j}\neq{}w^{\prime\prime}_{j}}\right\}|=i-1, |\mathopen{}\mathclose{{}\left\{j\mid w^{\prime}_{j}\neq{}w^{\prime\prime}_{j}}\right\}|=1 and \mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle}}\right]_{b}^{\mathbb{R}}=\mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle\boldsymbol{w^{\prime\prime}},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle}}\right]_{b}^{\mathbb{R}}=\mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle\boldsymbol{w^{\prime}},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle}}\right]_{b}^{\mathbb{R}}.

Since |\mathopen{}\mathclose{{}\left\{j\mid w_{j}\neq{}w^{\prime\prime}_{j}}\right\}|=i-1 and \mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle}}\right]_{b}^{\mathbb{R}}=\mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle\boldsymbol{w^{\prime\prime}},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle}}\right]_{b}^{\mathbb{R}}, by induction hypothesis $\mathcal{A}$ accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{w^{\prime\prime}},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle. Since |\mathopen{}\mathclose{{}\left\{j\mid w^{\prime\prime}_{j}\neq{}w^{\prime}_{j}}\right\}|=1 and \mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle\boldsymbol{w^{\prime\prime}},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle}}\right]_{b}^{\mathbb{R}}=\mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle\boldsymbol{w^{\prime}},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle}}\right]_{b}^{\mathbb{R}} and since $\mathcal{A}$ accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{w^{\prime\prime}},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle, by Property (3), $\mathcal{A}$ accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{w^{\prime}},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle.

Property

(2) implies Property (1)

We must prove that, for all \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle,(\boldsymbol{w}^{\prime},\mathopen{}\mathclose{{}\left\{s^{\prime}}\right\})\in\mathopen{}\mathclose{{}\left(\Sigma_{b,d}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}}\right)^{\omega}, if $\mathcal{A}$ accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle and \mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle}}\right]_{b}^{\mathbb{R}}=\mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle\boldsymbol{w}^{\prime},\mathopen{}\mathclose{{}\left\{s^{\prime}}\right\}}\right\rangle}}\right]_{b}^{\mathbb{R}} then $\mathcal{A}$ accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{w}^{\prime},\mathopen{}\mathclose{{}\left\{s^{\prime}}\right\}}\right\rangle. Let us assume that $s\leq s^{\prime}$, the case $s>s^{\prime}$ is similar. Since $\delta(q_{0},\boldsymbol{0})=q_{0}$ and $\mathcal{A}$ accepts (\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s}\right\}), $\mathcal{A}$ accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{0}^{s^{\prime}-s},\mathopen{}\mathclose{{}\left\{s^{\prime}}\right\}}\right\rangle. Note that \mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle\boldsymbol{0}^{s^{\prime}-s}\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s^{\prime}}\right\}}\right\rangle}}\right]_{b}^{\mathbb{R}}=\mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s}\right\}}\right\rangle}}\right]_{b}^{\mathbb{R}}=\mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle\boldsymbol{w}^{\prime},\mathopen{}\mathclose{{}\left\{s^{\prime}}\right\}}\right\rangle}}\right]_{b}^{\mathbb{R}}. Since \mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle\boldsymbol{0}^{s^{\prime}-s}\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s^{\prime}}\right\}}\right\rangle}}\right]_{b}^{\mathbb{R}}=\mathopen{}\mathclose{{}\left[{\mathopen{}\mathclose{{}\left\langle\boldsymbol{w}^{\prime},\mathopen{}\mathclose{{}\left\{s}\right\}^{\prime}}\right\rangle}}\right]_{b}^{\mathbb{R}} and $\mathcal{A}$ accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{0}^{s^{\prime}-s}\boldsymbol{w},\mathopen{}\mathclose{{}\left\{s^{\prime}}\right\}}\right\rangle, by Property (2), $\mathcal{A}$ accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{w}^{\prime},\mathopen{}\mathclose{{}\left\{s^{\prime}}\right\}}\right\rangle. ∎

9 Characterization of $d$-sequential automata

A characterization of $d$-sequential automata is now given. This characterization is similar to Property 4 of Section 8. Instead of doing the whole proof again for sequential automata, we prove that this characterization is correct by proving that it implies the characterization of Section 8 on the parallelization of the $d$-sequential automata.

Proposition \theproposition.

Let $\mathcal{A}$ be a minimal weak $d$-sequential Büchi automaton. The following statements are equivalent:

The automaton $\mathcal{A}$ is a RVA. 2. 2.

• •

$\delta(q_{0},0^{d})=q_{0}$ and

• •

For each $q\in Q$ accessible in $\mathcal{A}$ from $q_{0}$, for each $a\in\Sigma_{b}\setminus{b-1}$, {\mathopen{}\mathclose{{}\left(\mathcal{A}^{(b-1)}}\right)_{(\delta(q,a),0)}} and {\mathopen{}\mathclose{{}\left(\mathcal{A}^{0}}\right)_{(\delta(q,a+1),0)}} accept the same language.

In order to prove this proposition, we introduce the following lemma. This lemma allows us to reduce Property (2) of Section 9 to Property (4) of Section 8.

Lemma \thelemma.

Let $\mathcal{A}$ be a weak $d$-sequential Büchi automaton, $f\in[d-1]$, $z\in\Sigma_{b}$, $q$ a state of $\mathcal{A}$, $\boldsymbol{a}\in\Sigma_{b,d}$ and \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle\in\mathopen{}\mathclose{{}\left(\Sigma_{b,d}^{\square\MVAt{}f}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}}\right)^{\omega}. The word \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle is accepted by \mathopen{}\mathclose{{}\left(\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathcal{A}}\right)^{z\MVAt{}f}}\right)_{(\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\delta}\right)(q,\boldsymbol{a}),0)} if and only if \mathopen{}\mathclose{{}\left(\mathcal{A}^{z}}\right)_{\delta(q,a_{0}\dots a_{f})} accepts a_{f+1}\dots a_{d-1}\operatorname{seq}_{d}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right).

Proof.

By Section 7.2 “\mathopen{}\mathclose{{}\left(\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathcal{A}}\right)^{z\MVAt{}f}}\right)_{(\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\delta}\right)(q,\boldsymbol{a}),0)} accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle” is equivalent to: “\mathopen{}\mathclose{{}\left(\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathcal{A}}\right)_{\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\delta}\right)(q,\boldsymbol{a})}}\right)^{z\MVAt{}f} accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle”. By Section 7.2, it is equivalent to: “\mathopen{}\mathclose{{}\left(\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathcal{A}}\right)_{\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\delta}\right)(q,\boldsymbol{a})}}\right) accepts \operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right)”, hence to “\mathopen{}\mathclose{{}\left(\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathcal{A}}\right)}\right)_{q} accepts \boldsymbol{a}\operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right)”. By Section 6.1, it is also equivalent to: “\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathcal{A}_{q}}\right) accepts \boldsymbol{a}\operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right)”. By Section 6.1, it is also equivalent to: “$\mathcal{A}_{q}$ accepts \operatorname{seq}_{d}\mathopen{}\mathclose{{}\left(\boldsymbol{a}\operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right)}\right)”. Note that \operatorname{seq}_{d}\mathopen{}\mathclose{{}\left(\boldsymbol{a}\operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right)}\right) equals a_{0}\dots a_{d-1}\operatorname{seq}_{d}\mathopen{}\mathclose{{}\left(\operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right)}\right), thus the above-mentionned properties are equivalent to: “$\mathcal{A}_{q}$ accepts a_{0}\dots a_{d-1}\operatorname{seq}_{d}\mathopen{}\mathclose{{}\left(\operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right)}\right)” and then to: “$\mathcal{A}_{\delta(q,a_{0}\dots,a_{f})}$ accepts a_{f+1}\dots a_{d-1}\operatorname{seq}_{d}\mathopen{}\mathclose{{}\left(\operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right)}\right)”. By Section 7.2, it is equivalent to: “\mathopen{}\mathclose{{}\left(\mathcal{A}_{{}_{\delta(q,a_{0}\dots,a_{f})}}}\right)^{z} accepts \operatorname{fix}^{\square\MVAt{}d-1}\mathopen{}\mathclose{{}\left(a_{f+1}\dots a_{d-1}\operatorname{seq}_{d}\mathopen{}\mathclose{{}\left(\operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right)}\right)}\right)”.

Note that the length of $a_{f+1}\dots a_{d-1}$ is $(d-1)-(f+1)+1=d-f-1$, and that $(d-1)-(d-f-1)=f$, thus by Section 7.1, \operatorname{fix}^{\square\MVAt{}d-1}\mathopen{}\mathclose{{}\left(a_{f+1}\dots a_{d-1}\operatorname{seq}_{d}\mathopen{}\mathclose{{}\left(\operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right)}\right)}\right) equals a_{f+1}\dots a_{d-1}\operatorname{fix}^{\square\MVAt{}f}\mathopen{}\mathclose{{}\left(\operatorname{seq}_{d}\mathopen{}\mathclose{{}\left(\operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right)}\right)}\right). By definition of $\operatorname{fix}_{\square\MVAt f}$ on $d$-sequential number, \operatorname{fix}^{\square\MVAt{}f}\mathopen{}\mathclose{{}\left(\operatorname{seq}_{d}\mathopen{}\mathclose{{}\left(\operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right)}\right)}\right) equals \operatorname{seq}_{d}\mathopen{}\mathclose{{}\left(\operatorname{fix}^{\square\MVAt{}f}\mathopen{}\mathclose{{}\left(\operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right)}\right)}\right). By Section 7.1, \operatorname{fix}^{\square\MVAt{}f}\mathopen{}\mathclose{{}\left(\operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right)}\right) equals \operatorname{fix}^{\square\MVAt{}f}\mathopen{}\mathclose{{}\left({\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}}\right). Since $w_{f}=\square^{\omega}$, by Section 7.1, \operatorname{fix}^{\square\MVAt{}f}\mathopen{}\mathclose{{}\left({\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}}\right)=\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle. It follows that \operatorname{fix}^{\square\MVAt{}d-1}\mathopen{}\mathclose{{}\left(a_{f+1}\dots a_{d-1}\operatorname{seq}_{d}\mathopen{}\mathclose{{}\left(\operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right)}\right)}\right) equals a_{f+1}\dots a_{d-1}\operatorname{seq}_{d}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right). Thus, all the above mentionned facts are equivalent to: “\mathopen{}\mathclose{{}\left(\mathcal{A}_{{}_{\delta(q,a_{0}\dots,a_{f})}}}\right)^{b-1} accepts a_{f+1}\dots a_{d-1}\operatorname{seq}_{d}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right)”. Finally, by Section 7.2, it is equivalent to “\mathopen{}\mathclose{{}\left(\mathcal{A}^{z}}\right)_{\delta(q,a_{0}\dots a_{f})} accepts a_{f+1}\dots a_{d-1}\operatorname{seq}_{d}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right)”. ∎

Section 9 is now proven.

Proof.

Let us show that Property (1) implies Property (2). The proof of the first part of this Property is the same than the proof of Section 8. The proof of the second part of this Property is the same than the proof that Property (1) of Section 8 implies Property (4) of Section 8.

It remains to prove that Property (2) implies Property (1). We want to prove that $\mathcal{A}$ is a RVA. Since $\mathcal{A}$ is $d$-sequential, it remains to prove that L_{\omega}\mathopen{}\mathclose{{}\left({\mathcal{A}}}\right) is saturated. It suffices to prove that \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(L_{\omega}\mathopen{}\mathclose{{}\left({\mathcal{A}}}\right)}\right) is saturated. By Section 6.1, \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathcal{A}}\right) accepts \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(L_{\omega}\mathopen{}\mathclose{{}\left({\mathcal{A}}}\right)}\right). Therefore, we only have to prove that \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathcal{A}}\right) is a RVA. By Section 8, it suffices to prove that \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\delta}\right)(q_{0},\boldsymbol{0})=q_{0} and that, for each $f\in[d-1]$, for each $q\in Q$, accessible in $\mathcal{A}$ from $q_{0}$, for each $\boldsymbol{a}\in\Sigma_{b,d}$ with $a_{f}<b-1$, L_{\omega}\mathopen{}\mathclose{{}\left({\mathopen{}\mathclose{{}\left(\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathcal{A}}\right)^{(b-1)\MVAt{}f}}\right)_{\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\delta}\right)(q,\boldsymbol{a})}}}\right)=L_{\omega}\mathopen{}\mathclose{{}\left({\mathopen{}\mathclose{{}\left(\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathcal{A}}\right)^{0\MVAt{}f}}\right)_{\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\delta}\right)(q,\boldsymbol{a}^{\prime})}}}\right) where $\boldsymbol{a}^{\prime}=a_{0}\dots a_{f-1}(a_{f}+1)a_{f+1}\dots a_{d-1}$.

Note that the first part of Property (2) clearly implies \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\delta}\right)(q_{0},\boldsymbol{0})=q_{0}. Let $q$, $\boldsymbol{a}$, $\boldsymbol{a}^{\prime}$ as above, it remains to prove that L_{\omega}\mathopen{}\mathclose{{}\left({\mathopen{}\mathclose{{}\left(\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathcal{A}}\right)^{(b-1)\MVAt{}f}}\right)_{\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\delta}\right)(q,\boldsymbol{a})}}}\right)\subseteq L_{\omega}\mathopen{}\mathclose{{}\left({\mathopen{}\mathclose{{}\left(\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathcal{A}}\right)^{0\MVAt{}f}}\right)_{\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\delta}\right)(q,\boldsymbol{a^{\prime}})}}}\right), the reverse inclusion is similar. Let \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle\in\Sigma_{b,d}^{\square\MVAt{}f}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}^{\omega} accepted by \mathopen{}\mathclose{{}\left(\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathcal{A}}\right)^{(b-1)\MVAt{}f}}\right)_{\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\delta}\right)(q,\boldsymbol{a})}, we want to prove that it is accepted by \mathopen{}\mathclose{{}\left(\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathcal{A}}\right)}\right)_{\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\delta}\right)(q,\boldsymbol{a}^{\prime})}^{0\MVAt{}f}.

Since \mathopen{}\mathclose{{}\left(\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathcal{A}}\right)^{(b-1)\MVAt{}f}}\right)_{\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\delta}\right)(q,\boldsymbol{a})} accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle\in\mathopen{}\mathclose{{}\left(\Sigma_{b,d}^{\square\MVAt{}f}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}}\right)^{\omega}, by Section 9, \mathopen{}\mathclose{{}\left(\mathcal{A}_{\delta(q,a_{0}\dots a_{f-1}a_{f})}}\right)^{b-1} accepts a_{f+1}\dots a_{d-1}\operatorname{seq}_{d}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right). By the second part of Property (2), it follows that \mathopen{}\mathclose{{}\left(\mathcal{A}_{\delta(q,a_{0}\dots a_{f-1}(a_{f}+1))}}\right)^{0} accepts a_{f+1}\dots a_{d-1}\operatorname{seq}_{d}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right). By Section 9, it follows that \mathopen{}\mathclose{{}\left(\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathcal{A}}\right)^{0\MVAt{}f}}\right)_{\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\delta}\right)(q,\boldsymbol{a^{\prime}})} accepts \mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle. ∎

10 Algorithms

We now show how to decide efficiently whether an automaton is a RVA.

Theorem 10.1**.**

Let \mathcal{A}=\mathopen{}\mathclose{{}\left(Q,\Sigma_{b,d}\cup\mathopen{}\mathclose{{}\left\{\star}\right\},\delta,q_{0},F}\right) an automaton with $n$ states. It is decidable in time O\mathopen{}\mathclose{{}\left(n\log(n)db^{d}}\right) and space O\mathopen{}\mathclose{{}\left(nb^{d}}\right) whether $\mathcal{A}$ is a RVA.

Note that $b^{d}$ is the cardinality of the alphabet. Thus this algorithm is quasi-linear in the size of its input.

Proof.

Without loss of generality, it can be assumed that the automaton is minimal. The algorithm consists in three parts. First, the algorithm checks whether the algorithm of Theorem 6.1 applied on $\mathcal{A}$ returns true. Secondly, the algorithm checks whether $\delta(q_{0},\boldsymbol{0})=q_{0}$. Thirdly, the algorithm runs on each $f\in[d-1]$. For each $f$, the algorithm generates the automata $\mathcal{A}^{0\MVAt{}f}$ and $\mathcal{A}^{(b-1)\MVAt{}f}$ and the data structure mentionned in Section 4.2. The algorithm runs on each $q\in Q$ and $\boldsymbol{a}$, $\boldsymbol{a}^{\prime}$ as in Property (4) of Section 8. The algorithm then applies the algorithm of Section 4.2 to check whether, for all pairs (\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\delta}\right)(q,\boldsymbol{a}),\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\delta}\right)(q,\boldsymbol{a}^{\prime})), \mathopen{}\mathclose{{}\left(\mathcal{A}^{b-1\MVAt{}f}}\right)_{\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\delta}\right)(q,\boldsymbol{a})} and \mathopen{}\mathclose{{}\left(\mathcal{A}^{0\MVAt{}f}}\right)_{\operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\delta}\right)(q,\boldsymbol{a}^{\prime})} accept the same language. If one of those checks fail the algorithm rejects. Otherwise, the algorithm accepts.

By Section 7.2, $\mathcal{A}^{0\MVAt{}f}$ and $\mathcal{A}^{(b-1)\MVAt{}f}$ are weak, thus, Section 4.2 can be used. It follows from Theorem 6.1, Section 8 and Section 8 that this algorithm accepts exactly the $d$-parallel automata which are RVA.

It remains to consider the complexity. By Theorem 6.1, the first part runs in O\mathopen{}\mathclose{{}\left(nb^{d}}\right) and space O\mathopen{}\mathclose{{}\left(n}\right). The second part clearly runs in constant time and space. By Section 4.2, the last part runs in time O\mathopen{}\mathclose{{}\left(n\log(n)b^{d}d}\right) and space O\mathopen{}\mathclose{{}\left(n\log{n}b^{d}}\right). ∎

We now prove a similar theorem for $d$-sequential automata.

Theorem 10.2**.**

Let \mathcal{A}=\mathopen{}\mathclose{{}\left(Q,\Sigma_{b}\cup\mathopen{}\mathclose{{}\left\{\star}\right\},\delta,q_{0},F}\right) an automaton with $n$ states. It is decidable in time O\mathopen{}\mathclose{{}\left(nd\log(nd)b}\right) and space O\mathopen{}\mathclose{{}\left(ndb}\right) whether $\mathcal{A}$ is a RVA.

Proof.

Without loss of generality, it can be assumed that the automaton is minimal. The algorithm and its proof are similar to the ones of Theorem 10.1. The algorithm consists in three parts. Firstly, the algorithm applies the algorithm of Theorem 6.2 to check whether $\mathcal{A}$ is a $d$-sequential automaton. Secondly, it checks whether $\delta(q_{0},0^{d})=q_{0}$. Thirdly, the algorithm generates the automata $\mathcal{A}^{0}$ and $\mathcal{A}^{(b-1)}$ and the data structure mentionned in Section 4.2. The algorithm runs on each $q\in Q$ and $a\in\Sigma_{b}\setminus{b-1}$. For each $q$ and $a$, the algorithm applies the algorithm of Section 4.2 to check whether {\mathopen{}\mathclose{{}\left(\mathcal{A}^{(b-1)}}\right)_{\delta(q,a)}} and {\mathopen{}\mathclose{{}\left(\mathcal{A}^{0}}\right)_{\delta(q,a+1)}} accept the same language.

By Section 7.2, $\mathcal{A}^{0}$ and $\mathcal{A}^{(b-1)}$ are weak, thus, Section 4.2 can be used. It follows from Theorem 6.2 and Section 9 that this algorithm accepts exactly the $d$-sequential automata which are RVAs.

It remains to consider the complexity. By Theorem 6.2, the first part runs in time O\mathopen{}\mathclose{{}\left(ndb}\right) and space O\mathopen{}\mathclose{{}\left(nd}\right). The second part runs in time O\mathopen{}\mathclose{{}\left(d}\right) and constant space. Finally, by Section 4.2, the third part runs in time O\mathopen{}\mathclose{{}\left(nd\log(nd)b}\right) and space O\mathopen{}\mathclose{{}\left(ndb}\right).

∎

A last algorithm is given for the special case of dimension $d=1$.

Theorem 10.3**.**

Let \mathcal{A}=\mathopen{}\mathclose{{}\left(Q,\Sigma_{b},\delta,q_{0},F}\right) a minimal weak Büchi automaton with $n$ states. It is decidable in time O\mathopen{}\mathclose{{}\left(nb}\right) and space O\mathopen{}\mathclose{{}\left(n}\right) whether L_{\omega}\mathopen{}\mathclose{{}\left({\mathcal{A}}}\right) is saturated.

Note that $\mathcal{A}$ is assumed minimal.

Proof.

Note that $\Sigma_{b,1}^{\square\MVAt{}f}$ contains exactly one letter, \mathopen{}\mathclose{{}\left(\square}\right), thus both languages of Equation (4) are either $\emptyset$ or \mathopen{}\mathclose{{}\left(\square}\right)^{\omega}. It follows that Equation (4) holds if and only if $\delta(q,a)\in Q_{\emptyset}^{(b-1)}$ is equivalent to $\delta(q,a+1)\in Q_{\emptyset}^{0}$, where $Q_{\emptyset}^{z}$ is the set of states $q$ such that $\mathcal{A}^{z\MVAt{}0}_{q}$ accepts the empty language.

The algorithm is now given. The algorithm checks whether $\delta(q_{0},0)=q_{0}$. The algorithm computes $\mathcal{A}^{(b-1)\MVAt{}0}$ and $\mathcal{A}^{0\MVAt{}0}$. The algorithm applies the algorithm of Section 6.2 to those two automata in order to compute the sets $Q_{\emptyset}^{(b-1)}$ and $Q_{\emptyset}^{0}$. The algorithm runs on each state $q\in Q$ accessible from $q_{0}$, and on each a\in\Sigma_{b}\setminus\mathopen{}\mathclose{{}\left\{b-1}\right\}. For each $q$ and $a$, the algorithm checks whether $\delta(q,a)\in Q_{\emptyset}^{(b-1)}$ is equivalent to $\delta(q,a+1)\in Q_{\emptyset}^{0}$. Finally, if one of the checks fail, the algorithm rejects, otherwise it accepts.

Let us consider the complexity. The automata $\mathcal{A}^{(b-1)\MVAt{}0}$ and $\mathcal{A}^{0\MVAt{}0}$ clearly takes space O\mathopen{}\mathclose{{}\left(n}\right). Applying the algorithm of Section 6.2 takes time O\mathopen{}\mathclose{{}\left(n}\right) and takes space O\mathopen{}\mathclose{{}\left(n}\right). For a set $q$ and a letter $a$, checking the equivalence is done in constant time and space. Thus, the final loop runs in time O\mathopen{}\mathclose{{}\left(nb}\right) and constant space. Finaly, the whole algorithm runs in time O\mathopen{}\mathclose{{}\left(nb}\right) and space O\mathopen{}\mathclose{{}\left(n}\right). ∎

11 Considering negative reals

In this section, we consider the case of negative numbers. Given $w_{I}\in\Sigma_{b}^{*}$, $aw$ encodes, in $b$-complement representation, the number \mathopen{}\mathclose{{}\left[{w_{I}}}\right]_{b}^{I} if $a=0$, -b^{\mathopen{}\mathclose{{}\left|{w_{I}}}\right|}+\mathopen{}\mathclose{{}\left[{w_{I}}}\right]_{b}^{I} if $a=(b-1)$, and is undefined otherwise. Similarly, given $w_{F}\in\Sigma_{b}^{\omega}$, \mathopen{}\mathclose{{}\left[{aw_{I}\star w_{F}}}\right]_{b}^{\mathbb{R}} encodes, in $b$-complement representation, the number encoded by $aw_{I}$, plus \mathopen{}\mathclose{{}\left[{w_{F}}}\right]_{b}^{F}.

When considering $b$-complement representation, Theorem 3.1 must be changed as follows. For $l$ great enough, a real $q$ has two encoding whose natural part’s length is $l$ if and only if it is of the form $nb^{p}$ with $n,p\in\mathbb{Z}{}$. If $q=0$, those encodings are $(b-1)^{l}\star(b-1)^{\omega}$ and $0^{l}\star 0^{\omega}$, otherwise they are as in Equation (2).

A characterization of automata accepting saturated languages in $b$-complement representation is now given. This characterization and its proof is similar to the ones of (8).

Proposition \theproposition.

Let \mathcal{A}=\mathopen{}\mathclose{{}\left(Q,\Sigma_{b,d}\cup\mathopen{}\mathclose{{}\left\{\star}\right\},\delta,q_{0},F}\right) a weak Büchi automaton over alphabet \Sigma_{b,d}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}. It accepts a saturated language in $b$-complement if and only if:

$\delta(q_{0},\boldsymbol{a}\boldsymbol{a})=\delta(q_{0},\boldsymbol{a})$ for all \boldsymbol{a}\in\mathopen{}\mathclose{{}\left\{0,(b-1)}\right\}^{d}, 2. 2.

$\delta(q_{0},\boldsymbol{a})\in Q_{\emptyset}$ for all \boldsymbol{a}\in\Sigma_{b,d}\cup\mathopen{}\mathclose{{}\left\{\star}\right\}\setminus\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\{0,(b-1)}\right\}^{d}}\right), 3. 3.

for each $f\in[d-1]$, for each $q\in Q\setminus q_{0}$, accessible in $\mathcal{A}$ from $q_{0}$, for each $\boldsymbol{a}\in\Sigma_{b,d}$ with $a_{f}<b-1$,

[TABLE]

where $\boldsymbol{a}^{\prime}=a_{0}\dots a_{f-1}(a_{f}+1)a_{f+1}\dots a_{d-1}$ 4. 4.

[TABLE]

Property (4) allows to consider the case of the real 0. Note that Property (1) considers $b^{d}$ letters. It implies that this proposition does not lead to a polynomial time algorithm in the case of $d$-sequential automata. In the case of $d$-parallel automata, this proposition leads easily to algorithms, as Section 9 led to Theorem 10.1 and to Theorem 10.3.

Theorem 11.1**.**

Let \mathcal{A}=\mathopen{}\mathclose{{}\left(Q,\Sigma_{b,d}\cup\mathopen{}\mathclose{{}\left\{\star}\right\},\delta,q_{0},F}\right) an automaton with $n$ states reading reals in $b$-complement. It is decidable in time O\mathopen{}\mathclose{{}\left(n\log(n)db^{d}}\right) and space O\mathopen{}\mathclose{{}\left(nb^{d}}\right) whether $\mathcal{A}$ is a RVA.

Theorem 11.2**.**

Let \mathcal{A}=\mathopen{}\mathclose{{}\left(Q,\Sigma_{b}\cup\mathopen{}\mathclose{{}\left\{\star}\right\},\delta,q_{0},F}\right) a minimal weak Büchi automaton with $n$ states reading reals in $b$-complement. It is decidable in time O\mathopen{}\mathclose{{}\left(nb}\right) and space O\mathopen{}\mathclose{{}\left(n}\right) whether L_{\omega}\mathopen{}\mathclose{{}\left({\mathcal{A}}}\right) accepts a saturated language in $b$-complement.

12 Conclusion

In this paper, we have proven that it is decidable in quasi-linear time whether a weak Büchi automaton reading digits and dots accept a language which encode a saturated set of vector reals.

Two natural questions remain open.

Can this algorithm be adapted for some classes of automata which are not weak. Even in the case of dimension 1, it seems complicated to test whether L_{\omega}\mathopen{}\mathclose{{}\left({\mathcal{A}_{\delta(q,0)}}}\right)=L_{\omega}\mathopen{}\mathclose{{}\left({\mathcal{A}}}\right), when the automaton is not weak.

Given an automaton $\mathcal{A}$ which accept a set R\subseteq\mathopen{}\mathclose{{}\left(\mathbb{R}^{\geq 0}}\right)^{d}, is there some efficient way to compute a saturated automaton $\mathcal{A}^{\prime}$ which also accept $R$. One could compute a \FO\mathopen{}\mathclose{{}\left[\mathbb{R},\mathbb{Z}{};X_{b},+,<}\right]-formula defining $R$, and from this formula a saturated Büchi automaton. However, this method is inneficient, and does not preserve weakness.

Index

• \mathopen{}\mathclose{{}\left[{.}}\right]_{b}^{F} §3.1
• \mathopen{}\mathclose{{}\left[{.}}\right]_{b}^{I} §3.1
• \mathopen{}\mathclose{{}\left[{.}}\right]_{b}^{\mathbb{R}} §3.1
• $L^{*}$ §2
• $L^{+}$ §2
• $\boldsymbol{0}$ §2
• $\mathcal{A}_{q}$ for $\mathcal{A}$ an automaton and $q$ a state. §4.1, §4.1
• \mathopen{}\mathclose{{}\left[{\mathcal{A}}}\right]_{b}^{\mathbb{R}} Notation \thenotation
• Accessible §4.1
• $\mathcal{A}^{z\MVAt{}f}$ for $\mathcal{A}$ a $d$-parallel Büchi automaton Definition \thedefinition, Definition \thedefinition
• Alphabet §2
• Concatenation of words §2
• $d$-parallel language §3.4
• $d$-sequential language §3.4
• Deterministic Büchi automaton §4.1
• $\epsilon$ §2
• Finite word §2
• Fractional part of a word of $\Sigma_{b}^{*}\star\Sigma_{b}^{\omega}$ §3.1
• \mathopen{}\mathclose{{}\left[{L}}\right]_{b}^{\mathbb{R}} for $L$ a $d$-parallel language. §3.4
• Language §2
• Letter §2
• Morphism of automata §4.2, §4.2
• $\mathbb{N}{}$ §2
• \mathopen{}\mathclose{{}\left[n}\right] for $n\in\mathbb{N}{}$. §2
• Natural part of a word of $\Sigma_{b}^{*}\star\Sigma_{b}^{\omega}$ §3.1
• \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle w,S}\right\rangle}\right) §3.3
• Parallelization of a word §3.3
• Parallelization of an automaton §6.1
• \operatorname{par}_{d}\mathopen{}\mathclose{{}\left(L}\right) for $L$ a $d$-sequential language §3.4
• Predecessor state §4.1
• w\mathopen{}\mathclose{{}\left[<n}\right] - Prefix of $w$ of length $n$ §2
• $Q_{F}$ 3rd item
• $Q_{\emptyset}$ 1st item
• Quotient of automata §4.2
• $\mathbb{R}$ §2
• Run §4.1
• Run of an automaton §4.1
• Saturated language §3.4
• \operatorname{seq}_{d}\mathopen{}\mathclose{{}\left(\boldsymbol{w}}\right) §3.3
• Sequentialization of a word §3.3
• $\Sigma_{b,d}^{\square\MVAt{}f}$ Definition \thedefinition
• Strongly connected components §4.1
• w\mathopen{}\mathclose{{}\left[\geq{}n}\right] - Suffix of $w$ without its $n$ first letters. §2
• \operatorname{fix}^{z\MVAt{}f}\mathopen{}\mathclose{{}\left(\mathopen{}\mathclose{{}\left\langle\boldsymbol{w},S}\right\rangle}\right) Definition \thedefinition
• $\omega$-word §2