Bidirectional Nested Weighted Automata

TL;DR

This paper introduces bidirectional nested weighted automata (NWA), expanding their expressive power by allowing input processing in both directions, while maintaining similar computational complexity for key decision problems.

Contribution

The paper presents a novel bidirectional NWA framework, demonstrating increased expressiveness without added complexity for emptiness and universality problems.

Findings

Bidirectional NWA can express properties not possible with forward-only NWA.

Decidability and complexity results for emptiness and universality are preserved in the bidirectional setting.

Bidirectionality does not increase computational complexity for these decision problems.

Abstract

Nested weighted automata (NWA) present a robust and convenient automata-theoretic formalism for quantitative specifications. Previous works have considered NWA that processed input words only in the forward direction. It is natural to allow the automata to process input words backwards as well, for example, to measure the maximal or average time between a response and the preceding request. We therefore introduce and study bidirectional NWA that can process input words in both directions. First, we show that bidirectional NWA can express interesting quantitative properties that are not expressible by forward-only NWA. Second, for the fundamental decision problems of emptiness and universality, we establish decidability and complexity results for the new framework which match the best-known results for the special case of forward-only NWA. Thus, for NWA, the increased expressiveness of bidirectionality is achieved at no additional computational complexity. This is in stark contrast to the unweighted case, where bidirectional finite automata are no more expressive but exponentially more succinct than their forward-only counterparts.

Tables

Table 1. Table 1: The complexity of the emptiness problem for ( LimAvg ; g ) LimAvg 𝑔 (\textsc{LimAvg};g) -automata. The columns describe respectively: the value function g 𝑔 g , additional restrictions imposed on the problem, the complexity in the case with bidirectional slave automata, and the complexity in the previously studied  [ 13 , 14 ] case with only forward-walking slave automata. Results presented in this paper are boldfaced.

Value	Restrictions	Complexity	Complexity
func. $g$		Bidirectional	Forward case
Min,Max,	None	PSpace-complete	PSpace-complete [13]
${\text{Sum}}^{L,U}$		(Thm 6)
	finite	PSpace-hard	PSpace-hard
${\text{Sum}}^{+}$	width	ExpSpace	ExpSpace [13]
		(Thm 11)
${\text{Sum}}^{+}$,	constant width	NLogSpace-complete	NLogSpace-complete
Sum	unary weights	(Thm 17)	[14]
${\text{Sum}}^{+}$,	constant width	PTime	PTime [14]
Sum	binary weights	(Thm 17)
${\text{Sum}}^{+}$,	width given	PSpace-complete	PSpace-complete [14]
Sum	in unary	(Thm 17)

Full text

1 Introduction

We study an extension of nested weighted automata (NWA) [13] that can process words in both directions. We show that this new and natural framework can express many interesting quantitative properties that the previous formalism could not. We establish decidability and complexity results of the basic decision problems for the new framework. We start with the motivation for quantitative properties, then describe NWA and our new framework, and finally the contributions.

Weighted automata. Automata-theoretic formalisms provide a natural way to express quantitative properties of systems. Weighted automata extend finite automata where every transition is assigned an integer number called weight. Thus a run of an automaton gives rise to a sequence of weights. A value function aggregates the sequence of weights into a single value. For non-deterministic weighted automata, the value of a word $w$ is the infimum value of all runs over $w$. First, weighted automata were studied over finite words with weights from a semiring, and ring multiplication as value function [18], and later extended to infinite words with limit averaging or supremum as value function [12, 11, 10]. While weighted automata over semirings can express several quantitative properties [21], they cannot express long-run average properties that weighted automata with limit averaging can [12]. However, even weighted automata with limit averaging cannot express some basic quantitative properties (see [13]).

Nested weighted automata. A natural extension of weighted automata is to add nesting, which leads to nested weighted automata (NWA) [13]. A nested weighted automaton consists of a master automaton and a set of slave automata. The master automaton runs over input infinite words. At every transition the master can invoke a slave automaton that runs over a finite subword of the infinite word, starting at the position where the slave automaton is invoked. Each slave automaton terminates after a finite number of steps and returns a value to the master automaton. Each slave automaton is equipped with a value function for finite words, and the master automaton aggregates the returned values from slave automata using a value function for infinite words.

Advantages of NWA. We discuss the various advantages of NWA.

For Boolean finite automata, nested automata are equivalent to the non-nested counterpart, whereas NWA are strictly more expressive than non-nested weighted automata [13, Example 5]. It has been shown in [13] that NWA provide a specification framework where many basic quantitative properties can be expressed, which cannot be expressed by weighted automata. 2. 2.

NWA provide a natural and convenient way to express quantitative properties. Every slave automaton computes a subproperty, which is then combined using the master automaton. Thus NWA allow to decompose properties conveniently, and provide a natural framework to study quantitative run-time verification. 3. 3.

Finally, subclasses of NWA are equivalent in expressive power with automata with monitor counters [16], and thus they provide a robust framework to express quantitative properties.

Bidirectional NWA. Previous works considered slave automata that can only process input words in the forward direction (forward-only NWA). However, to specify quantitative properties, it is natural to allow slave automata to run backwards, for example, to measure the maximal or average time between a response and the preceding request. In this work we consider this natural extension of NWA, namely bidirectional NWA, where slave automata can process words in the forward as well as the backward direction.

Natural properties. First, we show that many natural properties can be expressed in the bidirectional NWA framework. We present two examples below (details in Section 3).

Average energy level. Consider a quantitative setting where each weight represents energy gain or consumption, and thus the sum of weights represents the energy level. To express the average energy level property, the master automaton has long-run average as the value function, and at every transition it invokes a slave automaton that walks backward with sum value function for the weights. Thus the average energy level property is naturally expressed by NWA with backward-walking slave automata, while this property is not expressible by NWA with forward-walking slave automata. 2. 2.

Data-consistency property (DCP). Consider the data-consistency property (DCP) where the input letters correspond to reads, writes, null instructions, and commits. For each read, the distance to the previous commit measures how fresh is the read with respect to the last commit, and this can be measured with a backward-walking slave automaton. For each write, the distance to the next commit measures how fresh is the write with respect to the following commit, and this can be measured with a forward-walking slave automaton. Thus the average freshness, called DCP, is expressed with bidirectional NWA. Moreover, the DCP can neither be expressed by NWA with only forward-walking slave automata nor by NWA with only backward-walking slave automata.

Our contributions. We propose bidirectional NWA as a specification framework for quantitative properties. First, we show that the classes of forward-only NWA and backward-only NWA have incomparable expressiveness, and bidirectional NWA strictly generalize both classes. Second, we establish complexity of the emptiness and universality problems for bidirectional NWA, where we consider the limit-average value function for the master automaton and for the slave automata we consider standard value functions for finite words (such as min, max, and variants of sum). The obtained complexity results coincide with the results for forward-only NWA, and range from NLogSpace-complete, PTime to PSpace-complete to ExpSpace. However the proofs for bidirectional NWA are much more involved than forward-only NWA. Thus bidirectional NWA have all the advantages of NWA but provide a more expressive framework for natural quantitative properties. Moreover, the added expressiveness of bidirectionality is achieved with no increase in the computational complexity of the decision problems (Table 1). We highlight two significant differences as compared to the unweighted case: (1) In the unweighted case bidirectionality does not change expressiveness, whereas we show for NWA it does; and (2) in the unweighted case for deterministic automata bidirectionality leads to exponential succinctness and increase in complexity of the decision problems, whereas for NWA bidirectionality does not change the computational complexity. Thus the combination of nesting and bidirectionality is very interesting in the weighted automata setting, which we study in this work.

Related works. Quantitative automata and logic have been extensively studied in recent years in many different contexts [18, 12, 4, 2]. The book [18] presents an excellent collection of results of weighted automata on finite words. Weighted automata on infinite words have been studied in [12, 11, 19]. Weighted automata over finite words extended with monitor counters have been considered (under the name of cost register automata) in [3, 20]. A version of nested weighted automata over finite words has been studied in [6], and nested weighted automata over infinite words has been studied in [13, 15, 14]. Several quantitative logics have also been studied, such as [5, 7, 1]. However, none of these works consider the rich and expressive formalism of quantitative properties expressible by NWA with slaves that walk both forward and backward, retaining decidability of the basic decision problems.

In the main paper, we present the key ideas and main intuitions of the proofs of selected results, and detailed proofs are relegated to the appendix.

2 Definitions

2.1 Words and automata

Words. We consider a finite alphabet of letters $\Sigma$. A word over $\Sigma$ is a (finite or infinite) sequence of letters from $\Sigma$. We denote the $i$-th letter of a word $w$ by $w[i]$, and for $i<j$ we define $w[i,j]$ as the word $w[i]w[i+1]\ldots w[j]$. The length of a finite word $w$ is denoted by $|w|$; and the length of an infinite word $w$ is $|w|=\infty$. For an infinite word $w$, word $w[i,\infty]$ is the suffix of $w$ with first $i-1$ letters removed. For a finite word $w$ of length $k$, we define the reverse of $w$, denoted by $w^{R}$, as the word $w[k]w[k-1]\ldots w[1]$.

Labeled automata. For a set $X$, an $X$-labeled automaton ${\cal A}$ is a tuple $\langle\Sigma,Q,Q_{0},\delta,F,{C}\rangle$, where (1) $\Sigma$ is the alphabet, (2) $Q$ is a finite set of states, (3) $Q_{0}\subseteq Q$ is the set of initial states, (4) $\delta\subseteq Q\times\Sigma\times Q$ is a transition relation, (5) $F$ is a set of accepting states, and (6) ${C}:\delta\mapsto X$ is a labeling function. A labeled automaton $\langle\Sigma,Q,\{q_{0}\},\delta,F,{C}\rangle$ is deterministic if and only if $\delta$ is a function from $Q\times\Sigma$ into $Q$ and $Q_{0}$ is a singleton.

Semantics of (labeled) automata. A run $\pi$ of a (labeled) automaton ${\cal A}$ on a word $w$ is a sequence of states of ${\cal A}$ of length $|w|+1$ such that $\pi[0]$ belongs to the initial states of ${\cal A}$ and for every $0\leq i\leq|w|-1$ we have $(\pi[i],w[i+1],\pi[i+1])$ is a transition of ${\cal A}$. A run $\pi$ on a finite word $w$ is accepting if and only if the last state $\pi[|w|]$ of the run is an accepting state of ${\cal A}$. A run $\pi$ on an infinite word $w$ is accepting if and only if some accepting state of ${\cal A}$ occurs infinitely often in $\pi$. For an automaton ${\cal A}$ and a word $w$, we define $\mathsf{Acc}(w)$ as the set of accepting runs on $w$. Note that for deterministic automata, every word $w$ has at most one accepting run ($|\mathsf{Acc}(w)|\leq 1$).

Weighted automata and their semantics. A weighted automaton is a $\mathbb{Z}$-labeled automaton, where $\mathbb{Z}$ is the set of integers. The labels are called weights. We define the semantics of weighted automata in two steps. First, we define the value of a run. Second, we define the value of a word based on the values of its runs. To define values of runs, we will consider value functions $f$ that assign real numbers to sequences of integers. Given a non-empty word $w$, every run $\pi$ of ${\cal A}$ on $w$ defines a sequence of weights of successive transitions of ${\cal A}$, i.e., ${C}(\pi)=({C}(\pi[i-1],w[i],\pi[i]))_{1\leq i\leq|w|}$; and the value $f(\pi)$ of the run $\pi$ is defined as $f({C}(\pi))$. We denote by $({C}(\pi))[i]$ the weight of the $i$-th transition, i.e., ${C}(\pi[i-1],w[i],\pi[i])$. The value of a non-empty word $w$ assigned by the automaton ${\cal A}$, denoted by ${\cal L}_{{{\cal A}}}(w)$, is the infimum of the set of values of all accepting runs; i.e., $\inf_{\pi\in\mathsf{Acc}(w)}f(\pi)$, and we have the usual semantics that the infimum of the empty set is infinite, i.e., the value of a word that has no accepting run is infinite. Every run $\pi$ on the empty word has length $1$ and the sequence ${C}(\pi)$ is empty, hence we define the value $f(\pi)$ as an external (not a real number) value $\bot$. Thus, the value of the empty word is either $\bot$, if the empty word is accepted by ${\cal A}$, or $\infty$ otherwise. To indicate a particular value function $f$ that defines the semantics, we call a weighted automaton ${\cal A}$ with value function $f$ an $f$-automaton.

Value functions. For finite runs we consider the following classical value functions: for runs of length $n+1$ we have

• •

Max and min: $\textsc{Max}(\pi)=\max_{i=1}^{n}({C}(\pi))[i]$ and $\textsc{Min}(\pi)=\min_{i=1}^{n}({C}(\pi))[i]$.

• •

Sum and absolute sum: the sum function $\textsc{Sum}(\pi)=\sum_{i=1}^{n}({C}(\pi))[i]$, the absolute sum $\textsc{Sum}^{+}(\pi)=\sum_{i=1}^{n}\mathop{\mathsf{Abs}}(({C}(\pi))[i])$, where $\mathop{\mathsf{Abs}}(x)$ is the absolute value of $x$.

• •

Variants of bounded sum: we consider a family of functions called the (variant of) bounded sum value function $\textsc{Sum}^{L,U}$. Each of these functions returns the sum if all the partial sums are in the interval $[L,U]$, otherwise there are many possibilities which lead to multiple variants. For example, we can require that for all prefixes $\pi^{\prime}$ of $\pi$ we have $\textsc{Sum}(\pi^{\prime})\in[L,U]$. We can impose a similar restriction on all suffixes, all infixes etc. Moreover, if partial sums are not contained in $[L,U]$, a bounded sum can return $\infty$, the first violated bound, etc.

For infinite runs we consider:

• •

Limit average: $\textsc{LimAvg}(\pi)=\liminf\limits_{k\rightarrow\infty}\frac{1}{k}\cdot\sum_{i=1}^{k}({C}(\pi))[i]$.

Silent moves. Consider a $(\mathbb{Z}\cup\{\bot\})$-labeled automaton. We consider such an automaton as an extension of a weighted automaton in which transitions labeled by $\bot$ are silent, i.e., they do not contribute to the value of a run. Formally, for every function $f\in\mathsf{InfVal}$ we define $\mathsf{sil}({f})$ as the value function that applies $f$ on sequences after removing $\bot$ symbols. The significance of silent moves is as follows: it allows to ignore transitions, and thus provides robustness where properties could be specified based on desired events rather than steps.

2.2 Nested weighted automata

Nested weighted automata (NWA) have been introduced in [13] and originally allowed slave automata to move only forward. The variant we define here allow two types of slave automata, forward walking and backward walking. The original definition of NWA from [13] is versatile and hence it can be seamlessly extended to the case with bidirectional (forward- and backward-walking) slave automata. We follow the description of [13].

Informal description. A nested weighted automaton consists of a labeled automaton over infinite words, called the master automaton, a value function $f$ for infinite words, and a set of weighted automata over finite words, called slave automata. A nested weighted automaton can be viewed as follows: given a word, we consider the run of the master automaton on the word, but the weight of each transition is determined by dynamically running slave automata; and then the value of a run is obtained using the value function $f$. That is, the master automaton proceeds on an input word as an usual automaton, except that before taking a transition, it starts a slave automaton corresponding to the label of the current transition. The slave automaton starts at the current position of the master automaton in the input word and works on some finite part of it. There are two types of slave automata: (a) forward walking, which move onward the input word (toward higher positions), and (b) backward walking, which move towards the beginning of the input word. Once a slave automaton finishes, it returns its value to the master automaton, which treats the returned value as the weight of the current transition that is being executed. The slave automaton might immediately accept and return value $\bot$, which corresponds to a silent transition, i.e., transition with no weight. If one of slave automata rejects, the nested weighted automaton rejects. We present two examples of properties expressible by NWA. Additional examples are presented in Section 3.

Example 1** (Average response time and its dual).**

Consider infinite words over $\{r,g,\#\}$, where $r$ represents requests, $g$ represents grants, and $\#$ represents idle. A basic and interesting property is the average number of letters between a request and the corresponding grant, which represents the long-run average response time (ART) of the system. This property cannot be expressed by a non-nested automaton [13]. ART can be expressed by a deterministic nested weighted automaton, which basically implements the definition of ART. This automaton invokes at every request a forward-walking slave automaton with $\textsc{Sum}^{+}$ value function, which counts the number of events until the following grant. On the other events the NWA takes silent transitions. Finally, the master automaton applies LimAvg value function to the values returned by slave automata. Figure 1 presents a run of the NWA computing ART.

We define the average workload property (AW), which measures the average number of pending requests. The average is computed over all positions in a word. Intuitively, if we pick a position in word $w$ at random, the expected number of pending requests is the average workload of $w$. Formally, we define the workload at $i$ in $w$, denoted $wl(w,i)$, as the number of letters $r$ among $w[j,i]$, where $j$ is the last position in $w[1,i]$ where $g$ occurs or $1$ if such a position does not exist. The average workload of $w$ is the limit average over all positions $i$ of $wl(w,i)$.

AW can be expressed by a deterministic $(\textsc{LimAvg};\textsc{Sum}^{+})$-automaton with backward-walking slave automata. Basically, the NWA invokes at every position a slave automaton, which counts the number of $r$ letter from its current position to the first position containing letter $g$, where it terminates. Since slave automata run backwards, each of them computes the workload at the position of its invocation. Figure 1 presents a run of the NWA computing AW.

Now, we present a formal definition of NWA and their semantics.

Nested weighted automata. A nested weighted automaton (NWA) with bidirectional slave automata is a tuple $\langle{\cal A}_{mas};f;{\mathfrak{B}}_{-m},\ldots,{\mathfrak{B}}_{0},\ldots,{\mathfrak{B}}_{l}\rangle$, with $m,l\in\mathbb{N}$ where (1) ${\cal A}_{mas}$, called the master automaton, is a $\{-m,\ldots,l\}$-labeled automaton over infinite words (the labels are the indexes of automata ${\mathfrak{B}}_{-m},\ldots,{\mathfrak{B}}_{l}$), (2) $f$ is a value function on infinite words, called the master value function, and (3) ${\mathfrak{B}}_{-m},\ldots,{\mathfrak{B}}_{l}$ are weighted automata over finite words called slave automata. Intuitively, an NWA can be regarded as an $f$-automaton whose weights are dynamically computed at every step by the corresponding slave automaton. The automata ${\mathfrak{B}}_{-m},\ldots,{\mathfrak{B}}_{-1}$ (resp., ${\mathfrak{B}}_{1},\ldots,{\mathfrak{B}}_{l}$) are called backward walking (resp., forward walking) slave automata. We refer to NWA with both forward and backward walking slave automata as bidirectional NWA. The automaton ${\mathfrak{B}}_{0}$ immediately accepts and returns no weight; it is used to implement silent transitions, which have no weight. We define an $(f;g)$-automaton as an NWA where the master value function is $f$ and all slave automata are $g$-automata.

Semantics: runs and values. A run of $\mathbb{A}$ on an infinite word $w$ is an infinite sequence $(\Pi,\pi_{1},\pi_{2},\ldots)$ such that (1) $\Pi$ is a run of ${\cal A}_{mas}$ on $w$; (2) for every $i>0$ the label $j={C}(\Pi[i-1],w[i],\Pi[i])$ pointers at a slave automaton and (a) if $j<0$, then $\pi_{i}$ is a run of the automaton ${\mathfrak{B}}_{j}$ on some prefix of the reverse word $(w[1,i])^{R}$, and (b) if $j\geq 0$, then $\pi_{i}$ is a run of the automaton ${\mathfrak{B}}_{j}$ on some finite prefix of $w[i,\infty]$. The run $(\Pi,\pi_{1},\pi_{2},\ldots)$ is accepting if all runs $\Pi,\pi_{1},\pi_{2},\ldots$ are accepting (i.e., $\Pi$ satisfies its acceptance condition and each $\pi_{1},\pi_{2},\ldots$ ends in an accepting state) and infinitely many runs of slave automata have length greater than $1$ (the master automaton takes infinitely many non-silent transitions). The value of the run $(\Pi,\pi_{1},\pi_{2},\ldots)$ is defined as $\mathsf{sil}({f})(v(\pi_{1})v(\pi_{2})\ldots)$, where $v(\pi_{i})$ is the value of the run $\pi_{i}$ in the corresponding slave automaton, and $\mathsf{sil}({f})$ is the value function that takes its input sequence, removes $\bot$ symbols and applies $f$ to the remaining sequence. The value of a word $w$ assigned by the automaton $\mathbb{A}$, denoted by ${\cal L}_{{\mathbb{A}}}(w)$, is the infimum of the set of values of all accepting runs. We require accepting runs to contain infinitely many non-silent transitions as $f$ is a value function over infinite sequences, hence the sequence $v(\pi_{1})v(\pi_{2})\ldots$ with $\bot$ removed must be infinite.

Deterministic nested weighted automata. An NWA $\mathbb{A}$ is deterministic if (1) the master automaton and all slave automata are deterministic, and (2) in all slave automata, accepting states have no outgoing transitions. Intuitively, a slave automaton in an accepting state can choose (non-deteministically) to terminate or continue running; condition (2) removes this source of non-determinism.

Width of NWA. An NWA has width $k$ if and only if in every run at every position at most $k$ slave automata are active.

3 Examples

In this section we present several examples of quantitative properties that can be expressed with bidirectional NWA.

Example 2** (Average energy level).**

We consider the average energy level property studied in [17, 8]. Consider $W\in\mathbb{N}$ and an alphabet $\Sigma_{W}$ consisting of integers from interval $[-W,W]$. These letters correspond to the energy change, i.e., negative values represent energy consumption whereas positive values represent energy gain. For $w\in\Sigma_{W}$ we define the energy level at $i$ as the sum $w[1]+\ldots+w[i]$. The average energy property (AE) is the limit average of the energy levels at every position. For example, the average energy level of $2(-1)3((-1)1)^{\omega}$ is $4$.

AE can be expressed by a $(\textsc{LimAvg};\textsc{Sum})$-automaton $\mathbb{A}$ with backward-walking slave automata, but it is not expressible by $(\textsc{LimAvg};\textsc{Sum})$-automata with forward-walking slave automata. To express AE, a $(\textsc{LimAvg};\textsc{Sum})$-automaton $\mathbb{A}$ with backward-walking slave automata invokes at every position a slave automaton, which runs backward to the beginning of the word and sums up all the letters. In contrast, $(\textsc{LimAvg};\textsc{Sum})$-automata with forward-walking slave automata can use finite memory of the master automaton, but finite prefixes influence only finitely many values returned by slave slave automata and the limit-average value function neglects finite prefixes. Formally, we can show with a simple pumping argument that for every $(\textsc{LimAvg};\textsc{Sum})$-automaton with forward-walking slave automata, among words $w_{i}=1^{i}0^{\omega}$ there exists a pair of words with the same value. In contrast, all these words have different AE (AE of $w_{i}$ is $i$).

AE property is often considered in conjunction with bounds on energy values. Typically, energy should not drop below some threshold, in particular, it should not be negative. In addition, the energy storage is limited, which motivates the upper bound on the stored energy, where the excess energy is released. These two restrictions lead to the interval constraint on energy levels, i.e., we require the energy level at every position to belong to a given interval $[L,U]$, which results in a variant of the bounded sum $\textsc{Sum}^{L,U}$.

Example 3** (Data consistency).**

Consider a database server, which processes instructions grouped into transactions. There are four instructions: read $r$, write $w$, void $\#$ and commit $c$. The commit instruction applies all writes, finishes the current transaction and starts a new one. The read instructions refer to writes applied before the previous commit.

In the presence of multiple clients connected to the database, there are two options to achieve consistency. One option is to use locks that can limit concurrency. A second approach is optimistic concurrency which proceeds without locks, and then rolls back in case there was a collision between transactions. In ordered to limit the number of roll backs, it is preferred that the read instructions occur shortly after commit, while write instructions are followed by the commit instruction as quickly as possible. Formally, we define (a) consistency (or freshness) of a read instruction as the number of steps to the first preceding commit instruction, and (b) consistency of a write instruction as the number of steps to the following commit instruction. The data consistency property (DCP) of $w$ is the limit average of consistency of reads and writes in $w$.

DCP is expressed by the following deterministic $(\textsc{LimAvg};\textsc{Sum}^{+})$-automaton $\mathbb{A}$ with bidirectional slave automata. On every read $r$ (resp., $w$), the NWA $\mathbb{A}$ invokes a slave automaton which walks backward (resp., forward) and counts the number of steps to the first encountered $c$. On the remaining instructions $c,\#$, the NWA $\mathbb{A}$ invokes a dummy slave automaton which corresponds to a silent transition.

Example 4**.**

Consider the framework of Example 3. For every position with read $r$ or write $w$ we define a regret at position $i$ as the minimal distance to the preceding or the following commit $c$. Intuitively, the regret corresponds to the number of instructions by which we have to prepone or postpone the commit to include the instruction at the current position. We consider the minimal regret property (MR) on words over $\{r,w,c,\#\}$ defined the limit average over positions with $r$ and $w$ of the regret at these positions. MR can be expressed by a non-deterministic $(\textsc{LimAvg};\textsc{Sum}^{+})$-automaton with bidirectional slave automata, which basically implements the definition of MR (the non-deterministic guess is whether it is the preceding or the following commit). The NWA invokes at every $r$ or $w$ position one of the following two slave automata ${\mathfrak{B}}_{B},{\mathfrak{B}}_{F}$. The automaton ${\mathfrak{B}}_{B}$ counts the number of steps to the preceding grant, while ${\mathfrak{B}}_{F}$ counts the number of steps to the following grant.

4 Decision questions

For NWA with bidirectional slave automata, we consider the quantitative counterparts of the fundamental problems of emptiness and universality. The (quantitative) emptiness and universality problems are defined in the same way for weighted automata and all variants of NWA; in the following definition ${\cal A}$ denotes either a weighted automaton or an NWA.

Emptiness and universality. Given an automaton ${\cal A}$ and a threshold $\lambda$, the emptiness (resp. universality) problem asks whether there exists a word $w$ with ${\cal L}_{\cal A}(w)\leq\lambda$ (resp., for every word $w$ we have ${\cal L}_{\cal A}(w)\leq\lambda$).

Remark 5**.**

The emptiness and universality problems have been studied for forward-only NWA in [13].

• •

For NWA the value functions considered for the master automaton are the infimum (or limit-infimum), the supremum (or limit-supremum), and the limit-average. For all the decidability results for the infimum (limit-infimum) and the supremum (limit-supremum) value functions the techniques are similar to unweighted automata **[13]**, which can be easily adapted to the bidirectional framework. Hence in the sequel we only focus on bidirectional NWA with the limit-average value function for the master automaton.

• •

Moreover, we study only the emptiness problem for the following reasons. First, for the deterministic case the emptiness and the universality problems are similar and hence we focus on the emptiness problem. Second, in the non-deterministic case the universality problem is already undecidable for LimAvg-automata even with no nesting **[9]**.

4.1 The minimum, maximum and bounded sum value functions

First, we show that for $g$ being $\textsc{Min},\textsc{Max}$, or a variant of the bounded sum value function $\textsc{Sum}^{L,U}$, the emptiness problem for $(\textsc{LimAvg};g)$-automata with bidirectional slave automata is decidable in PSpace. To show that, we prove a stronger result, i.e., every $(\textsc{LimAvg};g)$-automaton can be effectively transformed to a LimAvg-automaton of exponential size.

Key ideas. Weighted automata with value functions $\textsc{Min},\textsc{Max},\textsc{Sum}^{L,U}$ are close to (non-weighted) finite-state automata. In particular, these automata have finite range and for each value $\lambda$ from the range, the set of words of value $\lambda$ is regular. Thus, instead of invoking a slave automaton, the master automaton can non-deterministically pick value $\lambda$ and verify that the value returned by this slave automaton is $\lambda$. For backward-walking slave automata the guessing can be avoided as the master automaton can simulate (the reverse of) runs of all backward-walking slave automata until the current position. Thus, we can eliminate slave automata from NWA, i.e., we transform such NWA to weighted automata. Formally, we show that for $g\in\{\textsc{Min},\textsc{Max},\textsc{Sum}^{L,U}\}$, every $(\textsc{LimAvg};g)$-automaton with bidirectional slave automata can be transformed into an equivalent LimAvg-automaton of exponential size. The emptiness problem for non-deterministic LimAvg-automata is in NLogSpace (assuming weights given in unary) and hence we have the containment part in the following Theorem 6. The hardness part follows from PSpace-hardness of the emptiness problem for $(\textsc{LimAvg};g)$-automata with forward-walking slave automata only [13].

Theorem 6**.**

Let $g\in\{\textsc{Min},\textsc{Max},\textsc{Sum}^{L,U}\}$. The emptiness problem for non-deterministic $(\textsc{LimAvg};g)$-automata with bidirectional slave automata is PSpace-complete.

Note. The complexity in Theorem 6 does not depend on encoding of weights in slave automata, i.e., the problem is PSpace-hard even for a fixed set of weights, and it remains in PSpace for weights encoded in binary.

The average energy property from Example 2 with bounds on energy levels can be expressed with $(\textsc{LimAvg};\textsc{Sum}^{L,U})$-automata. The emptiness problem for these automata is decidable by Theorem 6.

Remark 7** (Parametrized complexity).**

If we assume that the size of slave automata in Theorem 6 is bounded by a constant, the complexity of the emptiness problem drops to NLogSpace-complete. NLogSpace-hardness follows from NLogSpace-hardness of the emptiness problem for LimAvg-automata, which can be considered as a special case of NWA.

The results of this section apply to general bidirectional NWA. In the following section we consider bidirectional NWA with the sum value function, where we consider additional restrictions of finite width (Section 5) and bounded width (Section 6). We also justify in Remark 9 that the finite width restriction is natural.

5 Finite-width case

In this section we study NWA satisfying the finite width condition. First, we briefly discuss the finite-width condition and argue that it is a natural restriction. Next, we show that the emptiness problem for (finite-width) $(\textsc{LimAvg};\textsc{Sum}^{+})$-automata with bidirectional slave automata is decidable in ExpSpace. We conclude this section with the expressiveness results; we show that classical NWA with forward-walking slave automata and NWA with backward-walking slave automaton have incomparable expressive power. Hence, (finite-width) $(\textsc{LimAvg};\textsc{Sum}^{+})$-automata with bidirectional slave automata are strictly more expressive than NWA with one-direction slave automata.

5.1 The finite-width condition

Finite width. An NWA $\mathbb{A}$ has finite width if and only if in every accepting run of $\mathbb{A}$ at every position at most finitely many slave automata are active. Classical NWA with forward-walking slave automata only have finite width. Indeed, in any run, at any position $i$ at most $i$ slave automata can be active.

Example 8**.**

Consider an NWA over $\{a,b\}$ such that the master automaton accepts a single word $ab^{\omega}$ and all slave automata are backward walking and accept words $b^{*}a$. All slave automata terminate at the first position of $ab^{\omega}$ and hence this NWA does not have finite width.

The automata expressing properties from Examples 1, 3 and 4 are finite-width $(\textsc{LimAvg};\textsc{Sum}^{+})$-automata with bidirectional slave automata. Observe that an NWA does not have finite width if and only if it has an accepting run, in which at some position $i$ infinitely many backward-walking slave automata terminate.

Remark 9** (Finite width is natural for positive sum).**

Let $\mathbb{A}$ be a $(\textsc{LimAvg};\textsc{Sum}^{+})$-automaton with bidirectional slave automata. Except for degenerate cases, runs of $\mathbb{A}$, which do not have finite width, have infinite value. Indeed, consider a run $\pi$ and a position $i_{0}$ at which infinitely many automata are active. Since only finitely many forward-walking slave automata are active at $i_{0}$, infinitely many of them are backward-walking and for some position $i<i_{0}$, infinitely many slave automata $S$ terminate at position $i$. Then, one of the following holds: either that value of this run is infinite or one of the following two degenerate cases happen: (a) The slave automata from $S$ are invoked with zero density (i.e., if consider the long-run average of the frequency of invoking slave automata, then it is zero). This situation represents that monitoring with slave automata happens with vanishing frequency which is a degenerate case. (b) The values returned by the slave automata from $S$ are bounded. It follows that these automata take transitions of non-zero weight only in some finite subword $w[i,j]$ of the input word $w$. This situation represents monitoring of an infinite sequence, in which all events past position $j$ are irrelevant. This is a degenerate case in the infinite-word case.

The finite-width property does not depend on weights and hence we can construct an exponential-size Büchi automaton ${\cal A}$, which simulates runs of a given NWA $\mathbb{A}$. Having ${\cal A}$, we can check whether it has a run corresponding to an accepting run of $\mathbb{A}$, in which infinitely many backward-walking slave automata terminate at the same position. This check can be done in logarithmic space and hence checking the finite-width property is in PSpace. A simple reduction from the non-emptiness problem for NWA shows PSpace-hardness of checking the finite-width property.

Theorem 10**.**

The problem whether a given NWA has finite width is PSpace-complete.

5.2 The absolute sum value function

We present the main result on NWA of finite width.

Theorem 11**.**

The emptiness problem for finite-width $(\textsc{LimAvg};\textsc{Sum}^{+})$-automata with bidirectional slave automata is PSpace-hard and it is decidable in ExpSpace.

Key ideas. PSpace-hardness follows from PSpace-hardness of the emptiness problem for $(\textsc{LimAvg};\textsc{Sum}^{+})$-automata with forward-walking slave automata only. Containment in ExpSpace is shown by reduction to the bounded-width case, which is shown decidable in the following section (Theorem 17). We briefly describe this reduction. Consider a finite-width $(\textsc{LimAvg};\textsc{Sum}^{+})$-automaton $\mathbb{A}$ with bidirectional slave automata. First, we observe that without loss of generality, we can assume that $\mathbb{A}$ is deterministic. Second, we observe that in every word accepted by $\mathbb{A}$, at almost every position $i$ there exists a barrier, which is a word $u$ such that (a) the word $w^{\prime}=w[1,i]uw[i+1,\infty]$, i.e., $w$ with $u$ inserted at position $i$, is accepted by $\mathbb{A}$, and the runs on $w$ and $w^{\prime}$ coincide except for positions in $w^{\prime}$ corresponding to $u$, (b) in the run on $w^{\prime}$, backward-walking slave automata active at the end of $u$ terminate within $u$, (c) in the run on $w^{\prime}$, forward-walking slave automata active at the beginning of $u$ terminate within $u$, and (d) $u$ has exponential length. Basically, active slave automata cannot cross $u$ in $w^{\prime}$ and in the effect insertion of $u$ bounds the number of active slave automata. Existence of barriers follows from the finite-width property of $\mathbb{A}$.

We insert barriers in $w$ to reduce the number of active slave automata. While inserting $u$ at a certain position may increase the partial average, we show that if at position $i$ in $w$, exponentially many active slave automata accumulates exponential weight past crossing $i$ (some slave automata walk forward while other backwards), all partial averages (of values returned by slave automata) in $w^{\prime}$ are bounded by the corresponding partial averages in $w$. We conclude that for every word $w$, there exists a word $w^{\prime}$ such that (i) at every position at most exponentially many slave automata accumulate exponential values, and (ii) the value of $w^{\prime}$ does not exceed the value of $w$. Thus, to compute the infimum over all runs of $\mathbb{A}$, we can focus on runs in which at every position at most exponentially many slave automata accumulate exponential value. Runs of slave automata in which they accumulate bounded (exponential) values can be eliminated as in Theorem 6, i.e., we can construct an exponential size NWA $\mathbb{A}^{\prime}$, which simulates $\mathbb{A}$, and such that its slave automata run as long as they can accumulate value exponential (in $|\mathbb{A}|$) and otherwise they non-deterministically pick the remaining value and the master automaton verifies that the pick is correct. Therefore, the infimum over all runs of $\mathbb{A}$ coincides with the infimum over all runs of $\mathbb{A}^{\prime}$ of width exponentially bounded.

Remark 12** (Parametrized complexity).**

If we assume that the size of slave automata in Theorem 11 is bounded by a constant, the complexity of the emptiness problem drops to NLogSpace-complete. NLogSpace-hardness follows from NLogSpace-hardness of the emptiness problem for LimAvg-automata, which can be viewed as a special case of NWA.

5.3 Expressive power

DCP defined in Example 3 can be expressed by a deterministic finite-width $(\textsc{LimAvg};\textsc{Sum}^{+})$-automaton with bidirectional slave automata. We show that both forward-walking and backward-walking slave automata are required to express DCP. That is, we formally show that DCP cannot be expressed by any (non-deterministic) $(\textsc{LimAvg};\textsc{Sum}^{+})$-automaton with slave automata walking in one direction only.

Classes of NWA. We define $\mathcal{FB}(\textsc{LimAvg};\textsc{Sum}^{+})$ as the class of all finite-width $(\textsc{LimAvg};\textsc{Sum}^{+})$-automata with bidirectional slave automata. We define $\mathcal{F}(\textsc{LimAvg};\textsc{Sum}^{+})$ (resp., $\mathcal{B}(\textsc{LimAvg};\textsc{Sum}^{+})$) as the subclass of $\mathcal{FB}(\textsc{LimAvg};\textsc{Sum}^{+})$ consisting of NWA with forward-walking (resp., backward-walking) slave automata only.

We establish that classes $\mathcal{F}(\textsc{LimAvg};\textsc{Sum}^{+})$ and $\mathcal{B}(\textsc{LimAvg};\textsc{Sum}^{+})$ have incomparable expressive power and hence they are strictly less expressive than class $\mathcal{FB}(\textsc{LimAvg};\textsc{Sum}^{+})$.

Key ideas. Consider a word $w=(c\#^{N}r^{2K}c\#^{2N}r^{K})^{\omega}$ for some big $K$ and much bigger $N$. An NWA from $\mathcal{B}(\textsc{LimAvg};\textsc{Sum}^{+})$ computes DCP of $w$ by invoking (non-dummy) slave automata at every $r$ letter and taking silent transitions on letters $\#,c$. We show that an NWA $\mathbb{A}$ from $\mathcal{F}(\textsc{LimAvg};\textsc{Sum}^{+})$ cannot invoke the right number of slave automata, even if it uses non-determinism. More precisely, we show that $\mathbb{A}$ computing DCP has to invoke at most $O(K)$ non-dummy slave automata on average on subwords $c\#^{N}r^{2K}c\#^{2N}r^{K}$. Since $N$ is much bigger than $K$, we conclude that $\mathbb{A}$ has a cycle over $\#$ letters at which it takes only silent transitions and a cycle over $r$ letters on which it increases the multiplicity of active slave automata. Using these two cycles, we construct a run of value smaller than DCP, which contradicts the assumption that $\mathbb{A}$ computes DCP. Similarly, we can show that an NWA from $\mathcal{B}(\textsc{LimAvg};\textsc{Sum}^{+})$ cannot compute correctly DCP of words of the form $w=(cw^{2K}\#^{N}cw^{K}\#^{2N})^{\omega}$, while on these words DCP is expressible by an NWA from $\mathcal{F}(\textsc{LimAvg};\textsc{Sum}^{+})$.

Lemma 13**.**

(1) DCP restricted to alphabet $\{r,\#,c\}$ is expressed by an NWA from $\mathcal{B}(\textsc{LimAvg};\textsc{Sum}^{+})$, but it is not expressible by NWA from $\mathcal{F}(\textsc{LimAvg};\textsc{Sum}^{+})$. (2) DCP restricted to alphabet $\{w,\#,c\}$ is expressed by an NWA from $\mathcal{F}(\textsc{LimAvg};\textsc{Sum}^{+})$, but it is not expressible by NWA from $\mathcal{B}(\textsc{LimAvg};\textsc{Sum}^{+})$.

The above lemma implies that DCP over alphabet $\{r,w,\#,c\}$ is not expressible by any NWA from $\mathcal{F}(\textsc{LimAvg};\textsc{Sum}^{+})$ nor from $\mathcal{B}(\textsc{LimAvg};\textsc{Sum}^{+})$. In conclusion, we have:

Theorem 14**.**

(1) $\mathcal{F}(\textsc{LimAvg};\textsc{Sum}^{+})$ and $\mathcal{B}(\textsc{LimAvg};\textsc{Sum}^{+})$ have incomparable expressive power. (2) $\mathcal{FB}(\textsc{LimAvg};\textsc{Sum}^{+})$ are strictly more expressive than $\mathcal{F}(\textsc{LimAvg};\textsc{Sum}^{+})$ and $\mathcal{B}(\textsc{LimAvg};\textsc{Sum}^{+})$.

6 Bounded-width case

In this section, we study $(\textsc{LimAvg};\textsc{Sum})$-automata with bidirectional slave automata, which have bounded width. The bounded width restriction has been introduced in [14] to improve the complexity of the emptiness problem and to establish decidability of the emptiness problem for $(\textsc{LimAvg};\textsc{Sum})$-automata. NWA considered in [14] have only forward-walking slave automata, while we extend these results to NWA with bidirectional slave automata. This extension preserves the complexity bounds from [14], i.e., the emptiness problem is in PTime for constant width and PSpace-complete for width given in unary.

The bounded width restriction emerges naturally in examples presented so far. If we bound the number of pending requests, we can express ART and AW (Examples 1 and 1) by automata of bounded width. If we bound the number of writes and reads between any two commits, then DCP and MR (Examples 3 and 4) can be expressed by NWA of bounded width. These natural restrictions lead to more efficient decision procedures.

The decision procedure in this section differs from the one from [14]. The key step in the decidability proof from [14] is establishing the following dichotomy: either the infimum over values of all words is $-\infty$ or the infimum is realized by dense runs. A run is dense if for the values $v_{1},v_{2},\ldots$ returned by slave automata invoked at positions $1,2,\ldots$ we have $\frac{v_{i}}{i}$ converges to [math], i.e., values returned by slave automata are sublinear in the positions of their invocation. Properties of dense runs allow for further reductions, which lead to a decision procedure. However, we show in the following Example 15 that in case of NWA with bidirectional slave automata, dense runs may not attain the infimum of all runs.

Example 15**.**

Consider a $(\textsc{LimAvg};\textsc{Sum})$-automaton $\mathbb{A}$ with bidirectional slave automata over $\Sigma=\{a,b,c\}$. The NWA $\mathbb{A}$ accepts words $(ab^{*}c)^{\omega}$ and it works as follows. On letters $a$, $\mathbb{A}$ invokes a forward-walking slave automaton ${\mathfrak{B}}_{a}$, which returns the number of the following $b$ letters up to $c$. On letters $c$, $\mathbb{A}$ invokes a backward-walking slave automaton ${\mathfrak{B}}_{c}$, which returns the number of the preceding $b$ letters since $a$. Finally, on $b$ letters, $\mathbb{A}$ invokes a slave automaton ${\mathfrak{B}}_{b}$, which takes a single transition and returns value [math]. The NWA $\mathbb{A}$ has width $3$. We can show that the value of any dense run, is $2$. However, the infimum over values of all words is $1$. The partial average of the values returned by slave automata on finite word $u=(ab^{*}c)^{*}$ is $2$, while the partial average over $uab^{N}$ is $\frac{2|u|+N}{|u|+N}$. Therefore, the value, which is limit infimum over partial averages, of word $ab^{n_{1}}c\ldots ab^{n_{i}}c\ldots$ is $1$ if sequence $n_{1},\ldots$ is grows rapidly (e.g. doubly-exponentially).

Main ideas. In Example 15, the words attaining the least value contain long blocks of letter $b$, at which the NWA $\mathbb{A}$ is (virtually) in the same state, i.e., it loops in this state. On letters $b$, the sum of all weights collected by all active slave automata is $2$, i.e., automata ${\mathfrak{B}}_{a},{\mathfrak{B}}_{c}$ collect weight $1$ and ${\mathfrak{B}}_{b}$ collect [math]. However, in computing limit infimum over partial averages, we pick positions just before letter $c$ as they correspond to the local minima, i.e., we compute the partial average over prefixes $uab^{N}$, and hence the weights collected by ${\mathfrak{B}}_{c}$ do not contribute to this partial average. Then, the sum of all weights collected by slave automata ${\mathfrak{B}}_{a},{\mathfrak{B}}_{b}$ over a letter $b$ is $1$, which is equal to the least value of the limit infimum of the partial averages. In the following, we extend this idea and present the solution of all bounded-width $(\textsc{LimAvg};\textsc{Sum})$-automata with bidirectional slave automata. We show that the infimum over all words of a given NWA is the least average value over all cycles. In the following, we define appropriate notions of cycles of NWA and their average with exclusion of some slave automata.

The graph of $k$-configurations. Let $\mathbb{A}$ be a non-deterministic $(\textsc{LimAvg};\textsc{Sum})$-automaton of width $k$. We define a $k$-configuration of $\mathbb{A}$ as a tuple $(q;q_{1},\ldots,q_{k})$ where $q$ is a state of the master automaton, and each $q_{1},\ldots,q_{k}$ is either a state of a slave automaton of $\mathbb{A}$ or $\bot$. Given a run of $\mathbb{A}$, we say that $(q;q_{1},\ldots,q_{k})$ is the $k$-configuration at position $i$ in the run if $q$ is the state of the master automaton at position $i$ and there are $l\leq k$ active slave automata at position $i$, whose states are $q_{1},\ldots,q_{l}$ ordered by position of invocation (backward-walking slave automata are invoked past position $i$). If $l<k$, then $q_{l+1},\ldots,q_{k}=\bot$. We say that a $k$-configuration $C_{2}$ is a successor of a $k$-configuration $C_{1}$ if there exists an accepting run of $\mathbb{A}$ and $i>0$ such that $C_{1}$ is the $k$-configuration at $i$ and $C_{2}$ is the $k$-configuration at $i+1$ The graph of $k$-configurations of $\mathbb{A}$ is the set of $k$-configurations of $\mathbb{A}$, which occur infinitely often in some accepting run, with the successor relation.

Characteristics of cycles. Let $\mathcal{C}$ be a cycle in a graph of $k$-configurations of $\mathbb{A}$. Let $F$ (resp., $B$) be the set of forward-walking (resp., backward-walking) slave automata, which are active throughout $\mathcal{C}$, i.e., which are not invoked nor terminated within $\mathcal{C}$. A focus $Fc$ (for $\mathcal{C}$) is a downward closed subset of $F$, i.e., it contains all automata from $F$ invoked before some position. We define a focused gain $\textsc{Gain}(\mathcal{C},Fc)$ as the sum of weights which automata from $Fc$ accumulate over $\mathcal{C}$. A restriction $R$ (for $\mathcal{C}$) is an upward closed subset of $B$, i.e., it contains all automata from $B$ invoked past certain position. We define an average weight of $\mathcal{C}$ excluding $R$, denoted by $\textsc{AvgE}(\mathcal{C},R)$, as the sum of weights of all transitions of slave automata within $\mathcal{C}$, except of transitions of slave automata from $R$, divided by the number of slave automata invoked within $\mathcal{C}$.

Intuitively, a focused gain refers to the value, which forward-walking slave automata invoked before some position $i$, accumulate over the part of run corresponding to $\mathcal{C}$ (see Figure 2). If the focused gain $\textsc{Gain}(\mathcal{C},Fc)$ is negative, then by pumping $\mathcal{C}$ we can arbitrarily decrease the partial average of the values of slave automata invoked before $i$. In consequence, we can construct a run of the value $-\infty$. Formally, we define condition (), which implies that there exists a run of value $-\infty$, as follows: () there exists a cycle $\mathcal{C}$ in the graph of $k$-configurations of $\mathbb{A}$ and a focus $Fc$ such that $\textsc{Gain}(\mathcal{C},Fc)<0$.

If the focused gain of every cycle is non-negative, we need to examine averages of cycles, while excluding some backward-walking slave automata. The average weight with restriction corresponds to the partial average of values aggregated over $\mathcal{C}$ by all slave automata invoked before position $j$ (which can be past $\mathcal{C}$). Backward-walking slave automata in the restriction correspond to automata invoked past $j$, and hence their values do not contribute to the partial average (up to $i$) (see Figure 2). In Example 15, we compute the average of slave automata over letters $b$, but we exclude the backward-walking slave automaton invoked at the following letter $c$. Observe that for any cycle $\mathcal{C}$ and any restriction $R$, having a run containing $\mathcal{C}$ occurring infinitely often, we can repeat each occurrence of cycle $\mathcal{C}$ sufficiently many times so that the partial average of values of slave automata up to position corresponding to $j$ becomes arbitrarily close to the average $\textsc{AvgE}(\mathcal{C},R)$. The resulting run contains a subsequence of partial averages convergent to $\textsc{AvgE}(\mathcal{C},R)$ and hence its value does not exceed $\textsc{AvgE}(\mathcal{C},R)$. We can now state our key technical lemma. This lemma is a direct extension of an intuition behind computing the infimum over values of all words of the NWA $\mathbb{A}$ from Example 15.

Lemma 16**.**

Let $\mathbb{A}$ be a $(\textsc{LimAvg};\textsc{Sum})$-automaton of bounded width with bidirectional slave automata. (1) If condition () holds, then $\mathbb{A}$ has a run of value $-\infty$. (2) If () does not hold, then the infimum $\inf_{w}\mathbb{A}(w)$ equals the infimum $\inf_{\mathcal{C}\in\Lambda,R}\textsc{AvgE}(\mathcal{C},R)$, where $\Lambda$ is the set of all cycles $\mathcal{C}$ in the graph of $k$-configurations of $\mathbb{A}$.

If the width of $\mathbb{A}$ is constant, then the graph of $k$-configurations has polynomial size in $|\mathbb{A}|$ and it can be constructed in polynomial time by employing reachability checks on the set of all $k$-configurations w.r.t. to relaxation of the successor relation. Therefore, for every focus $Fc$ and every $k$-configuration $c$ we can check in polynomial time whether there exists a cycle $\mathcal{C}$ such that $\mathcal{C}[1]=c$ and $\textsc{Gain}(\mathcal{C},Fc)<0$. Thus, condition (1) can be check in logarithmic space assuming that weights are given in unary. If weights are given in binary, condition (1) can be checked in polynomial time. Checking condition (2) has the same complexity as condition (1). If the width $k$ is given in unary in input, the graph of $k$-configurations is exponential in $|\mathbb{A}|$ and conditions (1) and (2) can be checked in polynomial space. Weights in this case are logarithmic in the size of the graph and hence changing representation from binary to unary does not affect the (asymptotic) size of the graph.

Theorem 17**.**

The emptiness problem for $(\textsc{LimAvg};\textsc{Sum})$-automaton of width $k$ with bidirectional slave automata is (a) NLogSpace-complete for constant $k$ and weights given in unary, (b) in PTime for constant $k$ and weights given in binary, and (c) PSpace-complete for $k$ given in unary.

7 Extensions

In this section we briefly discuss some extensions of the model of bidirectional NWA, i.e., we discuss the possibility of invoking multiple slave automata in one transition and two-way walking slave automata.

Invocation of multiple slave automata. The master automaton of an NWA invokes exactly one slave automaton at every transition. We can generalize the definition of NWA and allow the master automaton to invoke up to some constant $k$ slave automata at every transition. We call such a model $k$-NWA. First note that $k$-NWA contain NWA. Conversely, we briefly describe a reduction of the emptiness problem for $k$-NWA to the emptiness problem for NWA. First, observe that without loss of generality we can assume that $k$-NWA always invokes exactly $k$-slave automata as it can always invoke a dummy slave automaton, which immediately accepts. Invocation of such a slave automaton is equivalent to taking a silent transition. Next, given a $k$-NWA $\mathbb{A}$ with bidirectional slave automata over the alphabet $\Sigma$, we can construct an NWA $\mathbb{A}^{\prime}$ with bidirectional slave automata over the alphabet $\Sigma\cup\{\#\}$, which accepts words of the form $w[1]\#^{k-1}w[2]\#^{k-1}\ldots$. The runs of $\mathbb{A}^{\prime}$ on the word $w[1]\#^{k-1}w[2]\#^{k-1}w[3]\ldots$ correspond to all runs of $\mathbb{A}$ on $w$; the $\mathbb{A}^{\prime}$ invokes at letters $w[i]\#^{k-1}$ exactly $k$ slave automata which $\mathbb{A}$ invokes at the corresponding transition over letter $w[i]$. Observe that the emptiness problems for $\mathbb{A}$ and $\mathbb{A}^{\prime}$ coincide.

Two-way walking slave automata. For the ease of presentation we focus on bidirectional NWA where each slave automaton is either forward walking or backward walking. However, in general, we can allow slave automata that change direction while running, i.e., allow two-way slave automata and obtain the same complexity results. Observe that in case of two-way $\textsc{Sum}^{+}$-automata, we can assume that such an automaton does not visit the same position in the same state twice. Indeed, such a cycle can be eliminated without increase of the value of the run. Thus, without loss of generality we assume that every two-way slave automaton visits every position at most $|{\mathfrak{B}}|$ times. Therefore, instead of invoking a two-way slave $\textsc{Sum}^{+}$-automaton the master automaton invokes multiple forward-walking and backward walking slave automata, two automata, a forward walking ${\mathfrak{B}}_{f}$ and a backward walking ${\mathfrak{B}}_{b}$ such that ${\mathfrak{B}}_{f}$ (resp., ${\mathfrak{B}}_{b}$) simulates the run of ${\mathfrak{B}}$ past its invocation position (resp., before its invocation position). This reduction shows that every $(\textsc{LimAvg};\textsc{Sum}^{+})$-automaton $\mathbb{A}$ with two-way walking slave automata is equivalent to a $2$-NWA with bidirectional slave automata. This reduction however involves exponential blow-up as slave automata ${\mathfrak{B}}_{f},{\mathfrak{B}}_{b}$ can have exponential size in $\mathbb{A}$. This follows from the fact that due to reversals each visited position by ${\mathfrak{B}}$ can be visited $|{\mathfrak{B}}|$ times in different states. To simulate that in one run, ${\mathfrak{B}}_{f}$ and ${\mathfrak{B}}_{b}$ have to simulate $|{\mathfrak{B}}|$ instances of ${\mathfrak{B}}$ in different states. This exponential blow-up can be avoided by dividing ${\mathfrak{B}}_{f},{\mathfrak{B}}_{b}$ into multiple slave automata, each of which tracks only one loop in the run of ${\mathfrak{B}}$ as shown in Figure 3 with automata ${\mathfrak{B}}_{1},\ldots,{\mathfrak{B}}_{4}$. Each of these automata have to track at most two instances of ${\mathfrak{B}}$ and hence it involves only quadratic blow-up. The resulting automaton is an $|\mathbb{A}|$-NWA as up to $\frac{|{\mathfrak{B}}|}{2}$ slave automata have to be invoked at every position. Still, the emptiness problems for $|\mathbb{A}|$-NWA and for NWA have the same complexity and hence we conclude that allowing two-way slave automata does not increase the emptiness problem for $(\textsc{LimAvg};\textsc{Sum}^{+})$-automata.

8 Discussion and Conclusion

Discussion. We established decidability of the emptiness problem for classes of bidirectional NWA, which include all NWA presented in the examples. An NWA from Example 2 is covered by Theorem 6, while NWA from Examples 1, 3 and 4 are covered by Theorem 11. The lower bounds in the presented theorems follow from the lower bounds of the special case of forward-only NWA. The established complexity bounds (Table 1) coincide with the bounds for forward-only NWA.

Concluding remarks. In this work we present bidirectional NWA as a specification formalism for quantitative properties. In this formalism many natural quantitative properties can be expressed, and we present decidability and complexity results for the basic decision problems. There are several interesting directions for future work. The study of bidirectional NWA with other value functions is an interesting direction. The second direction of future work is to consider other formalism (such as a logical framework) which has the same expressive power as bidirectional NWA.

Acknowledgements.

This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23,S11407-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), ERC Start grant (279307: Graph Games), Vienna Science and Technology Fund (WWTF) through project ICT15-003 and by the National Science Centre (NCN), Poland under grant 2014/15/D/ST6/04543.

Appendix

In the appendix we recall statements of theorems and lemmas from the main body of the paper keeping their original numbering. Lemmas introduced in the appendix have subsequent numbers. For this reason, the numbering of theorem and lemmas in the appendix is mixed.

Appendix A Proofs from Section 4

See 6

The PSpace-hardness part follows from PSpace-hardness of the emptiness problem for $(\textsc{LimAvg};g)$-automata with forward-walking slave automata only [13]. Therefore, we focus on the containment in PSpace. We begin with a definition of a unifying framework of regular value functions.

Regular weighted automata and regular value functions. Following [13], we say that a weighted automaton ${\cal A}$ over finite words is a regular weighted automaton if and only if there is a finite set of rationals $\{q_{1},\ldots,q_{n}\}$ and there are regular languages ${{\cal L}}_{1},\ldots,{{\cal L}}_{n}$ such that

1. (i)

every word accepted by ${\cal A}$ belongs to $\bigcup_{1\leq i\leq n}{{\cal L}}_{i}$, and 2. (ii)

for every $w\in{{\cal L}}_{i}$, its value w.r.t. ${\cal A}$ is $q_{i}$.

A value function $f$ is a regular value function if and only if all $f$-automata are regular weighted automata. Examples of regular value functions are $\textsc{Min},\textsc{Max}$ and variants of the bounded sum $\textsc{Sum}^{L,U}$ with regular conditions, i.e., the partial sum of every prefix, suffix, infix of the run belongs to interval $L,U$, e.t.c. Having the definition of regular value function, we can easily check whether our variant of the bounded sum is admissible.

We define the description size of a given regular weighted automaton ${\cal A}$, as the size of automata ${\cal A}_{1},\ldots,{\cal A}_{n}$ recognizing languages ${{\cal L}}_{1},\ldots,{{\cal L}}_{n}$ that witness ${\cal A}$ being a regular weighted automaton.

Lemma 18**.**

Let $g$ be a regular value function. Every $(\textsc{LimAvg};g)$-automaton $\mathbb{A}$ with bidirectional slave automata is equivalent to an exponential-size LimAvg-automaton ${\cal A}$. The automaton ${\cal A}$ can be constructed implicitly in polynomial time.

Since the emptiness problem for LimAvg-automata can be solved in NLogSpace, Lemma 18 implies Theorem 6. Moreover, Remark 7 follows directly from the construction in the following proof.

Proof.

Let $Q_{m}$ be the set of states of the master automaton of $\mathbb{A}$. Since $g$ is a regular value function, every slave automaton ${\mathfrak{B}}$ has a finite range $R_{{\mathfrak{B}}}$ and for each value $v\in R_{{\mathfrak{B}}}$ there exists a finite-state automaton ${\cal A}_{{\mathfrak{B}},v}$ recognizing the set of words of value $v$. Let $Q_{SF}$ (resp., $Q_{SB}$) be the union of the sets of states of all automata ${\cal A}_{{\mathfrak{B}},v}$, where ${\mathfrak{B}}$ if a forward-walking (resp., backward-walking) slave automaton and $v\in R_{{\mathfrak{B}}}$. We assume that sets of states of automata ${\cal A}_{{\mathfrak{B}},v}$ are disjoint.

We define a LimAvg-automaton ${\cal A}$ with generalized Büchi condition as follows. The set of states of ${\cal A}$ is $Q_{m}\times 2^{Q_{SF}}\times 2^{Q_{SF}}\times 2^{Q_{SB}}$. States of ${\cal A}$ are of the form $(q,F_{1},F_{2},B)$, whose objectives are as follows.

Component $q$ is used to simulate the run of the master automaton. Components $F_{1},F_{2}$ are used to simulate finite-state automata corresponding to forward-walking slave automata. Accepting states correspond to termination of a slave automaton and hence they are removed from $F_{1},F_{2}$. Every newly invoked forward-walking slave automaton is added to component $F_{2}$, i.e., automaton ${\cal A}$ picks a transition invoking slave automaton ${\mathfrak{B}}$ and picks weight of this transition $v$, then it adds to $F_{2}$ an initial state of finite-state automaton ${\cal A}_{{\mathfrak{B}},v}$. The weight of such a transition is $v$,

If every slave automaton has finite run than $F_{1}$ becomes empty at some point of time. Then, we move all states from $F_{2}$ to $F_{1}$, and put $F_{2}=\emptyset$. Observe that runs of all forward-walking slave automaton are finite if and only if $F_{1}$ is empty infinitely often.

Component $B$ is used to simulate finite-state automata corresponding to backward-walking slave automata. Accepting states of backward-walking slave automata correspond to their termination. Since ${\cal A}$ moves in the opposite direction w.r.t. $\mathbb{A}$, the automaton ${\cal A}$ adds to component $B$ some subset of accepting states from $Q_{SB}$. There is only one position in the run of ${\cal A}$ at which it adds states to $B$. Whenever a backward-walking slave automaton is invoked in a state $q_{i}$, we require that $q_{i}$ belongs to $B$. This state $q_{i}$ may be removed from the corresponding set but does not have to. Removal corresponds to a situation when only a single slave automaton is in the state $q_{i}$, while leaving $q_{i}$ in $B$ corresponds the situation when more than one slave automaton is in state $q_{i}$.

Due to the construction we have (i) for every run of $\mathbb{A}$, the automaton ${\cal A}$ has a run of the same weight, and conversely (ii) for every run of ${\cal A}$, there exists a run $\mathbb{A}$ of the same value. ∎

Appendix B Proofs from Section 5

B.1 The proof of Theorem 10

See 10

Proof.

Let $Q_{slv}^{F}$ (resp., $Q_{slv}^{B}$) be the set of states of forward-walking (resp., backward-walking) slave automata of $\mathbb{A}$ and let $Q_{m}$ be the set of states of the master automaton of $\mathbb{A}$. We define a (generalized) Büchi-automaton (with no weights) ${\cal A}$ as follows. The set of states of ${\cal A}$ is $Q_{m}\times 2^{Q_{slv}^{F}}\times 2^{Q_{slv}^{F}}\times 2^{Q_{slv}^{B}}\times 2^{Q_{slv}^{B}}$. Initially ${\cal A}$ starts with $(q,\emptyset,\emptyset,\emptyset,\emptyset)$, where $q$ is some initial state of the master automaton. We use sets of states to simulate runs of slave automata and to ensure that every forward-walking slave automaton runs for finitely many steps. We treat backward-walking slave automata in a similar way to forward-walking slave automata except that backward-walking slave automata are started at the termination step of the corresponding slave automata, and they can terminate (which correspond to invocation) multiple, but finitely many times. More precisely, states of ${\cal A}$ are of the form $(q,F_{1},F_{2},B_{1},B_{2})$, whose objectives are as follows.

Component $q$ is used to simulate the run of the master automaton. Components $F_{1},F_{2}$ are used to simulate forward-walking slave automata. Accepting states correspond to termination of a slave automaton and hence they are removed from $F_{1},F_{2}$. A newly invoked forward-walking slave automaton is added to component $F_{2}$. Thus, if every slave automaton has finite run than $F_{1}$ becomes empty at some point of time. Then, we move all states from $F_{2}$ to $F_{1}$, and put $F_{2}=\emptyset$. Observe that runs of all forward-walking slave automaton are finite if and only if $F_{1}$ is empty infinitely often.

Components $B_{1},B_{2}$ are used to simulate backward-walking slave automata. Component $B_{1}$ contains the states of slave automata that all finish at the same position, while $B_{2}$ contains states of other slave automata. We require that $B_{1}$ and $B_{2}$ are disjoint at every position. Accepting states of backward-walking slave automata correspond to their termination. However, as the simulating automaton ${\cal A}$ moves in the opposite direction, it guesses at every step whether some (backward-walking) slave automaton have been terminated at the current position and it may add some accepting states to $B_{1}$ or $B_{2}$. There is only one position in the run of ${\cal A}$ at which it adds states to $B_{1}$. Whenever a backward-walking slave automaton is invoked in a state $q_{i}$, we require that $q_{i}$ belongs to $B_{1}$ or $B_{2}$. This state $q_{i}$ may be removed from the corresponding set but does not have to. Removal corresponds to a situation when only a single slave automaton is in the state $q_{i}$, while leaving $q_{i}$ in $B_{1}$ or $B_{2}$ corresponds the situation when more than one slave automaton is in state $q_{i}$.

Consider an infinite run $\pi$ of ${\cal A}$, in which (a) component $q$ equals infinitely often to some accepting state of the master automaton, (b) component $F_{1}$ is empty infinitely often, and (c) component $B_{1}$ is never empty and infinitely often contains an initial state of the slave automaton invoked at the current position. The run $\pi$ corresponds to an accepting run of $\mathbb{A}$ in which infinitely many backward-walking slave automata terminate at the same position (which is the position at which $B_{1}$ becomes non-empty for the first time). Conversely, having a run of $\mathbb{A}$ of infinite width, the corresponding run of ${\cal A}$ satisfies (a), (b) and (c). Checking existence of a run of ${\cal A}$ satisfying (a), (b) and (c) can be done in non-deterministic logarithmic space. Thus, checking whether $\mathbb{A}$ has infinite width can be done in polynomial space.

We show PSpace-hardness of checking finite-width, by reduction from the emptiness problem for NWA with forward-walking slave automata only, which is PSpace-complete [13]. Let $\mathbb{A}$ be an NWA with forward-walking slave automata only over the alphabet $\Sigma$. We extend the alphabet $\Sigma$ by \,#$. Next, we construct an NWA$\mathbb{A}^{\prime}$whose every run has infinite width and which accepts precisely words of the form$$w[1]#w[2]#$such that$\mathbb{A}$accepts$w[1]w[2]\ldots$. Basically, forward-walking slave automata of$\mathbb{A}$ignore letters$#$and every transition$(q,a,q^{\prime})$of the master automaton of$\mathbb{A}$is replaced with two transitions$(q,a,q^{\prime}{#})$and$(q^{\prime}{#},#,q^{\prime})$. On the first transition,$\mathbb{A}^{\prime}$invokes the same automaton as$\mathbb{A}$and on transitions labeled by$#$, the automaton$\mathbb{A}^{\prime}$invokes a backward-walking slave automaton that runs until$$$. Now, if$\mathbb{A}$does not have an accepting run,$\mathbb{A}^{\prime}$does not have an accepting run and it has trivially finite width. Otherwise, if$\mathbb{A}$accepts$w$, the automaton$\mathbb{A}^{\prime}$accepts$$w[1]#w[2]#$and it has a run of infinite width on it. Therefore,$\mathbb{A}$has an accepting run if and only if$\mathbb{A}^{\prime}$ does not have finite width.

∎

B.2 The proof of Theorem 11

See 11

The PSpace-hardness part follows from PSpace-hardness of the emptiness problem for $(\textsc{LimAvg};\textsc{Sum}^{+})$-automata with forward-walking slave automata only [13]. Therefore, we focus on the containment in ExpSpace.

Overview. The proof is by reduction to the bounded-width case, which is decidable due to Theorem 17. First, we show that without loss of generality we can assume that a given NWA $\mathbb{A}$ is deterministic (Lemma 19). Next, we define words, called barriers, upon which all active (backward- and forward-walking) slave automata terminate. We show that for finite-width NWA such words do exist (Lemma 21). Properties of barriers ensure that if as some position $i$ in the input word, exponentially many slave automata accumulate exponential values, then inserting a barrier actually decreases the partials sum of values returned by slave automata (Lemma 22), and hence we can insert barriers even at infinitely many positions and the value of the resulting word does not exceed the value of the original word. Thanks to barriers, we can show that for every word $w$, there exists a word $w^{\prime}$ such that at every position at most exponentially many slave automata aggregate exponential values and the value of $w^{\prime}$ does not exceed the value of $w$. Slave automata which aggregate bounded (exponential) values can be eliminated, i.e., we construct an NWA $\mathbb{A}^{\prime}$ which simulates $\mathbb{A}^{\prime}$ in such a way that runs of slave automata that accumulate at most exponential values are compressed into a single transition. Observe that $\mathbb{A}^{\prime}$ on word $w^{\prime}$ as above has exponential width. Hence, the infimum of $\mathbb{A}$ over all words coincides with the infimum of $\mathbb{A}^{\prime}$ over words on which it has a run of exponential width. We can encode the bound on width into $\mathbb{A}^{\prime}$ and decide the emptiness problem of $\mathbb{A}^{\prime}$ in non-deterministic logarithmic space (Theorem 17). The size of $\mathbb{A}^{\prime}$ is doubly-exponentially bounded in the size of $\mathbb{A}$, and hence the emptiness problem for finite-width $(\textsc{LimAvg};\textsc{Sum}^{+})$-automata with bidirectional slave automata is in ExpSpace.

Configuration and multiplicities. Invocation of a slave automaton in an NWA is a form of a universal transition in the sense of alternating automata. We adapt the power-set construction, which is used to convert alternating automata to non-deterministic automata, to the NWA case. Given a (non-deterministic) NWA $\mathbb{A}$ with bidirectional slave automata, we define configurations and multiplicities of $\mathbb{A}$ as follows. Let $Q_{\textrm{slv}}$ be the disjoint union of the sets of states of all slave automata of $\mathbb{A}$. For a run of $\mathbb{A}$, we say that $(q_{m},A)$ is the configuration at position $p$ if $q_{m}$ is the state of the master automaton at position $p$ and $A\subseteq Q_{\textrm{slv}}$ is the set of states of slave automata at position $p$. We denote by $\mathsf{conf}({\mathbb{A}})$ the number of configurations of $\mathbb{A}$. We define the multiplicity ${\mathsf{mult}}$ at position $p$ as the function ${\mathsf{mult}}:Q_{\textrm{slv}}\mapsto\mathbb{N}$, such that ${\mathsf{mult}}(q)$ specifies the number of slave automata in the state $q$ at position $p$. The configuration together with the multiplicity give a complete description of the state of $\mathbb{A}$ at position $p$.

We observe that without loss of generality we can assume that NWA are deterministic. Basically, non-deterministic choices of the master automaton and slave automata can be encoded in the input alphabet. More precisely, the proof consists of two steps. First, we define simple runs as follows. A run of an NWA is simple if at every position in the run slave automata that are in the same state take the same transition. We show that (i) for every run $(\Pi,\pi_{1},\pi_{2},\dots)$ of $\mathbb{A}$ there exists a simple run of $\mathbb{A}$ of the value not exceeding the value of $(\Pi,\pi_{1},\pi_{2},\dots)$. Second, we show that (ii) there exists a deterministic $(\textsc{LimAvg};\textsc{Sum}^{+})$-automaton $\mathbb{A}^{\prime}$ over an extended alphabet such that the sets of accepting simple runs of $\mathbb{A}$ and accepting runs of $\mathbb{A}^{\prime}$ coincide and each run has the same value in both automata.

The proof of the following lemma is virtually the same as in the case of NWA with forward-walking slave automata only [13].

Lemma 19**.**

Given a $(\textsc{LimAvg};\textsc{Sum}^{+})$-automaton $\mathbb{A}$ over $\Sigma$ with bidirectional slave automata, (i) for every run of $\mathbb{A}$, there exists a simple run of at most the same value, and (ii) one can compute in polynomial space a deterministic $(\textsc{LimAvg};\textsc{Sum}^{+})$-automaton $\mathbb{A}^{\prime}$ over an alphabet $\Sigma\times\Gamma$ such that: (1) $\inf_{w\in\Sigma^{+}}{\cal L}_{{{\cal A}}}(w)=\inf_{w^{\prime}\in(\Sigma\times\Gamma)^{+}}{\cal L}_{{{\cal A}^{\prime}}}(w^{\prime})$, and (2) $\mathsf{conf}({\mathbb{A}})=\mathsf{conf}({\mathbb{A}^{\prime}})$.

Proof.

(i): Consider a run $(\Pi,\pi_{1},\pi_{2},\dots)$ of $\mathbb{A}$. Suppose that $\pi_{i},\pi_{j}$ are runs of the same slave automaton ${\mathfrak{B}}$ invoked at positions $i$ and $j$, such that its both instances are in the same state at position $s$ in the word, i.e., $\pi_{i}[i^{\prime}]=\pi_{j}[j^{\prime}]$, where $i^{\prime},j^{\prime}$ are the positions in $\pi_{i},\pi_{j}$ corresponding to the position $s$ in $w$. We pick from the suffixes $\pi_{i}[i^{\prime},|\pi_{i}|],\pi_{j}[j^{\prime},|\pi_{j}|]$ the one with the smaller sum, and in case of the equal sum we pick the shorter. Then, we change the suffixes of both runs to the picked one. Such a transformation does not increase the value of the partial sums and does not introduce infinite runs of slave automata. Indeed, a run of each slave automaton can be changed by such an operation only finitely many times. Thus, this transformation can be applied to any pair of slave runs to obtain a simple run of the value not exceeding the value of $(\Pi,\pi_{1},\pi_{2},\dots)$.

(ii): Without loss of generality, we can assume that for every slave automaton in $\mathbb{A}$ final states have no outgoing transitions. Let $Q_{\textrm{all}}$ be the disjoint union of the sets of states of the master automaton and all slave automata of $\mathbb{A}$. We define $\Gamma$ as the set of all partial functions $h:Q_{\textrm{all}}\mapsto Q_{\textrm{all}}$. We define a $(\textsc{LimAvg};\textsc{Sum}^{+})$-automaton $\mathbb{A}^{\prime}$ over the alphabet $\Sigma\times\Gamma$ by modifying only the transition relations and labeling functions of the master automaton and slave automata of $\mathbb{A}$; the sets of states and accepting states are the same as in the original automata. The transition relation and the labeling function of the master automaton ${\cal A}_{mas}^{\prime}$ of $\mathbb{A}^{\prime}$ are defined as follows: $(q,\langle{a},{h}\rangle,q^{\prime})$ is a transition of ${\cal A}_{mas}^{\prime}$ if and only if $h(q)=q^{\prime}$ and ${\cal A}_{mas}$ has the transition $(q,a,q^{\prime})$. The label of the transition $(q,\langle{a},{h}\rangle,q^{\prime})$ is the same as the label of the transition $(q,a,q^{\prime})$ in ${\cal A}_{mas}$. Similarly, for each slave automaton ${\mathfrak{B}}_{i}$ in $\mathbb{A}$, the transition relation and the labeling function of the corresponding slave automaton ${\mathfrak{B}}_{i}^{\prime}$ in $\mathbb{A}^{\prime}$ are defined as follows: $(q,\langle{a},{h}\rangle,q^{\prime})$ is a transition of ${\mathfrak{B}}_{i}^{\prime}$ if and only if $h(q)=q^{\prime}$ and ${\mathfrak{B}}_{i}$ has the transition $(q,a,q^{\prime})$. The label of the transition $(q,\langle{a},{h}\rangle,q^{\prime})$ is the same as the label of the transition $(q,a,q^{\prime})$ in ${\mathfrak{B}}_{i}$.

First, we see that $\mathsf{conf}({\mathbb{A}})=\mathsf{conf}({\mathbb{A}^{\prime}})$. Second, observe that the master automaton ${\cal A}_{mas}^{\prime}$ and all slave automata ${\mathfrak{B}}_{i}^{\prime}$ are deterministic. Moreover, since we assumed that for every slave automaton in $\mathbb{A}$ final states have no outgoing transitions, slave automata ${\mathfrak{B}}_{i}^{\prime}$ recognize prefix free languages. Finally, it follows from the construction that (i) every simple run $(\Pi,\pi_{1},\pi_{2},\dots)$ of $\mathbb{A}$ is a run of $\mathbb{A}^{\prime}$ of the same value. Basically, we encode in the input word all transitions in functions $h\in\Gamma$. The value of each transition is the same by the construction. Conversely, (ii) every run $(\Pi,\pi_{1},\pi_{2},\dots)$ of $\mathbb{A}^{\prime}$ is a simple run of $\mathbb{A}$ of the same value. Indeed, the fact that transitions are directed by functions $h\in\Gamma$ implies that the run is simple. ∎

In the following definition we introduce barriers, which are words on which all active slave automata terminate, i.e., if $u$ is a barrier, then forward-walking slave automata terminate while reading $u$, and backward-walking slave automata terminate while reading $u^{R}$ (word $u$ from right to left). Barriers have additional properties, which allow us tho show that if exponentially many slave automata accumulate exponential values, then inserting a barrier decreases multiplicities of slave automata and does not increase the partial sums of values returned by slave automata.

Definition 20** (Barriers).**

Let $w$ be an infinite word, $i$ be a position and $k>i$ be the first position such that all backward-walking slave automata invoked past $k$ terminate past $i$. A finite word $u$ is a barrier at $i$ in $w$ if in word $w^{\prime}=w[1,i]uw[i+1,\infty]$ we have

1. BC1

backward-walking slave automata invoked past position $i+|u|$ terminate past position $i$ (between positions $i+1$ and $i+|u|$) 2. BC2

forward-walking slave automata invoked before position $i$ terminate before position $i+|u|$, 3. BC3

the configurations at $i$ and $i+|u|$ in $w^{\prime}$ are the same as the one at $i$ in $w$, 4. BC4

the length of $u$ is bounded by $\mathbf{N}=(|Q_{s}+2|)\cdot\mathsf{conf}({\mathbb{A}})\cdot|Q_{s}|^{2\cdot|Q_{s}|}$, 5. BC5

for every state $q$ of some backward-walking (resp., forward-walking) slave automaton, the multiplicity $mult(q)$ at $i$ in $w^{\prime}$ (resp., ${\mathsf{mult}}(q)$ at $i+|u|$ in $w^{\prime}$) is bounded by $mult(q)$ at $i$ in $w$, and 6. BC6

every backward-walking (resp., forward-walking) slave automaton active at position $i$, accumulates over $w[1,i]$ (resp., $w[i,\infty]$) a value greater or equal to the value accumulated over $w[1,i]u$ (resp., $uw[i+1,\infty]$).

The above conditions simply state that a barrier terminates all slave automata active and reduces their multiplicities, i.e., the multiplicity of backward-walking slave automata, which are invoked in the suffix $w[i+1,\infty]$ is reduced by word $u$ (BC1) and the multiplicity of forward-walking slave automata invoked in prefix $w[1,i]$ is reduced by word $u$ (BC2). Property BC3 ensures that inserting a barrier at position $i$ does not change the run essentially (except for $u$ it only reduces the multiplicities of slave automata). These properties and the bound on the length of barriers (BC4) allow us to reduce the multiplicity of slave automata along words. Properties BC5, BC6 are necessary to show that such a reduction of multiplicities does not increase the values of words.

Lemma 21**.**

Let $\mathbb{A}$ be a deterministic $(\textsc{LimAvg};\textsc{Sum}^{+})$-automaton of finite width with bidirectional slave automata. Then, for every word $w$, at almost every position a barrier exists.

Proof.

Let $w$ be a word. We consider the unique run of $\mathbb{A}$ on $w$ and refer to the positions in $w$ and the corresponding positions in the run, i.e., we refer to “the configuration at $i$ in $w$” as the unique configuration of $\mathbb{A}$ at $i$ while processing word $w$.

We define the profile at position $j$ in $w$ as a pair of the configuration at $j$ and multiplicities at $j$ bounded by $\mathbf{N}$, defined for every $q\in Q_{s}$ as $min({\mathsf{mult}}(q),\mathbf{N})$. Let $c_{0}<c_{1}$ positions in $w$ such that every profile that occurs infinitely often in $w$ occurs between $c_{0}$ and $c_{1}$. Next, we define $c_{2}$ as the minimal position past $c_{1}$ such that every backward-walking slave automaton invoked past $c_{2}$ terminates at some position past $c_{1}$, i.e., any backward-walking slave automaton invoked past $c_{2}$ terminates before it reaches $c_{1}$. The NWA $\mathbb{A}$ has finite width and hence such $c_{2}$ exists. We show that there exists a barrier in $w$ for every position $i>c_{2}$.

Construction of a barrier $u$ at position $i$. Let $i>c_{2}$. We pick positions $a<i<b$ such that all slave automata active at $i$ terminate within $w[a,b]$ and the profiles at positions $a,i,b$ and letters in $w$ are the same. Since $i>c_{2}>c_{1}>c_{0}$ such $a,b$ exist. Observe that $w[a,b]$ satisfies first three conditions of the barrier definition, but it does not have to satisfy the remaining conditions. Consider word $w[b,i]w[a+1,i]$. It satisfies all barrier conditions except for BC4. We take $w[b,i]w[a+1,i]$ and transform it into a barrier $u$ by removing certain subwords corresponding to cycles in $\mathbb{A}$, i.e., subwords such that at the beginning and at the end of this subword $\mathbb{A}$ is in the same configuration. Removal of such subwords does not change runs of the master automaton or slave automata in the suffix of the word. However, to show condition RC5 we need to ensure that the removal operation does not change the profile, i.e., the profiles at positions $i$ and $i+|u|$ in $w[1,i]uw[i+1,\infty]$ are the same as the profile at $i$ in $w$.

We define an extended configuration in a finite word $x$ at position $p$ as the pair of the configuration at $p$ and the equivalence relation $R_{p}$ on states of slave automata active at position $p$ such that $q_{1}R_{p}q_{2}$ if and only if either

• •

$q_{1},q_{2}$ are states of forward-walking slave automata and slave automata in states $q_{1}$ and $q_{2}$ at position $p$ reach the same state at the end of word $x$, or

• •

$q_{1},q_{2}$ are states of backward-walking slave automata and slave automata in states $q_{1}$ and $q_{2}$ at position $p$ reach the same state at the beginning of word $x$.

The slave automata that do not reach the end o word $x$ (resp., the beginning of $x$) are in the same equivalence class $\emptyset$. Given two positions $p<p^{\prime}$ in $x$ with the same extended configuration, we define transformation from $p$ to $p^{\prime}$ as a function from the set of equivalence classes of $R_{p}$ (which is equal $R_{p^{\prime}}$) into itself such that

• •

for a state $q$ of a forward-walking slave automaton, the equivalence class $[q]$ is transformed into a class $[q^{\prime}]$ if some slave automaton in state $q$ at position $p$ reaches state from $[q^{\prime}]$ at position $p^{\prime}$, and

• •

for a state $q$ of a backward-walking slave automaton, the equivalence class $[q]$ is transformed into a class $[q^{\prime}]$ if some slave automaton in state $q^{\prime}$ at position $p^{\prime}$ reaches state from $[q]$ at position $p$.

Due to determinicity of $\mathbb{A}$, the transformation is, indeed, a function and a permutation.

Now we describe the subword removal process. First, we mark positions $j_{1},\ldots,j_{n}$ in $w$ at which each of slave automata active at position $i$ in $w$ terminates. Observe that these belong to the interval $[a,b]$. Now, starting with word $w[b,i]w[a+1,i]$ we iteratively remove subwords $y$ such that (a) the extended configurations at the first and the last position of $y$ are the same, (b) the transformation between these positions is the identity, and (c) $y$ does not contain any position corresponding to positions $\{j_{1},\ldots,j_{n}\}$. The last word, from which no such a subword can be removed is $u$. We show that $u$ is a barrier.

Word $u$ is a barrier. The positions at which slave automata are terminated are not removed from $w[a,b]$ and hence $u$ satisfies conditions BC1, BC2. Removal of a word satisfying (a) and (b) preserves profile at every step and hence condition BC3 holds for $u$.

Condition BC4 follows from the fact that there are at most $\mathsf{conf}({\mathbb{A}})\cdot|Q_{s}|^{|Q_{s}|}$ different extended configurations. Transformations are permutations of equivalence classes, i.e., they are permutations of sets of size at most $|Q_{s}|$. Therefore, if $k>|Q_{s}|^{|Q_{s}|}$, then among positions $p_{1}<\ldots<p_{k}$ with the same extended configuration there exists a pair such that the transformation between these positions is the identity. Thus, words of length at least $\mathsf{conf}({\mathbb{A}})\cdot|Q_{s}|^{2\cdot|Q_{s}|}$ contain a subword $y$ satisfying (a) and (b). Furthermore, words of length at least $(|Q_{s}+2|)\cdot\mathsf{conf}({\mathbb{A}})\cdot|Q_{s}|^{2\cdot|Q_{s}|}={\mathbf{N}}$, contain a subword $y$ satisfying (a), (b) and (c). Therefore, the length of $v$ is bounded by ${\mathbf{N}}$.

We show that $u$ satisfies BC5. Let $q$ be a state of some slave automaton and let $mult_{1}(q)$ be the multiplicity of $q$ in $w$ at position $i$ and $mult_{2}(q),mult_{3}(q)$ be multiplicities of $q$ in $w[1,i]uw[i+1,\infty]$ at positions $i$ and $i+|u|$ respectively. Observe that (a) and (b) imply the the profiles at positions $i$ and $i+|u|$ in $w[1,i]uw[i+1,\infty]$ are the same as the profile at $i$ in $w$. It follows that $min(mult_{1}(q),N)=min(mult_{2}(q),N)=min(mult_{3}(q),N)$. Now, if $q$ is a state of a backward-walking slave automaton, then all such automata active at position $i$ in $w[1,i]uw[i+1,\infty]$ have been invoked in $v$ and hence $mult_{2}(q)<|u|\leq{\mathbf{N}}$. It follows that $mult_{2}(q)\leq mult_{1}(q)$. Otherwise, similarly if $q$ is a state of a forward-walking slave automaton we have $mult_{3}(q)<N$ and $mult_{3}(q)\leq mult_{1}(q)$. Therefore, condition BC5 holds.

Finally, word $u$ satisfies condition BC6. Consider a backward-walking slave automaton ${\mathfrak{B}}$ active at position $i$ in $w$. This automaton terminates before position $a$ and hence it accumulates equal values on subwords $w[a,i]$ and $w[1,i]w[b,i]w[a+1,i]$. Now, word $u$ results from $w[b,i]w[a+1,i]$ by deletion of certain subwords, while it preserves positions corresponding to termination of slave automata. Moreover, the deletion process only shortens runs; the transitions taken by slave automata correspond to the transitions in the original run. Thus, ${\mathfrak{B}}$ accumulates over $w[1,i]u$ a value smaller or equal to the value accumulated over $w[1,i]w[b,i]w[a+1,i]$. The case of forward-walking slave automata is symmetric. ∎

Now, we show the key property of barriers, i.e., they decrease the partial sum of values if inserted at a position where exponentially many slave automata accumulate exponential values. This enables us to reduce the emptiness problem for finite-width NWA to the bounded-width case.

Lemma 22**.**

Let $\mathbb{A}$ be a deterministic $(\textsc{LimAvg};\textsc{Sum}^{+})$-automaton with bidirectional slave automata. Let $C$ be the maximal weight of slave automata of $\mathbb{A}$. Let $w$ be a word and let $u$ be a barrier for $w$ at position $i$. If more than $2\cdot|\mathbb{A}|\cdot\mathbf{N}$ slave automata accumulate the value exceeding $4\cdot C\cdot\mathbf{N}$ past $i$ in $w$ (i.e, for backward-walking slave automata it is at $w[1,i]$), then for almost all $K$, the sum of values returned by slave automata invoked up to $k$ in $w$ is greater than the sum of values of returned by slave automata invoked up to $k+|u|$ in $w[1,i]uw[i+1,\infty]$.

Proof.

Let $k$ be the first position past $i$ such that all backward-walking slave automata invoked past $k$ terminate before position $i$. We show that the partial sum of values returned by slave automata invoked up to $k$ in $w$ is greater than the partial sum of values of returned by slave automata invoked up to $k+|u|$ in $w[1,i]uw[i+1,\infty]$. This argument works for every $k_{0}\geq k$. The partial sum of values returned by slave automata invoked up to $k$ in $w$ consists of the sum of weights: (1) accumulated by slave automata before they reach position $i$, and (2) accumulated by slave automata after they reach position $i$. In (1) we include values of backward-walking (resp., forward-walking) slave automata that do not reach position $i$. Let $A$ be the set of states of slave automata active at position $i$ in $w$. For $q\in A$, we define ${\mathsf{mult}}(q)$ (resp., $val(q)$) as the multiplicity at $i$ (resp., the value accumulated past $i$) in $w$ by slave automata that are in the state $q$ at $i$. Observe that (2) = $\sum_{q\in A}mult(q)\cdot val(q)$.

The partial sum of values returned by slave automata invoked up to $k+|u|$ in $w$ consists of four components, which are the sum of weights (1’) aggregated by slave automata before they reach any of positions $i,\ldots i+|u|$, (2’a) aggregated over positions $i,\ldots i+|u|$ by backward-walking slave automata invoked past $i+|u|$ and forward-walking slave automata invoked before $i$, (2’b) aggregated past positions $i,\ldots i+|u|$ by slave automata invoked on positions $i,\ldots i+|u|$, i.e., the values aggregated by backward-walking slave automata over $w^{\prime}[1,i]=w[1,i]$ and forward-walking slave automata over $w^{\prime}[i+|u|+1,\infty]=w[i+1,\infty]$, and (2’c) aggregated over positions $i,\ldots i+|u|$ by slave automata invoked on positions $i,\ldots i+|u|$.

We observe that (1)$=$(1’) and we show that (2) $>$ (2’a)+(2’b)+(2’c). Observe that (2’c) is bounded by $C\cdot|u|^{2}$. In (2’a), the multiplicities of slave automata are the same as the multiplicities of the corresponding slave automata active at $i$ in $w$ while the values they accumulate are bounded by the minimum of the values accumulated within $w$ and $C\cdot|u|$. Indeed, consider a backward-walking slave automaton, which is in state $q$ at position $i+|u|$ in $w^{\prime}$. The multiplicity of such automata is equal to the multiplicity of slave automata that are in state $q$ at position $i$ in $w$. Moreover, due to condition BC6 satisfied by $u$, the value which such an automaton accumulates along $w^{\prime}[1,i+|u|]$ is bounded by the value it accumulates at $w[1,i]$. Also, such an automaton terminates within $|u|$ and hence its value is bounded by $C\cdot|u|$ as well. The similar reasoning holds for forward-walking slave automata active at position $i$ in $w^{\prime}$ and hence (2’a) is bounded by $\sum_{a\in A}{\mathsf{mult}}(q)\min(C\cdot|u|,val(q))$. In (2’b), slave automata accumulate the same values as the corresponding slave automata in $w$, but multiplicities are bounded by $|u|$ and the values of the corresponding slave automata at position $i$ in $w$. Indeed, consider a backward-walking slave automaton, which is in state $q$ at position $i$ in $w^{\prime}$. Since the profile at $i$ in $w$ and $w^{\prime}$ is the same, the multiplicity ${\mathsf{mult}}^{\prime}(q)$ of such automata is bounded by the multiplicity of slave automata that are in state $q$ at position $i$ in $w$. Moreover, all backward-walking slave automata active at position $i$ in $w^{\prime}$ have been invoked within positions $i,\ldots,i+|u|$ and hence the sum of their multiplicities is bounded by $|u|$. Since $w[1,i]=w^{\prime}[1,i]$, a backward-walking slave automaton in state $q$ at position $i$ in $w^{\prime}$ accumulates value $val(q)$ at past position $i$, i.e, the value which accumulates the same automaton in $w$. Similar estimates hold for forward-walking slave automata past position $i+|u|$. Therefore, (2’b) is bounded by $\sum_{q\in A}mult^{\prime}(q)val(q)$, where $\sum_{q\in A}mult^{\prime}(q)\leq|u|$. Due to condition BC5 of barriers, for every $q\in A$ we have ${\mathsf{mult}}^{\prime}(q)\leq mult(q)$. Now, we estimate $(2)-(2^{\prime}a)-(2^{\prime}b)-(2^{\prime}c)$, which equals $\sum_{q\in A}({\mathsf{mult}}(q)\cdot(val(q)-\min(C\cdot|u|,val(q)))-\sum_{q\in A}mult^{\prime}(q)val(q))-C\cdot|u|^{2}$. We partition $A$ into $A_{1}$, the states of slave automata at position $i$, which accumulate the value at least $4\cdot C\cdot\mathbf{N}$ past position $i$ in $w$, and $A_{2}$ the reaming states from $A$. Then, (2) - (2’a)+(2’b)+(2’c) $\geq\sum_{q\in A_{1}}({\mathsf{mult}}(q)-{\mathsf{mult}}^{\prime}(q))\cdot(val(q)-C\cdot|u|)-\sum_{q\in A_{1}}{\mathsf{mult}}^{\prime}(q)C\cdot|u|-\sum_{q\in A_{2}}{\mathsf{mult}}^{\prime}(q)4\cdot C\cdot\mathbf{N}-C\cdot|u|^{2}$. Since $\sum_{q\in A}mult^{\prime}(q)\leq|u|$ and $|u|\leq\mathbf{N}$, we get (2) - (2’a)+(2’b)+(2’c) $\geq\sum_{q\in A_{1}}({\mathsf{mult}}(q)-{\mathsf{mult}}^{\prime}(q))\cdot(val(q)-C\cdot|u|)-5\cdot C\cdot\mathbf{N}^{2}$. Recall that $\sum_{q\in A_{1}}{\mathsf{mult}}(q)\geq 2\cdot\mathbf{N}$ and for every $q\in A_{1}$ we have $val(q)\geq 4\cdot C\cdot\mathbf{N}$. Therefore, $\sum_{q\in A_{1}}({\mathsf{mult}}(q)-{\mathsf{mult}}^{\prime}(q))\cdot(val(q)-C\cdot|u|)>8\cdot C\cdot\mathbf{N}^{2}$ and hence (2) $>$ (2’a)+(2’b)+(2’c). This concludes the proof that insertion of a barrier decreases the partial sum.

∎

Using the above lemma we can reduce the emptiness problem for finite-width $(\textsc{LimAvg};\textsc{Sum}^{+})$-automata with bidirectional slave automata to the bounded-width case.

Lemma 23**.**

Let $\mathbb{A}$ be a deterministic $(\textsc{LimAvg};\textsc{Sum}^{+})$-automaton of finite width with bidirectional slave automata. There exists a deterministic $(\textsc{LimAvg};\textsc{Sum}^{+})$-automaton $\mathbb{A}^{\prime}$ over an extended alphabet $\Sigma_{1}$ with bidirectional slave automata of width bounded exponentially in $|\mathbb{A}|$, such that the emptiness problems for $\mathbb{A}$ and $\mathbb{A}^{\prime}$ coincide, i.e., $\inf_{w\in\Sigma^{\omega}}{\cal L}_{{\mathbb{A}}}(w)=\inf_{w\in\Sigma_{1}^{\omega}}{\cal L}_{{\mathbb{A}^{\prime}}}(w)$. The size of $\mathbb{A}^{\prime}$ is $O(\mathbf{N}\cdot|\mathbb{A}|)$.

Proof.

We define an exponential size $(\textsc{LimAvg};\textsc{Sum}^{+})$-automaton $\mathbb{A}^{\prime}$ with bidirectional slave automata of width bounded by exponentially in $|\mathbb{A}|$ such that $\mathbb{A}^{\prime}$ simulates a subset of runes of $\mathbb{A}$ which satisfy the following condition (): at almost every position $s$, among slave automata active at $s$, at most $2\cdot|\mathbb{A}|\cdot\mathbf{N}$ will accumulate value greater than $4\cdot C\cdot\mathbf{N}$. Next, we show that for every run of $\mathbb{A}$ there exists a run satisfying () of at most the same value. It follows that the emptiness problems for $\mathbb{A}$ and $\mathbb{A}^{\prime}$ coincide.

Definition of $\mathbb{A}$. The alphabet $\Sigma_{1}$ consists of $\Sigma$ and additional marking letters described below. First, the automaton $\mathbb{A}^{\prime}$ invokes only dummy slave automata before the initiation marking. Past initial marking the master automaton keeps track of the number of invoked slave automata and rejects if the number of slave automata exceeds $2\cdot|\mathbb{A}|\cdot\mathbf{N}$. Second, we modify each slave automaton of $\mathbb{A}$ so that they work only as long as they can accumulate the value exceeding $4\cdot C\cdot\mathbf{N}$, where $C$ is the maximal weight among all slave automata of $\mathbb{A}$. In particular, slave automata, which accumulate the value below $4\cdot C\cdot\mathbf{N}$, are invoked for a single transition only. We encode in the alphabet whether a slave automaton is invoked for a single transition and the weight of this transition. Moreover, we encode in the alphabet that slave automata in state $q$ ought to terminate as in the following run they accumulate the value below $4\cdot C\cdot\mathbf{N}$. The master automaton checks whether the external markings are correct. These constructions involve a single exponential blow up of the master automaton, slave automata and the alphabet. Observe that accepting runs of $\mathbb{A}^{\prime}$ correspond to accepting runs of $\mathbb{A}$, which satisfy condition (). The values of the corresponding runs are the same. Now, we need to show that while computing the infimum over all accepting runs of $\mathbb{A}$, we can restrict ourselves to runs satisfying ().

The emptiness problems for $\mathbb{A}$ and $\mathbb{A}^{\prime}$ coincide. Since $\mathbb{A}^{\prime}$ simulates a subset of runs of $\mathbb{A}$ we have $\inf_{w\in\Sigma^{\omega}}{\cal L}_{{\mathbb{A}}}(w)\leq\inf_{w\in\Sigma_{1}^{\omega}}{\cal L}_{{\mathbb{A}^{\prime}}}(w)$. We show how to transform any word $w$ of $\mathbb{A}$ into a word whose unique run satisfies (*), which means that is can be simulated by $\mathbb{A}^{\prime}$, and whose value does not exceed the value of $w$. It follows that $\inf_{w\in\Sigma^{\omega}}{\cal L}_{{\mathbb{A}}}(w)\geq\inf_{w\in\Sigma_{1}^{\omega}}{\cal L}_{{\mathbb{A}^{\prime}}}(w)$.

Let $w$ be a word accepted by $\mathbb{A}$. Let $s$ be a position such that on every position $p\geq s$ in $w$ a barrier exists (Lemma 21). We start with $i=0$, word $w_{0}=w$ and $p_{0}=s$. We iteratively at step $i$, pick first position $p>p_{i}$ at which more than $2\cdot|\mathbb{A}|\cdot\mathbf{N}$ slave automata accumulate the values exceeding $4\cdot C\cdot\mathbf{N}$ and we insert a barrier $u_{i}$ at position $p$. Barrier $u_{i}$ exists as a barrier for $w$ at the corresponding position. Then, we start the next iteration $i+1$ with word $w_{i+1}=w_{i}[1,p]u_{i}w_{i}[p+1,\infty]$ and $p_{i+1}=p+|u_{i}|$. Observe that iterations past $i$ change only positions past $p_{i}$ in words $w_{i},w_{i+1},\ldots$, i.e., all words $w_{i},w_{i+1},\ldots$ share the prefix $w[1,p_{i}]$. Thus, there exists the limit word $w_{B}$, which is the result of the iterative process. We argue that the resulting word $w_{B}$ satisfies () and its value does not exceed the value of $w$. First, we show that $w_{B}$ satisfies ().

Let $u_{i}$ be a barrier at position $p$ in $w_{i}$ and let $w^{\prime}=w_{i}[1,p]u_{i}w_{i}[p+1,\infty]$. The forward-walking slave automata active at $p$ in $w_{i}$ are terminated within $u_{i}$ in $w^{\prime}$ and hence accumulate the value below $|u_{i}|<C\cdot N$ in $w^{\prime}$, where $C$ is the maximal weight of slave automata of $\mathbb{A}$. The number of forward-walking slave automata active between positions $p$ and $p+|u_{i}|$ which are not terminated within $u$ is bounded by $|u_{i}|<\mathbf{N}$. Therefore, at every position between $i$ and $p+|u|$ in $w^{\prime}$, at most $\mathbf{N}$ forward-walking slave automata accumulate the value exceeding $4\cdot C\cdot\mathbf{N}$. The similar argument applies to backward-walking slave automata, which shows that at positions $p$ to $p+|u|$ condition (*) is satisfied.

It remains to comment on the value of $w_{B}$. Barriers inserted in the iterative process satisfy conditions of Lemma 22, and hence the partial sums decrease from $w_{0}$ to $w_{1},w_{2}$ and so on. It follows partial sums in $w_{B}$ are bounded by partial sums in every word $w_{0},w_{1},\ldots$ and hence the value of $w_{B}$ does not exceed the value of $w$. ∎

Algorithm. Let $\mathbb{A}$ be a non-deterministic finite-width $(\textsc{LimAvg};\textsc{Sum}^{+})$-automaton with bidirectional slave automata. Lemma 19 reduces the emptiness problem of $\mathbb{A}$ to the emptiness problem of $\mathbb{A}_{d}$, which has the same properties as $\mathbb{A}$, but it is deterministic. The reduction takes exponential time and produces an exponential-size automaton, while it does not change the number of configurations. Therefore, the value of $\mathbf{N}$ for $\mathbb{A}$ and $\mathbb{A}_{d}$ is the same. Next, Lemma 23 reduces the emptiness problem for $\mathbb{A}_{d}$ to the emptiness problem of $\mathbb{A}_{B}$ which is a deterministic $(\textsc{LimAvg};\textsc{Sum}^{+})$-automaton with bidirectional slave automata and the width of $\mathbb{A}_{B}$ is linear in $\mathbf{N}$, i.e., it is exponential in $|\mathbb{A}|$. The size of $\mathbb{A}_{B}$ is $O(\mathbf{N}\cdot|\mathbb{A}_{d}|)$, i.e., it is exponential in $|\mathbb{A}|$. Therefore, the emptiness problem for $\mathbb{A}_{B}$ can be solved in polynomial space in $\mathbf{N}\cdot|\mathbb{A}_{B}|$ (Theorem 17) and in the exponential space in the size of $\mathbb{A}$.

B.3 The proof of Theorem 14

In the finite-automata framework, the pumping lemma is a standard tool to show inexpressibility results. It is difficult to state a pumping lemma for NWA as their state space is infinite. While there is finitely many configurations of NWA, the multiplicity of running slave automata is unbounded. We consider the graph of configurations of an NWA to reduce the infinite-space case to the finite-state case.

Recall that we assume that slave automata do not have outgoing transitions from accepting states. We also assume (without loss of generality) that initial states of slave automata do not have ingoing transitions.

Graph of configurations. Let $\mathbb{A}$ be an NWA with bidirectional slave automata over an alphabet $\Sigma$. We define the graph of configurations $G$ of an NWA $\mathbb{A}$ as a $\Sigma$-labeled graph whose nodes are configurations of $\mathbb{A}$. For $a\in\Sigma$, there exists an $a$-labeled edge from configuration $(q_{m},A_{1})$ to $(q_{m}^{\prime},A_{2})$ if and only if

• •

the master automaton of $\mathbb{A}$ has a transition $(q_{m},a,q_{m}^{\prime})$ invoking a slave automaton ${\mathfrak{B}}$ in an initial state $q_{I}$,

• •

for $i=1,2$, states $A_{i}$ are partitioned into states of backward-walking slave automata $A_{i}^{B}$ and forward-walking slave automata $A_{i}^{F}$,

• •

there exists a function $h_{F}$, which transforms all non-final states from $A_{1}^{F}$ onto $A_{2}^{F}\setminus\{q_{I}\}$ such that for every $q\in dom(h_{F})$ tuple $(q,a,h(q))$ is a transition of some slave automaton,

• •

there exists a function $h_{B}$, which transforms all non-final states from $A_{2}^{B}$ onto $A_{1}^{B}\setminus\{q_{I}\}$ such that for every $q\in dom(h_{B})$ tuple $(q,a,h(q))$ is a transition of some slave automaton, and

• •

if ${\mathfrak{B}}$ is forward-walking $q_{I}\in A_{2}^{F}$; otherwise $q_{I}\in A_{1}^{B}$.

Paths in $G$ are related to simple runs of $\mathbb{A}$. Consider a simple run of $\mathbb{A}$. Its sequence of configurations is an infinite path in $G$. Conversely, given a path $\pi$ in $G$ starting in the initial configuration $(q_{I},\emptyset)$, we can specify regular conditions ensuring (a) existence of a simple run corresponding to $\pi$ and (b) existence of a simple accepting run corresponding to $\pi$. Regularity of these conditions follows from the fact that unweighted parts of runs of $\mathbb{A}$ can be simulated by an alternating Büchi automaton. This automaton checks whether runs of all slave automata are finite; this suffices to ensure that a path corresponds to a valid simple run. It can also check acceptance condition, i.e., whether runs of all slave automata terminate in accepting states and the master automaton visits some accepting state infinitely often.

The graph of configurations of $\mathbb{A}$ enables us to construct accepting runs of $\mathbb{A}$ with desired properties. Having an accepting run of $\mathbb{A}$ with a sequence of configurations $\alpha\beta\gamma$ such that $\beta$ is a cycle in the graph of configurations of $\mathbb{A}$, we know that for every $n>0$ there exists an accepting run of $\mathbb{A}$ whose sequence of configurations is $\alpha\beta^{n}\gamma$. This is a key observation used in the following lemma.

See 13

Proof.

We show (i) in detail and next we comment on (ii). Suppose that $\mathbb{A}$ is a $(\textsc{LimAvg};\textsc{Sum}^{+})$-automaton with forward-walking slave automata which computes DCP (Example 3) restricted to the alphabet $\{r,\#,c\}$. First, we show that in the graph of configurations of $\mathbb{A}$ there exist two cycles $\tau_{r},\tau_{\#}$ such that $\tau_{r}$ is an $r$-labeled cycle in which at least one (non-dummy) slave automaton is invoked, and $\tau_{\#}$ is an $\#$-labeled cycle in which $\mathbb{A}$ takes only silent transitions, i.e., it invokes only slave automata that immediately accept returning no value. Next, we use $\tau_{r},\tau_{\#}$ to construct of a run $\pi_{0}$ on some word $u$ such that the value of $\pi_{0}$ is smaller than DCP of $u$, which contradicts the assumption that $\mathbb{A}$ computes DCP.

Existence of $\tau_{r}$ and $\tau_{\#}$. Let $K$ be greater than the number of configurations of $\mathbb{A}$ and let $N>15K^{2}$. To simplify the calculations, we denote by $\mathcal{O}(2K)$ some natural number from interval $[0,2K]$. For example, we write $N+\frac{3K-1}{2}=N+\mathcal{O}(2K)$.

Consider a word $w=(c\#^{N}r^{2K}c\#^{2N}r^{K})^{\omega}$. DCP of $w$ is $\frac{4}{3}\cdot N+\mathcal{O}(2K)$. Let $\pi$ be a run of $\mathbb{A}$ on $w$ of the value $\frac{4}{3}\cdot N+\mathcal{O}(2K)$. We can assume that $\pi$ is simple (Lemma 19). In every block $\#^{2K}$ in $w$, there exist positions $i_{1}<i_{2}$ such that the configurations in $\pi$ at $i_{1}$ and $i_{2}$ are the same and $i_{2}-i_{1}>K$. We remove these parts of $\pi$. The resulting sequence $\pi^{\prime}$ is a run of $\mathbb{A}$ on some word $w^{\prime}=c\#^{N}r^{L_{1}}c\#^{2N}r^{K}c\#^{N}r^{L_{2}}c\#^{2N}r^{K}\ldots$ such that $L_{1},L_{2},\ldots$ are at most $K-1$. Observe that DCP of $w^{\prime}$ is at least $\frac{3}{2}\cdot N$ and hence the value of $\pi^{\prime}$ is at least $\frac{3}{2}\cdot N$. However, the partial sums of the values returned by slave automata in $\pi^{\prime}$ are bounded by the corresponding partial sums in $\pi$. Therefore, the value of $\pi^{\prime}$ increases due to the fact that the removed parts of $\pi$ contain invocations of slave automata returning small values and removal of these parts of $\pi$ increase partial averages. It follows that infinitely often at least one (non-dummy) slave automaton is invoked over the block $r^{2K}$. Consider the sequence of configurations $\sigma[\pi]$ of run $\pi$. There exists infinitely many subsequences $\tau$ of $\sigma[\pi]$, which correspond to transitions over letters $r$ and satisfy: (A1) the first and the last configuration of $\tau$ is the same, (A2) along $\tau$ at least one slave automaton is invoked and (A3) the length of $\tau$ is bounded by $K$. Such a sequence corresponds to an $r$-labeled cycle in the graph of configurations of $\mathbb{A}$ of length at most $K$. There are finitely many such cycles and hence there exists a cycle $\tau_{r}$ satisfying condition (A1), (A2) and (A3) which occurs infinitely often in $\sigma[\pi]$.

In a similar we show that $\sigma[\pi]$ contains infinitely often a subsequence $\tau_{\#}$, which corresponds to transitions over letters $\#$, such that (B1) the first and the last configuration of $\tau_{\#}$ is the same, (B2) slave automata invoked along $\tau_{\#}$ return no value (correspond to silent transitions), and (B3) the length of $\tau_{\#}$ is bounded by $K$. To see that, we divide runs $\pi$ and $\pi^{\prime}$ into blocks separated by letter $c$. In transformation from $\pi$ to $\pi^{\prime}$, the average number of invocations of (non-dummy) slave automata per block decreases by at most $\frac{2K}{3}$. Yet, the value of $\pi^{\prime}$ increases by at least $\frac{1}{6}N-\mathcal{O}(2K)$ w.r.t. the value of $\pi$. Therefore, the average number of invoked slave automata per block cannot exceed $9K$ in $\pi$. It follows that at most $14\cdot K$ non-dummy slave automata are invoked on average in a block of $N$ letters $\#$. Thus, there exists infinitely many occurrences of subsequences of $\sigma[\pi]$ satisfying (B1), (B2) and (B3), and hence there exists a $\#$-labeled cycle $\tau_{\#}$ satisfying conditions (B1), (B2) and (B3), which occurs infinitely often in $\sigma[\pi]$.

Observe that there exist infinitely many subwords $c\#^{N}r^{2K}c\#^{2N}r^{K}$ of $w$ such that in the corresponding positions in $\sigma[\pi]$ occur both $\tau_{\#}$ and $\tau_{r}$. Thus, there exists a path $\alpha_{A}$ in the graph of configurations of $\mathbb{A}$ such that $\alpha_{A}$ leads from the last configuration of $\tau_{\#}$ to the first configuration of $\tau_{r}$ over letters $\#,r$. Moreover, all slave automata in $\pi$ terminate after finite number of steps, while $\tau_{\#}$ and $\tau_{r}$ occur infinitely often. Therefore, there exists a path $\alpha_{B}$ from the first configuration of $\tau_{r}$ to the last configuration of $\tau_{\#}$ over letters $\#,r,c$ such that (C1) at least one transition is over letter $c$, and (C2) all slave automata active at the first configuration of $\alpha_{B}$ are terminated before the end of $\alpha_{B}$, (C3) the master automaton of $\mathbb{A}$ visits an accepting state within $\alpha_{B}$. Let $u_{A}$ (resp., $u_{B}$) be a subword of $w$ at which configurations of $\pi$ form the sequence $\alpha_{A}$ (resp., $\alpha_{B}$). Next, we show the construction of $\pi_{0}$ using $\tau_{r},\tau_{\#}$, $\alpha_{A}$ and $\alpha_{B}$.

The construction of $\pi_{0}$. Let $M,L$ be natural numbers, which we fix later. We define $\pi_{0}$ as some simple accepting run that corresponds to the sequence of configurations $\alpha_{0}((\tau_{\#})^{L}\alpha_{A}(\tau_{r})^{M}\alpha_{B})^{\omega}$, where $\alpha_{0}$ is a sequence of configurations from an initial configuration to the first configuration of $\tau_{\#}$. Such a run exists as we can ensure that at positions corresponding to $\alpha_{B}$ all slave automata terminate in accepting states and the master automaton visits an accepting state. Let $u_{0}$ be a word at which there exists a run with the sequence of configurations $\alpha_{0}$. We define $u=u_{0}(\#^{L\cdot|\tau_{\#}|}u_{A}r^{M\cdot|\tau_{r}|}u_{B})^{\omega}$. The run $\pi_{0}$ is an accepting run on $u$. Observe that DCP of $u$ exceeds $|\tau_{\#}|\cdot L$. However, we show that the value of $\pi_{0}$ is smaller. Run $\pi_{0}$ is a lasso and its limit average is the average of the cycle, which corresponds to the average of $\alpha_{B}(\tau_{\#})^{L}\alpha_{A}(\tau_{r})^{M}\alpha_{B}$ excluding values of slave automata invoked in the second occurrence of $\alpha_{B}$. The non-dummy slave automata are invoked only in $\alpha_{B}$ and in $\alpha_{A}(\tau_{r})^{M}$. All slave automata invoked within this cycle terminate by the end of it, and hence (a) the values of slave automata invoked in $\alpha_{B}$ are bounded by the length of the cycle multiplied by $C$, the maximal weight of $\mathbb{A}$, i.e., $S_{1}=C\cdot(|\alpha_{B}|+|\alpha_{A}|+L\cdot|\tau_{\#}|+M\cdot|\tau_{r}|)$, and (b) the values of slave automata invoked in $\alpha_{A}(\tau_{r})^{M}$ are bounded by $S_{2}=C\cdot(|\alpha_{A}|+|\alpha_{B}|+M\cdot|\tau_{r}|)$. We have $S_{1}>S_{2}$, however there are at most $|\alpha_{B}|$ slave automata invoked in $\alpha_{B}$, which accumulate value at most $S_{1}$. The remaining slave automata are invoked in $\alpha_{A}(\tau_{r})^{M}$ and there are at least $M$ of them. Thus, the average value of the cycle is at most $\frac{S_{1}\cdot|\alpha_{B}|+S_{2}\cdot M}{|\alpha_{B}|+M}$. Now, for $M=2\cdot C\cdot|\alpha_{B}|\cdot|\tau_{\#}|$, we have $\frac{S_{1}\cdot|\alpha_{B}|}{|\alpha_{B}|+M}<|\alpha_{B}|+|\alpha_{A}|+\frac{L}{2}+C\cdot|\tau_{r}|\cdot|\alpha_{B}|$ and $\frac{S_{2}\cdot M}{|\alpha_{B}|+M}<S_{2}$. Let $L>2\cdot(S_{2}+|\alpha_{B}|+|\alpha_{A}|+C\cdot|\tau_{r}|\cdot|\alpha_{B}|)$, then the average of the cycle, which is bounded by $\frac{S_{1}\cdot|\alpha_{B}|+S_{2}\cdot M}{M+|\alpha_{B}|}$, is smaller than $L$. However, DCP of $u$ exceeds $L$, which contradicts the fact that $\mathbb{A}$ computes DCP.

Backward-walking slave automata. The proof for backward-walking slave automata is similar. We consider numbers $K,N$ and a word $w=(cw^{2K}\#^{N}cw^{K}\#^{2N})^{\omega}$; we show that there exist cycles $\tau_{w},\tau_{\#}^{\prime}$ in $\mathbb{A}$, with similar properties to $\tau_{r},\tau_{\#}$ from the forward case. Moreover, there exist sequences of configurations $\alpha_{A}^{\prime}$ from the last configuration of $\tau_{w}$ to the first configuration of $\tau_{\#}^{\prime}$, and $\alpha_{B}^{\prime}$ from the last configuration of $\tau_{\#}^{\prime}$ to the first configuration of $\tau_{w}$, with the properties similar to (C1), (C2) and (C3). To show (C2) we use the fact that $\tau_{w}$ and $\tau_{\#}^{\prime}$ occur infinitely often and $\mathbb{A}$ has finite-width, and hence for every position $i$ there exists position $j>i$ such that every (backward-walking) slave automaton active at position $j$ terminates before $i$ (i.e., at some position within $[i,j]$). Next, we construct from $\tau_{w},\tau_{\#}^{\prime},\alpha_{A}^{\prime},\alpha_{B}^{\prime}$ a run $\pi_{0}^{\prime}$ of the value lower than DCP of the corresponding word. The construction is virtually the same as in the forward case. ∎

Appendix C Proofs from Section 6

See 16

Proof.

(1): Assume that (*) is satisfied. Consider an accepting run $\pi$ with configuration $\mathcal{C}[1]$ occurring infinitely often. Let $i$ be a position at which configuration $\mathcal{C}[1]$ occurs. Let $i^{\prime}<i$ be the last position at which any automaton from $Fc$ is invoked. Consider the run resulting from inserting cycle $\mathcal{C}$ repeated $N$ times at position $i$ in $\pi$. The only slave automata active past position $i+|\mathcal{C}|$, which has been invoked before $i^{\prime}$ are the automata from $Fc$. Therefore, the partial sum of values returned by slave automata up to position $i^{\prime}$ decreases by at least $(N-1)\cdot\textsc{Gain}(\mathcal{C},Fc)+C<-(N-1)+C$, where $C$ is the value of forward slave automata invoked before $i^{\prime}$, which terminate in $\mathcal{C}$. The number of slave automata invoked before $i^{\prime}$ does not change and hence by picking $N$ large enough we can decease the partial average up to $i^{\prime}$ arbitrarily. We can apply such a pumping step at every position with configuration $\mathcal{C}[1]$ obtaining a run whose limit infimum of partial averages diverges to $-\infty$.

(2): $(\Rightarrow)$: Assume that there exists a cycle $\mathcal{C}$ in the graph of configurations of $\mathbb{A}$ and a restriction $R$ such that $\textsc{AvgE}(\mathcal{C},R)$ and there exists an accepting run $\pi$ with configuration $\mathcal{C}[1]$ occurring infinitely often. Let $i$ be a position at which configuration $\mathcal{C}[1]$ occurs. We insert $\mathcal{C}$ at position $i$ and obtain run $\pi^{\prime}$. Let $i^{\prime}$ be the last position in $\pi^{\prime}$ such that $i^{\prime}\geq i+|\mathcal{C}|$ and all automata active at position $i$, which are not in $R$, are invoked before $i^{\prime}$. Due to presence of backward-walking slave automata $i^{\prime}$ can be strictly grater than $i+|\mathcal{C}|$. Consider the run resulting from inserting cycle $\mathcal{C}$ repeated $N$ times at position $i$ in $\pi^{\prime}$. Then, the partial average up to position $i^{\prime}+N|\mathcal{C}|$ is given by the expression $\frac{a+N\cdot p-\Delta}{b+N\cdot q}$, where

• •

$a$ is the partial sum of values returned by slave automata invoked up to $i^{\prime}$ in run $\pi$,

• •

$b$ is the number of slave automata invoked up to $i^{\prime}$ in run $\pi$,

• •

$\frac{p}{q}=\textsc{AvgE}(\mathcal{C},R)$ and $q$ is the number of slave automata invoked in $\mathcal{C}$, and

• •

$\Delta$ is the value accumulated by backward-walking slave automata invoked past $i^{\prime}+N|\mathcal{C}|$, which terminate within interval $[i+N|\mathcal{C}|,i+(N+1)|\mathcal{C}|]$.

Now, by taking $N$ large enough we can bring the partial average arbitrarily close to $\frac{a}{b}$. Using that and simple iteration, we can construct an accepting run of the value $\textsc{AvgE}(\mathcal{C},R)$.

$(\Leftarrow)$: Assume that $\mathbb{A}$ does not satisfy () from (1). It follows that in every accepting run of $\mathbb{A}$ for almost every position $i$, slave automata invoked before $i$, accumulate past $i$ the value exceeding value $D$ defined as $-C\cdot k^{2}\cdot conf(\mathbb{A})$, where $C$ is the maximal weight occurring in $\mathbb{A}$ and $conf(\mathbb{A})$ is the number of configurations of $\mathbb{A}$. Indeed, if there exists such a position $i$, there exists a cycle past $i$ which we can pump to lower the sum of value returned by slave automata invoked before $i$. Hence, existence of infinitely many such positions $i$, implies that condition () holds.

Let $\pi$ be an accepting run of $\mathbb{A}$ of value $\lambda$. Consider $\epsilon>0$. There exists a prefix of $\pi$ up to position $i$ such that the partial average of values returned by slave automata up to $i$ is at most $\lambda+\epsilon$, the sum of values accumulated by slave automata invoked before $i$ exceeds $D$ and and the number of slave automata before $i$ exceeds $\frac{\epsilon}{-D}$. Then, the partial average of the values accumulated by slave automata invoked before $i$ within positions $1,\ldots,i$ is at most $\lambda+2\cdot\epsilon$.

Now, we can decompose the prefix up to $i$ into simple cycles one by one, i.e., having a prefix $\tau$ of $\pi$ up to position $i$, we pick a simple cycle, remove it from $\tau$ and repeat the process. We terminate when we end up with run $\tau_{E}$ which has no simple cycle to remove; the remaining run $\tau_{E}$ has length bounded by the number of configurations and therefore its sum of values is greater than $D$. Thus, the partial average of the values accumulated by slave automata invoked before $i$ within positions $1,\ldots,i$ equals (a)  the weighted average of average weights of simple cycles excluding backward-walking slave automata invoked past $i$, plus (b) the average of $\tau_{E}$ bounded by $D\cdot\frac{\epsilon}{D}$. It follows that there exist a simple cycle $\mathcal{C}$ and a restriction $R$ such that $\textsc{AvgE}(\mathcal{C},R)\leq\lambda+3\cdot\epsilon$; otherwise the weighted average in (a) exceeds $\lambda+3\cdot\epsilon$, which contradicts the choice of prefix of $\pi$.

However, there are infinitely many $\epsilon>0$, while there are finitely many simple cycles. Therefore, there exist a simple cycle $\mathcal{C}$ and a restriction $R$ such that $\textsc{AvgE}(\mathcal{C},R)\leq\lambda$. ∎

See 17

Proof.

It suffices to show that conditions from Lemma 16 can be checked (a) in logarithmic space for constant $k$ and unary weights, (b) polynomial time for constant $k$ and binary weights, and (c) polynomial space for $k$ given in unary. Observe that these conditions reduce to weighted reachability, which can be computed in logarithmic space in the size of the graph of $k$-configurations of $\mathbb{A}$, provided that weights can fit in logarithmic space. Otherwise, if weights are represented in binary and are of length greater than logarithmic in the size of the graph, weighted reachability can be implemented using Dijkstra algorithm in polynomial time. The size of the graph of $k$-configurations is polynomial in the size of $\mathbb{A}$ and exponential in $k$. Thus, the graph of $k$-configurations of $\mathbb{A}$ is polynomial if $k$ is constant, and exponential if $k$ is given in unary. Finally, we comment how to compute the successor relation.

We define a presuccessor relation $R$ on $k$-configurations as follows. We have $(q;q_{1},\ldots,q_{k})R(q^{\prime};q_{1}^{\prime},\ldots,q_{k}^{\prime})$ if and only if for some $a\in\Sigma$ the master automaton of $\mathbb{A}$ has a transition $(q,a,q^{\prime})$ invoking a slave automaton ${\mathfrak{B}}$ in an initial state $q_{I}$, and for every component $j\in\{1,\ldots,k\}$ one of the following holds

• •

$q_{j}$ is a non-final state of a forward-walking slave automaton and $(q_{j},a,q_{j}^{\prime})$ is a transition of this automaton,

• •

$q_{j}$ is a final state of a forward-walking slave automaton, and $q_{j}^{\prime}=\bot$ or $q_{j}^{\prime}=q_{I}$,

• •

$q_{j}^{\prime}$ is a non-final state of a backward-walking slave automaton and $(q_{j}^{\prime},a,q_{j})$ is a transition of this automaton,

• •

$q_{j}^{\prime}$ is a final state of a backward-walking slave automaton, and $q_{j}=\bot$ or $q_{j}=q_{I}$,

if ${\mathfrak{B}}$ is forward-walking (resp., backward-walking) slave automaton, then for exactly one component $j$ we have $q_{I}=q_{j}^{\prime}$ (resp., $q_{I}=q_{j}$). Observe that $R$ encodes a local consistency of transitions of the master and slave automata. A sequence of $k$-configurations consistent with $R$ satisfying the following conditions (a) and (b) corresponds to an accepting simple run. These conditions are: (a) the master automaton visits one of its accepting states infinitely often, and (b) every slave automaton terminates after finitely many steps. Now observe that the successor relation defined in Section 6 is the presuccessor relation restricted to $k$-configurations $C$, which are (1) reachable through $R$ from the initial configuration and (2) a cycle w.r.t. $R$ satisfying conditions (a) and (b) is reachable through $R$ from $C$. Indeed, for such configurations $C_{1},C_{2}$ satisfying $C_{1}RC_{2}$ there exists a sequence of $k$-configurations consistent with $R$, which corresponds to an accepting run. It follows that the successor relation in the graph of $k$-configurations can be computed based on reachability w.r.t. presuccessor relation, which is computable in logarithmic space. ∎