[Theory of computation]: Formal languages and automata theory — Automata over
infinite objects — Quantitative automata Primary: 68Q45, 68Q70; Secondary:
68Q42

# Weighted $\omega$-Restricted One-Counter Automata

Manfred Droste  Universität Leipzig, Institut für Informatik
<EMAIL_ADDRESS>and  Werner Kuich  Technische Universität
Wien, Institut für Diskrete Mathematik und Geometrie<EMAIL_ADDRESS>
###### Abstract.

Let $S$ be a complete star-omega semiring and $\Sigma$ be an alphabet. For a
weighted $\omega$-restricted one-counter automaton $\mathcal{C}$ with set of
states $\\{1,\dots,n\\}$, $n\geq 1$, we show that there exists a mixed
algebraic system over a complete semiring-semimodule pair
${((S\ll\Sigma^{*}\gg)^{n\times n},(S\ll\Sigma^{\omega}\gg)^{n})}$ such that
the behavior $\|\mathcal{C}\|$ of $\mathcal{C}$ is a component of a solution
of this system. In case the basic semiring is $\mathbb{B}$ or
$\mathbb{N}^{\infty}$ we show that there exists a mixed context-free grammar
that generates $\|\mathcal{C}\|$. The construction of the mixed context-free
grammar from $\mathcal{C}$ is a generalization of the well-known triple
construction in case of restricted one-counter automata and is called now
triple-pair construction for $\omega$-restricted one-counter automata.

###### Key words and phrases:

weighted pushdown automata, algebraic series, weighted contextfree grammar,
formal power series, complete semiring

This work was partially supported by DFG Graduiertenkolleg 1763 (QuantLA)

The second author was partially supported by Austrian Science Fund (FWF):
grant no. I1661 – N25.

##  1\. Introduction

Restricted one-counter pushdown automata and languages were introduced by
Greibach [13] and considered in Berstel [1], Chapter vii@ 4. These restricted
one-counter pushdown automata are pushdown automata having just one pushdown
symbol accepting by empty tape, and the family of restricted one-counter
languages is the family of languages accepted by them.

Let L be the Lukasiewicz language, i.e., the formal language over the alphabet
$\Sigma=\\{a,b\\}$ generated by the context-free grammar with productions
$S\to aSS,S\to b$. Then the family of restricted one-counter languages is the
principal cone generated by L, while the family of one-counter languages is
the full AFL generated by L.

All these results can be transferred to formal power series and restricted
one-counter automata over them (see Kuich, Salomaa [16], Example 11.5).
Restricted one-counter automata can also be used to accept infinite words and
it is this aspect we generalize in our paper.

We consider weighted $\omega$-restricted one-counter automata and their
relation to algebraic systems over the complete semiring-semimodule pair
$(S^{n\times n},V^{n})$, where $S$ is a complete star-omega semiring. It turns
out that the well-known triple construction for pushdown automata in case of
unweighted restricted one-counter automata can be generalized to a triple-pair
construction for weighted $\omega$-restricted one-counter automata. In the
classical theory, the triple construction yields for a given pushdown
automaton an equivalent context-free grammar. (See Harrison [14], Theorem
5.4.3; Bucher, Maurer [3], Sätze 2.3.10, 2.3.30; Kuich, Salomaa [16], pages
178, 306; Kuich [15], page 642; Ésik, Kuich [11], pages 77, 78.)

The paper consists of this and three more sections. In Section 2, we review
the necessary preliminaries. In Section 3, restricted one-counter matrices are
introduced and their properties are studied. The main result is that, for such
a matrix $M$, the $p$-block of the infinite column vector $M^{\omega,k}$ is a
solution of the linear equation
$z=(M_{p,p^{2}}(M^{*})_{p,\varepsilon}+M_{p,p}+M_{p,p^{2}})z$. In Section 4,
weighted $\omega$-restricted one-counter automata are introduced as a special
case of weighted $\omega$-pushdown automata. We show that for a weighted
$\omega$-restricted one-counter automaton $\mathcal{C}$ there exists a mixed
algebraic system such that the behavior $\|\mathcal{C}\|$ of $\mathcal{C}$ is
a component of a solution of this system. In Section 5 we consider the case
that the complete star-omega semiring $S$ is equal to $\mathbb{B}$ or
$\mathbb{N}^{\infty}$. Then for a given weighted $\omega$-restricted one-
counter automaton $\mathcal{C}$ a mixed context-free grammar is constructed
that generates $\|\mathcal{C}\|$. This construction is a generalization of the
well-known triple construction in case of restricted one-counter automata and
is called _triple-pair construction_ for $\omega$-restricted one-counter
automata.

##  2\. Preliminaries

For the convenience of the reader, we quote definitions and results of Ésik,
Kuich [7, 8, 10] from Ésik, Kuich [11]. The reader should be familiar with
Sections 5.1-5.6 of Ésik, Kuich [11].

A semiring $S$ is called _complete_ if it is possible to define sums for all
families $(a_{i}\mid i\in I)$ of elements of $S$, where $I$ is an arbitrary
index set, such that the following conditions are satisfied (see Conway [4],
Eilenberg [6], Kuich [15]):

(i)
$\displaystyle\sum\limits_{i\in\emptyset}a_{i}=0,\qquad\sum\limits_{i\in\\{j\\}}a_{i}=a_{j},\qquad\sum\limits_{i\in\\{j,k\\}}a_{i}=a_{j}+a_{k}\text{
for }j\neq k\,,$ (ii) $\displaystyle\sum\limits_{j\in J}\big{(}\sum_{i\in
I_{j}}a_{i}\big{)}=\sum_{i\in I}a_{i}\,,\text{ if }\ \bigcup_{j\in
J}\\!I_{j}=I\ \text{ and }\ I_{j}\cap I_{j^{\prime}}=\emptyset\ \text{ for }\
j\neq j^{\prime}\,,$ (iii) $\displaystyle\sum_{i\in I}(c\cdot
a_{i})=c\cdot\big{(}\sum_{i\in I}a_{i}\big{)},\qquad\sum_{i\in I}(a_{i}\cdot
c)=\big{(}\sum_{i\in I}a_{i}\big{)}\cdot c\,.$

This means that a semiring $S$ is complete if it is possible to define
“infinite sums” (i) that are an extension of the finite sums, (ii) that are
associative and commutative and (iii) that satisfy the distribution laws. If
$S$ is a monoid and conditions (i) and (ii) are satisfied then $S$ is called a
_complete monoid_.

A semiring S equipped with an additional unary star operation ${}^{*}:S\to S$
is called a starsemiring. In complete semirings for each element $a$, the
_star_ $a^{*}$ of $a$ is defined by

$a^{*}=\sum_{j\geq 0}a^{j}\,.$

Hence, each complete semiring is a starsemiring, called a _complete
starsemiring_.

Suppose that $S$ is a semiring and $V$ is a commutative monoid written
additively. We call $V$ a (left) $S$-semimodule if $V$ is equipped with a
(left) action

$\displaystyle S\times V$ $\displaystyle\ \to\ V$ $\displaystyle(s,v)$
$\displaystyle\ \mapsto\ sv$

subject to the following rules:

$\displaystyle s(s^{\prime}v)$ $\displaystyle=(ss^{\prime})v$ $\displaystyle
1v$ $\displaystyle=v$ $\displaystyle(s+s^{\prime})v$
$\displaystyle=sv+s^{\prime}v$ $\displaystyle\hskip 56.9055pt0v$
$\displaystyle=0$ $\displaystyle s(v+v^{\prime})$
$\displaystyle=sv+sv^{\prime}$ $\displaystyle s0$ $\displaystyle=0,$

for all $s,s^{\prime}\in S$ and $v,v^{\prime}\in V$. When V is an
$S$-semimodule, we call $(S,V)$ a _semiring-semimodule pair_.

Suppose that $(S,V)$ is a semiring-semimodule pair such that $S$ is a
starsemiring and $S$ and $V$ are equipped with an omega operation
${}^{\omega}:S\to V$. Then we call $(S,V)$ a _starsemiring-omegasemimodule
pair_.

Ésik, Kuich [9] define a _complete semiring-semimodule pair_ to be a semiring-
semimodule pair $(S,V)$ such that $S$ is a complete semiring and V is a
complete monoid with

$\displaystyle s\big{(}\sum_{i\in I}v_{i}\big{)}$ $\displaystyle=\sum_{i\in
I}sv_{i}$ $\displaystyle\big{(}\sum_{i\in I}s_{i}\big{)}v$
$\displaystyle=\sum_{i\in I}s_{i}v\,,$

for all $s\in S$, $v\in V$, and for all families $(s_{i})_{i\in I}$ over $S$
and $(v_{i})_{i\in I}$ over $V$; moreover, it is required that an _infinite
product operation_

$(s_{1},s_{2},\ldots)\ \mapsto\ \prod_{j\geq 1}s_{j}$

is given mapping infinite sequences over $S$ to $V$ subject to the following
three conditions:

$\displaystyle\prod_{i\geq 1}s_{i}$ $\displaystyle\ =\ \prod_{i\geq
1}(s_{n_{i-1}+1}\cdot\dots\cdot s_{n_{i}})$ $\displaystyle
s_{1}\cdot\prod_{i\geq 1}s_{i+1}$ $\displaystyle\ =\ \prod_{i\geq 1}s_{i}$
$\displaystyle\prod_{j\geq 1}\sum_{i_{j}\in I_{j}}s_{i_{j}}$ $\displaystyle\
=\ \sum_{(i_{1},i_{2},\dots)\in I_{1}\times I_{2}\times\dots}\prod_{j\geq
1}s_{i_{j}}\,,$

where in the first equation $0=n_{0}\leq n_{1}\leq n_{2}\leq\dots$ and
$I_{1},I_{2},\dots$ are arbitrary index sets. Suppose that $(S,V)$ is
complete. Then we define

$\displaystyle s^{*}$ $\displaystyle\ =\ \sum_{i\geq 0}s^{i}$ $\displaystyle
s^{\omega}$ $\displaystyle\ =\ \prod_{i\geq 1}s\,,$

for all $s\in S$. This turns $(S,V)$ into a starsemiring-omegasemimodule pair.
Observe that, if $(S,V)$ is a complete semiring-semimodule pair, then
$0^{\omega}=0$.

For a starsemiring $S$, we denote by $S^{n\times n}$ the semiring of $n\times
n$-matrices over $S$. If $(S,V)$ is a complete semiring-semimodule pair then,
by Ésik, Kuich [12], $(S^{n\times n},V^{n})$ is again a complete semiring-
semimodule pair.

A _star-omega semiring_ is a semiring $S$ equipped with unary operations ∗ and
${}^{\omega}:S\to S$. A star-omega semiring $S$ is called _complete_ if
$(S,S)$ is a complete semiring semimodule pair, i.e., if $S$ is complete and
is equipped with an infinite product operation that satisfies the three
conditions stated above. For the theory of infinite words and finite automata
accepting infinite words by the Büchi condition consult Perrin, Pin [17].

##  3\. Restricted one-counter matrices

In this section we introduce restricted one-counter (roc) matrices. Restricted
one-counter matrices are a special case of pushdown matrices introduced by
Kuich, Salomaa [16]. A matrix $M\in(S^{n\times
n})^{\Gamma^{*}\times\Gamma^{*}}$ is termed a _pushdown transition matrix_
(with _pushdown alphabet_ $\Gamma$ and _set of states_ $\\{1,\dots,n\\}$) if

  1. (i)

for each $p\in\Gamma$ there exist only finitely many blocks $M_{p,\pi}$,
$\pi\in\Gamma^{*}$, that are non-zero;

  2. (ii)

for all $\pi_{1},\pi_{2}\in\Gamma^{*}$,

$M_{\pi_{1},\pi_{2}}=\left\\{\begin{array}[]{ll}M_{p,\pi}&\hskip
5.69046pt\text{if there exist }p\in\Gamma,\pi,\pi^{\prime}\in\Gamma^{*}\text{
with }\pi_{1}=p\pi^{\prime}\text{ and }\pi_{2}=\pi\pi^{\prime},\\\ 0&\hskip
5.69046pt\text{otherwise.}\end{array}\right.$

Theorem 10.5 of Kuich, Salomaa [16] states that for pushdown matrices over
power series semirings with particular properties,
$(M^{*})_{\pi_{1}\pi_{2},\varepsilon}=(M^{*})_{\pi_{1},\varepsilon}(M^{*})_{\pi_{2},\varepsilon}$
holds for all $\pi_{1},\pi_{2}\in\Gamma^{*}$. This result is generalized in
the case of roc-matrices to arbitrary roc-matrices over complete starsemirings
in Corollary 2. Then we prove some important equalities for roc-matrices. In
Theorem 1 and Corollary 2, $S$ denotes a complete starsemiring; afterwards in
this section, $(S,V)$ denotes a complete semiring-semimodule pair.

A _restricted one-counter_ (abbreviated _roc_) _matrix (with counter symbol
$p$)_ is a matrix $M$ in $(S^{n\times n})^{p^{*}\times p^{*}}$, for some
$n\geq 1$, subject to the following condition: There exist matrices $A,B,C\in
S^{n\times n}$ such that, for all $k\geq 1$,

$M_{p^{k},p^{k+1}}=A\,,\quad M_{p^{k},p^{k}}=C\,\quad M_{p^{k},p^{k-1}}=B\,,$

and these blocks of $M$ are the only ones which may be non-zero. (Here,
$p^{*}=\\{p^{n}\mid n\geq 0\\}$. A block of $M$ is an element of the matrix
$M$ which is itself a matrix in $S^{n\times n}$.)

Observe that, for $k\geq 1$,

$\displaystyle M_{p^{k},p^{k+1}}$ $\displaystyle\ =\ M_{p,p^{2}}$
$\displaystyle\ =\ A\,,$ $\displaystyle M_{p^{k},p^{k}}$ $\displaystyle\ =\
M_{p,p}$ $\displaystyle\ =\ C\,,$ $\displaystyle M_{p^{k},p^{k-1}}$
$\displaystyle\ =\ M_{p,\varepsilon}$ $\displaystyle\ =\ B\,,$ $\displaystyle
M_{\varepsilon,p^{k}}$ $\displaystyle\ =\ M_{\varepsilon,\varepsilon}$
$\displaystyle\ =\ 0\,.$

Also note that the matrix $A$ (resp $B,C$) in $S^{n\times n}$ describes the
weight of transitions when pushing (resp., popping, not changing) an
additional symbol $p$ to (resp., from) the pushdown counter.

######  Theorem 1.

Let S be a complete starsemiring and $M$ be a roc-matrix. Then, for all $i\geq
0$,

$(M^{*})_{p^{i+1},\varepsilon}\ =\
(M^{*})_{p,\varepsilon}(M^{*})_{p^{i},\varepsilon}\,.$

######  Proof 3.1.

First observe that

$(M^{*})_{p^{i+1}\\!,\varepsilon}=\\!\\!\sum_{m\geq
0}(M^{m+1})_{p^{i+1}\\!,\varepsilon}=\\!\\!\sum_{m\geq 0}\sum_{\hskip
8.5359pti_{1},\dots,i_{m}\geq
1}\\!\\!\\!\\!\\!M_{p^{i\text{+}1}\\!,p^{i_{1}}}M_{p^{i_{1}}\\!,p^{i_{2}}}\dots
M_{p^{i_{m\text{-}1}}\\!,p^{i_{m}}}M_{p^{i_{m}}\\!,\varepsilon}\,,$

where, for $m=0$, the product equals $M_{p^{i+1},\varepsilon}$. Now we obtain

$\displaystyle(M^{*})_{p^{i+1},\varepsilon}=\ $ $\displaystyle\sum_{m\geq
0}\sum_{i_{1},\dots,i_{m}\geq 1}M_{p^{i+1},p^{i_{1}}}\dots
M_{p^{i_{m-1}},p^{i_{m}}}M_{p^{i_{m}},\varepsilon}$ $\displaystyle=\ $
$\displaystyle\sum_{m_{1}\geq 0}\big{(}\sum_{j_{1},\dots,j_{m_{1}}\geq
1}M_{p^{i+1},p^{i+j_{1}}}\dots
M_{p^{i+j_{m_{1}-1}},p^{i+j_{m_{1}}}}M_{p^{i+j_{m_{1}}},p^{i}}\big{)}\cdot$
$\displaystyle\sum_{m_{2}\geq 0}\big{(}\sum_{i_{1},\dots,i_{m_{2}}\geq
1}M_{p^{i},p^{i_{1}}}\dots
M_{p^{i_{m_{2}-1}},p^{i_{m_{2}}}}M_{p^{i_{m_{2}}},\varepsilon}\big{)}$
$\displaystyle=\ $ $\displaystyle\sum_{m_{1}\geq
0}\big{(}\sum_{j_{1},\dots,j_{m_{1}}\geq 1}M_{p,p^{j_{1}}}\dots
M_{p^{j_{m_{1}-1}},p^{j_{m_{1}}}}M_{p^{j_{m_{1}}},\varepsilon}\big{)}(M^{*})_{p^{i},\varepsilon}$
$\displaystyle=\ $
$\displaystyle(M^{*})_{p,\varepsilon}(M^{*})_{p^{i},\varepsilon}\,.$

Clearly, in each sequence leading from $p^{i+1}$ to $\varepsilon$, there is a
first time at which the top $p$ is reduced to $\varepsilon$ and at which
$p^{i}$ is seen. This moment is reached at the end of the second line. Hence,
in the second line the pushdown contents $p^{i+j_{1}},\dots,p^{i+j_{m_{1}}}$,
$m_{1}\geq 0$ are always nonempty.

######  Corollary 2.

For all $i\geq 0$, $\ (M^{*})_{p^{i},\varepsilon}\ =\
((M^{*})_{p,\varepsilon})^{i}$.

######  Lemma 3.

Let $(S,V)$ be a complete semiring-semimodule pair. Let $M\in(S^{n\times
n})^{p^{*}\times p^{*}}$ be a roc-matrix. Then

$(M^{\omega})_{p^{2}}\ =\
(M^{\omega})_{p}+(M^{*})_{p,\varepsilon}(M^{\omega})_{p}\,.$

######  Proof 3.2.

Subsequently in the first equation we split the summation so that in the first
summand there is no factor $M_{p^{2},p}$, while in the second summand there is
at least one factor $M_{p^{2},p}$; since $k_{1},\dots,k_{m}\geq 2$,
$M_{p^{k_{m}},p}$ is the first such factor. In the second equality we use the
property of $M$ being a roc-matrix: $M_{p^{i},p^{j}}=M_{p^{i-1},p^{j-1}}$ for
$i\geq 2$, $j\geq 1$. We compute:

$\displaystyle(M^{\omega})_{p^{2}}=\ $
$\displaystyle\sum_{i_{1},i_{2},\dots\geq
2}M_{p^{2},p^{i_{1}}}M_{p^{i_{1}},p^{i_{2}}}\dots+$ $\displaystyle\sum_{m\geq
0}\sum_{k_{1},k_{2},\dots,k_{m}\geq
2}\\!\\!\\!M_{p^{2},p^{k_{1}}}M_{p^{k_{1}},p^{k_{2}}}\dots
M_{p^{k_{m}},p}\sum_{j_{1},j_{2},\dots\geq
1}\\!\\!M_{p,p^{j_{1}}}M_{p^{j_{1}},p^{j_{2}}}\dots$ $\displaystyle=\ $
$\displaystyle\sum_{i_{1},i_{2},\dots\geq
2}M_{p,p^{i_{1}-1}}M_{p^{i_{1}-1},p^{i_{2}-1}}\dots+$
$\displaystyle\sum_{m\geq 0}\sum_{k_{1},k_{2},\dots,k_{m}\geq
2}\\!\\!\\!M_{p,p^{k_{1}-1}}M_{p^{k_{1}-1},p^{k_{2}-1}}\dots
M_{p^{k_{m}-1},\varepsilon}(M^{\omega})_{p}$ $\displaystyle\
=(M^{\omega})_{p}+\sum_{m\geq 0}(M^{m+1})_{p,\varepsilon}(M^{\omega})_{p}$
$\displaystyle\ =(M^{\omega})_{p}+(M^{*})_{p,\varepsilon}(M^{\omega})_{p}\,.$

Intuitively, our next theorem states that infinite computations starting with
$p$ on the pushdown tape yield the same matrix $(M^{\omega})_{p}$ as the sum
of the following three matrix products:

  * •

$M_{p,p^{2}}(M^{\omega})_{p}$ (i.e., changing the contents of the pushdown
tape from $p$ to $pp$ and starting the infinite computations with the leftmost
$p$; the second $p$ is never read),

  * •

$M_{p,p^{2}}(M^{*})_{p,\varepsilon}(M^{\omega})_{p}$ (i.e., changing the
contents of the pushdown tape from $p$ to $pp$, emptying the leftmost $p$ by
finite computations and starting the infinite computations with the rightmost
$p$),

  * •

$M_{p,p}(M^{\omega})_{p}$ (i.e., changing the contents of the pushdown tape
from $p$ to $p$ and starting the infinite computations with this $p$).

The forthcoming Theorem 7 has an analogous intuitive interpretation.

######  Theorem 4.

Let $(S,V)$ be a complete semiring-semimodule pair and let $M\in(S^{n\times
n})^{p^{*}\times p^{*}}$ be a roc-matrix. Then

$(M^{\omega})_{p}\ =\
(M_{p,p^{2}}+M_{p,p^{2}}(M^{*})_{p,\varepsilon}+M_{p,p})(M^{\omega})_{p}\,.$

######  Proof 3.3.

We obtain, by Lemma 3

$\displaystyle(M_{p,p^{2}}+M_{p,p^{2}}(M^{*})_{p,\varepsilon}+M_{p,p})(M^{\omega})_{p}$
$\displaystyle=\quad$ $\displaystyle
M_{p,p^{2}}((M^{\omega})_{p}+(M^{*})_{p,\varepsilon}(M^{\omega})_{p})+M_{p,p}(M^{\omega})_{p}$
$\displaystyle=\quad$ $\displaystyle
M_{p,p^{2}}(M^{\omega})_{p^{2}}+M_{p,p}(M^{\omega})_{p}\ =\ (MM^{\omega})_{p}\
=\ (M^{\omega})_{p}\,.$

######  Corollary 5.

Let $M\in(S^{n\times n})^{p^{*}\times p^{*}}$ be a roc-matrix. Then
$(M^{\omega})_{p}$ is a solution of

$z=(M_{p,p^{2}}+M_{p,p^{2}}(M^{*})_{p,\varepsilon}+M_{p,p})z\,.$

When we say “$G$ is the graph with matrix $M\in(S^{n\times n})^{p^{*}\times
p^{*}}$” then it means that $G$ is the graph with adjacency matrix
$M^{\prime}\in S^{(p^{*}\times n)\times(p^{*}\times n)}$, where $M^{\prime}$
corresponds to $M$ with respect to the canonical isomorphism between
$(S^{n\times n})^{p^{*}\times p^{*}}$ and $S^{(p^{*}\times
n)\times(p^{*}\times n)}$.

Let now $M$ be a roc-matrix and $0\leq k\leq n$. Then $M^{\omega,k}$ is the
column vector in $(V^{n})^{p^{*}}$ defined as follows: For $i\geq 1$ and
$1\leq j\leq n$, let $((M^{\omega,k})_{p^{i}})_{j}$ be the sum of all weights
of paths in the graph with matrix $M$ that have initial vertex $(p^{i},j)$ and
visit vertices $(p^{i^{\prime}},j^{\prime})$, $i^{\prime}\in\mathbb{N}$,
$j^{\prime}\in\\{1,\ldots,k\\}$, infinitely often. Observe that
$M^{\omega,0}=0$ and $M^{\omega,n}=M^{\omega}$. Later on it will be seen that
this formalizes the Büchi acceptance condition with repeated states
$\\{1,\ldots,k\\}$.

Let $P_{k}=\\{(j_{1},j_{2},\dots)\in\\{1,\dots,n\\}^{\omega}\mid j_{t}\leq
k\text{ for infinitely many }t\geq 1\\}$.

Then for $1\leq j\leq n$, we obtain

$((M^{\omega,k})_{p})_{j}=\sum_{i_{1},i_{2},\dots\geq
1}\sum_{(j_{1},j_{2},\dots)\in
P_{k}}(M_{p,p^{i_{1}}})_{j,j_{1}}(M_{p^{i_{1}},p^{i_{2}}})_{j_{1},j_{2}}(M_{p^{i_{2}},p^{i_{3}}})_{j_{2},j_{3}}\dots\,.$

By Theorem 5.4.1 of Ésik, Kuich [11], we obtain for a finite matrix $A\in
S^{n\times n}$ and for $0\leq k\leq n$, $1\leq j\leq n$,

$(A^{\omega,k})_{j}=\sum_{(j_{1},j_{2},\dots)\in
P_{k}}A_{j,j_{1}}A_{j_{1},j_{2}}A_{j_{2},j_{3}}\dots\,.$

Observe that again $A^{\omega,0}=0$ and $A^{\omega,n}=A^{\omega}$.

In the next lemma, we use the following summation identity: Assume that
$A_{1},A_{2},\dots$ are matrices in $S^{n\times n}$. Then for $0\leq k\leq n$,
$1\leq j\leq n$, and $m\geq 1$,

$\displaystyle\sum_{(j_{1},j_{2},\dots)\in
P_{k}}(A_{1})_{j,j_{1}}(A_{2})_{j_{1},j_{2}\dots}=$ $\displaystyle\sum_{1\leq
j_{1},\dots,j_{m}\leq
n}(A_{1})_{j,j_{1}}\dots(A_{m})_{j_{m-1},j_{m}}\sum_{(j_{m+1},j_{m+2},\dots)\in
P_{k}}(A_{m+1})_{j_{m},j_{m+1}}\dots\,.$

######  Lemma 6.

Let $(S,V)$ be a complete semiring-semimodule pair. Let $M\in(S^{n\times
n})^{\Gamma^{*}\times\Gamma^{*}}$ be a roc-matrix and $0\leq k\leq n$. Then

$(M^{\omega,k})_{p^{2}}\ =\
(M^{\omega,k})_{p}+(M^{*})_{p,\varepsilon}(M^{\omega,k})_{p}\,.$

######  Proof 3.4.

We use the proof of Lemma 3, i.e., the proof for the case
$M^{\omega,n}=M^{\omega}$. For $1\leq j\leq n$, we obtain
$((M^{\omega,k})_{p^{2}})_{j}=$

$\displaystyle\sum_{i_{1},i_{2},\dots\geq 2}\sum_{(j_{1},j_{2},\dots)\in
P_{k}}(M_{p,p^{i_{1}-1}})_{j,j_{1}}(M_{p^{i_{1}-1},p^{i_{2}-1}})_{j_{1},j_{2}}\dots+$
$\displaystyle\Big{(}\sum_{1\leq j^{\prime}\leq n}\sum_{m\geq
0}\sum_{k_{1},k_{2},\dots,k_{m}\geq 2}\sum_{1\leq j_{1},\dots,j_{m}\leq
n}\\!\\!(M_{p,p^{k_{1}-1}})_{j,j_{1}}\dots(M_{p^{k_{m}-1},\varepsilon})_{j_{m},j^{\prime}}\Big{)}\
\cdot$ $\displaystyle\Big{(}\sum_{k_{m+2},k_{m+3},\dots\geq
1}\sum_{(j_{m+2},j_{m+3},\dots)\in
P_{k}}\\!\\!(M_{p,p^{k_{m+2}}})_{j^{\prime},j_{m+2}}(M_{p^{k_{m+2}},p^{k_{m+3}}})_{j_{m+2},j_{m+3}}\dots\Big{)}=$
$\displaystyle((M^{\omega,k})_{p})_{j}+\sum_{1\leq j^{\prime}\leq
n}((M^{*})_{p,\varepsilon})_{j,j^{\prime}}((M^{\omega,k})_{p})_{j^{\prime}}=$
$\displaystyle((M^{\omega,k})_{p})_{j}+((M^{*})_{p,\varepsilon}(M^{\omega,k})_{p})_{j}=$
$\displaystyle((M^{\omega,k})_{p}+(M^{*})_{p,\varepsilon}(M^{\omega,k})_{p})_{j}\,.$

######  Theorem 7.

Let $(S,V)$ be a complete semiring-semimodule pair and let $M\in(S^{n\times
n})^{p^{*}\times p^{*}}$ be a roc-matrix. Then

$(M^{\omega,k})_{p}\ =\
(M_{p,p^{2}}+M_{p,p^{2}}(M^{*})_{p,\varepsilon}+M_{p,p})(M^{\omega,k})_{p}\,,$

for all $0\leq k\leq n$.

######  Proof 3.5.

We obtain, by Lemma 6, for all $0\leq k\leq n$,

$\displaystyle(M_{p,p^{2}}+M_{p,p^{2}}(M^{*})_{p,\varepsilon}+M_{p,p})(M^{\omega,k})_{p}$
$\displaystyle=\quad$ $\displaystyle
M_{p,p^{2}}((M^{\omega,k})_{p}+(M^{*})_{p,\varepsilon}(M^{\omega,k})_{p})+M_{p,p}(M^{\omega,k})_{p}$
$\displaystyle=\quad$ $\displaystyle
M_{p,p^{2}}(M^{\omega,k})_{p^{2}}+M_{p,p}(M^{\omega,k})_{p}\ =\
(MM^{\omega,k})_{p}\ =\ (M^{\omega,k})_{p}\,.$

######  Corollary 8.

Let $M\in(S^{n\times n})^{p^{*}\times p^{*}}$ be a roc-matrix. Then, for all
$0\leq k\leq n$, $(M^{\omega,k})_{p}$ is a solution of

$z=(M_{p,p^{2}}+M_{p,p^{2}}(M^{*})_{p,\varepsilon}+M_{p,p})z\,.$

##  4\. $\omega$-restricted one-counter automata

In this section, we define $\omega$-roc automata as a special case of
$\omega$-pushdown automata. We show that for an $\omega$-roc automaton
$\mathcal{C}$ there exists an algebraic system over a complete semiring-
semimodule pair such that the behavior $\|\mathcal{C}\|$ of $\mathcal{C}$ is a
component of a solution of this system.

In the sequel, $(S,V)$ is a complete semiring-semimodule pair and $S^{\prime}$
is a subset of $S$ containing $0$ an $1$. An _$S^{\prime}$ -$\omega$-pushdown
automaton_

$\mathcal{P}=(n,\Gamma,I,M,P,p_{0},k)$

is given by

  1. (i)

a finite set of _states_ $\\{1,\dots,n\\}$, $n\geq 1$,

  2. (ii)

an alphabet $\Gamma$ of _pushdown symbols_ ,

  3. (iii)

a _pushdown transition matrix_ $M\in({S^{\prime}}^{n\times
n})^{\Gamma^{*}\times\Gamma^{*}}$,

  4. (iv)

an _initial state vector_ $I\in{S^{\prime}}^{1\times n}$,

  5. (v)

a _final state vector_ $P\in{S^{\prime}}^{n\times 1}$,

  6. (vi)

an _initial pushdown symbol_ $p_{0}\in\Gamma$,

  7. (vii)

a set of _repeated states_ $\\{1,\dots,k\\}$, $0\leq k\leq n$.

The definition of a pushdown transition matrix is given at the beginning of
Section 3. (See also Kuich, Salomaa [16], Kuich [15] and Ésik, Kuich [11].)
Clearly, any roc-matrix is a pushdown transition matrix.

The _behavior of $\mathcal{P}$_ is an element of $S\times V$ and is defined by

$\|\mathcal{P}\|=(I(M^{*})_{p_{0},\varepsilon}P,I(M^{\omega,k})_{p_{0}})\,.$

Here $I(M^{*})_{p_{0},\varepsilon}P$ is the behavior of the
$S^{\prime}$-$\omega$-pushdown automaton
$\mathcal{P}_{1}=(n,\Gamma,I,M,P,p_{0},0)$ and $I(M^{\omega,k})_{p_{0}}$ is
the behavior of the $S^{\prime}$-$\omega$-pushdown automaton
$\mathcal{P}_{2}=(n,\Gamma,I,M,0,p_{0},k)$. Observe that $\mathcal{P}_{2}$ is
an automaton with the Büchi acceptance condition: if $G$ is the graph with
adjacency matrix $M$, then only paths that visit the repeated states
${1,\dots,k}$ infinitely often contribute to $\|\mathcal{P}_{2}\|$.
Furthermore, $\mathcal{P}_{1}$ contains no repeated states and behaves like an
ordinary $S^{\prime}$-pushdown automaton.

An $S^{\prime}$-$\omega$-roc automaton is an $S^{\prime}$-$\omega$-pushdown
automaton with just one pushdown symbol such that its pushdown matrix is a
roc-matrix.

In the sequel, an $S^{\prime}$-$\omega$-roc automaton
$\mathcal{P}=(n,\\{p\\},I,M,P,p,k)$ is denoted by $\mathcal{C}=(n,I,M,P,k)$
with behavior

$\|\mathcal{C}\|=(I(M^{*})_{p,\varepsilon}P,I(M^{\omega,k})_{p})\,.$

######  Remark 9.

Consider an $S^{\prime}$-$\omega$-pushdown automaton $\mathcal{P}$ with just
one pushdown symbol. By the construction in the proof of Theorem 13.28 of
Kuich, Salomaa [16], an $S^{\prime}$-$\omega$-roc automaton $\mathcal{C}$ can
be constructed such that $\|\mathcal{C}\|=\|\mathcal{P}\|$.

The next definitions and results are taken from Ésik, Kuich [11, Section 5.6]

For the definition of an $S^{\prime}$-algebraic system over a quemiring
$S\times V$ we refer the reader to [11], page 136, and for the definition of
quemirings to [11], page 110. Here we note that a quemiring $T$ is isomorphic
to a quemiring $S\times V$ determined by the semiring-semimodule pair $(S,V)$,
cf. [11], page 110.

Observe that the forthcoming system (1) is a system over the quemiring
$S^{n\times n}\times V^{n}$. Compare the forthcoming algebraic system (2) with
the algebraic systems occurring in the proofs of Theorem 14.15 of Kuich,
Salomaa [16] and Theorem 6.4 of Kuich [15], both in the case of a roc-matrix.

Let $M$ be a roc-matrix. Consider the ${S^{\prime}}^{n\times n}$-algebraic
system over the complete semiring-semimodule pair $(S^{n\times n},V^{n})$

$y\ =\ M_{p,p^{2}}yy+M_{p,p}y+M_{p,\varepsilon}\,.$ (1)

Then by Theorem 5.6.1 of Ésik, Kuich [11] $(A,U)\in(S^{n\times n},V^{n})$ is a
solution of (1) iff $A$ is a solution of the ${S^{\prime}}^{n\times
n}$-algebraic system over $S^{n\times n}$

$x=M_{p,p^{2}}xx+M_{p,p}x+M_{p,\varepsilon}$ (2)

and $U$ is a solution of the $S^{n\times n}$-linear system over $V^{n}$

$z=M_{p,p^{2}}z+M_{p,p^{2}}Az+M_{p,p}z\,.$ (3)

######  Theorem 10.

Let $S$ be a complete starsemiring and $M$ be a roc-matrix. Then
$(M^{*})_{p,\varepsilon}$ is a solution of the ${S^{\prime}}^{n\times
n}$-algebraic system (2). If $S$ is a continuous starsemiring, then
$(M^{*})_{p,\varepsilon}$ is the least solution of (2).

######  Proof 4.1.

We obtain, by Theorem 1

$\displaystyle
M_{p,p^{2}}(M^{*})_{p,\varepsilon}(M^{*})_{p,\varepsilon}+M_{p,p}(M^{*})_{p,\varepsilon}+M_{p,\varepsilon}$
$\displaystyle=\ $ $\displaystyle
M_{p,p^{2}}(M^{*})_{p^{2},\varepsilon}+M_{p,p}(M^{*})_{p,\varepsilon}+M_{p,\varepsilon}$
$\displaystyle=\ $
$\displaystyle(MM^{*})_{p,\varepsilon}=(M^{+})_{p,\varepsilon}=(M^{*})_{p,\varepsilon}\,.$

This proves the first sentence of our theorem. The second sentence of Theorem
10 is proved by Theorem 6.4 of Kuich [15].

######  Theorem 11.

Let $(S,V)$ be a complete semiring-semimodule pair and $M$ be a roc-matrix.
Then

$((M^{*})_{p,\varepsilon},(M^{\omega,k})_{p})\,,$

is a solution of the ${S^{\prime}}^{n\times n}$-algebraic system (1), for each
$0\leq k\leq n$.

######  Proof 4.2.

Let $0\leq k\leq n$, and consider the $S^{n\times n}$-linear system

$z=(M_{p,p^{2}}+M_{p,p^{2}}(M^{*})_{p,\varepsilon}+M_{p,p})z\,.$

By Corollary 8, $(M^{\omega,k})_{p}$ is a solution of this system. Hence, by
Theorem 5.6.1 of Ésik, Kuich [11] (see the remark above) and Theorem 10,
$((M^{*})_{p,\varepsilon},(M^{\omega,k})_{p})$ is a solution of the system
(1).

Observe that, if $S$ is a continuous semiring, then the $S^{n\times n}$-linear
system in the proof of Theorem 11 is in fact an
$\mathfrak{Alg}({S^{\prime}})^{n\times n}$-linear system (see Kuich [15, p.
623]).

######  Theorem 12.

Let $(S,V)$ be a complete semiring-semimodule pair and let
$\mathcal{C}=(n,I,M,P,k)$ be an $S^{\prime}$-$\omega$-roc-automaton. Then
$(\|\mathcal{C}\|,((M^{*})_{p,\varepsilon},(M^{\omega,k})_{p}))$ is a solution
of the ${S^{\prime}}^{n\times n}$-algebraic system

$y_{0}=IyP\ ,\quad y=M_{p,p^{2}}yy+M_{p,p}y+M_{p,\varepsilon}$ (4)

over the complete semiring-semimodule pair $(S^{n\times n},V^{n})$.

######  Proof 4.3.

By Theorem 11, $((M^{*})_{p,\varepsilon},(M^{\omega,k})_{p})$ is a solution of
the second equation. Since

$I((M^{*})_{p,\varepsilon},(M^{\omega,k})_{p})P=(I(M^{*})_{p,\varepsilon}P,I(M^{\omega,k})_{p})=\|\mathcal{C}\|\,,$

$(\|\mathcal{C}\|,((M^{*})_{p,\varepsilon},(M^{\omega,k})_{p}))$ is a solution
of the given ${S^{\prime}}^{n\times n}$-algebraic system.

Let now $S$ be a complete star-omega semiring and $\Sigma$ be an alphabet.
Then by Theorem 5.5.5 of Ésik, Kuich [11],
$(S\ll\\!\Sigma^{*}\\!\gg,S\ll\\!\Sigma^{\omega}\\!\gg)$ is a complete
semiring-semimodule pair.

Let $\mathcal{C}\\!=\\!(n,I,M,P,k)$ be an
$S\langle\Sigma\cup\\{\varepsilon\\}\rangle$-$\omega$-roc automaton. Consider
the algebraic system (4) over the complete semiring-semimodule pair
${((S\ll\\!\Sigma^{*}\\!\gg)^{n\times
n},}\allowbreak{(S\ll\\!\Sigma^{\omega}\\!\gg)^{n})}$ and the mixed algebraic
system (5) over ${((S\ll\Sigma^{*}\gg)^{n\times n},}$
${(S\ll\Sigma^{\omega}\gg)^{n})}$ induced by (4)

$\displaystyle x_{0}$ $\displaystyle=IxP,\qquad$ $\displaystyle x$
$\displaystyle=M_{p,p^{2}}xx+M_{p,p}x+M_{p,\varepsilon}\,,$ (5) $\displaystyle
z_{0}$ $\displaystyle=Iz,$ $\displaystyle z$
$\displaystyle=M_{p,p^{2}}z+M_{p,p^{2}}xz+M_{p,p}z\,.$

Then, by Theorem 12,

$(I(M^{*})_{p,\varepsilon}P,(M^{*})_{p,\varepsilon},I(M^{\omega,k})_{p},(M^{\omega,k})_{p}),\
0\leq k\leq n,$

is a solution of (5). It is called _solution of order $k$_. Hence, we have
proved the next theorem.

######  Theorem 13.

Let $S$ be a complete star-omega semiring and $\mathcal{C}=(n,I,M,P,k)$ be an
$S\langle\Sigma\cup\\{\varepsilon\\}\rangle$-$\omega$-roc automaton. Then
$(I(M^{*})_{p,\varepsilon}P,(M^{*})_{p,\varepsilon},I(M^{\omega,k})_{p},(M^{\omega,k})_{p}),\
0\leq k\leq n$, is a solution of the mixed algebraic system (5). ∎

Let now in (5)

$x=([i,p,j])_{1\leq i,j\leq n}$

be an $n\times n$-matrix of variables and

$z=([i,p])_{1\leq i\leq n}$

be an $n$-dimensional column vector of variables. If we write the mixed
algebraic system (5) component-wise, we obtain a mixed algebraic system over
$({(S\ll\Sigma^{*}\gg),}{(S\ll\Sigma^{\omega}\gg)})$ with variables $[i,p,j]$
over $S\ll\Sigma^{*}\gg$, where $1\leq i,j\leq n$, and variables $[i,p]$ over
$S\ll\Sigma^{\omega}\gg$, where $1\leq i\leq n$. Observe that we do not really
need $p$ in the notation of the variables. But we want to save the form of the
triple construction in connection with pushdown automata.

Let

$M_{p,p^{2}}=(a_{ij})_{1\leq i,j,\leq n},M_{p,p}=(c_{ij})_{1\leq i,j,\leq
n},M_{p,\varepsilon}=(b_{ij})_{1\leq i,j,\leq n}$

and write (5) with the matrices $x$ and $z$ of variables component-wise then
we obtain:

$\displaystyle x_{0}$ $\displaystyle=$ $\displaystyle\sum_{1\leq
m_{1},m_{2}\leq n}I_{m_{1}}[m_{1},p,m_{2}]P_{m_{2}}$ (6)
$\displaystyle[i,p,j]$ $\displaystyle=$ $\displaystyle\sum_{1\leq
m_{1},m_{2}\leq n}a_{im_{1}}[m_{1},p,m_{2}][m_{2},p,j]+$
$\displaystyle\sum_{1\leq m\leq n}c_{im}[m,p,j]+b_{ij}$ $\displaystyle z_{0}$
$\displaystyle=$ $\displaystyle\sum_{1\leq m\leq n}I_{m}[m,p]$
$\displaystyle[i,p]$ $\displaystyle=$ $\displaystyle\sum_{1\leq m\leq
n}a_{im}[m,p]+\sum_{1\leq m_{1},m_{2}\leq
n}a_{im_{1}}[m_{1},p,m_{2}][m_{2},p]+$ $\displaystyle\sum_{1\leq m\leq
n}c_{im}[m,p]$

for all $1\leq i,j\leq n$.

######  Theorem 14.

Let $S$ be a complete star-omega semiring and $\mathcal{C}=(n,I,M,P,k)$ be an
$S\langle\Sigma\cup\\{\varepsilon\\}\rangle$-$\omega$-roc automaton. Then

$(\sigma_{0},((M^{*})_{p,\varepsilon})_{ij},\tau_{0},(M^{\omega,k})_{p})$

is a solution of the system (6) with $\|\mathcal{C}\|=(\sigma_{0},\tau_{0})$ .

######  Proof 4.4.

By Theorem 13.

##  5\. Mixed algebraic systems and mixed context-free grammars

In this section we associate a mixed context-free grammar with finite and
infinite derivations to the algebraic system (6). The language generated by
this mixed context-free grammar is then the behavior $\|\mathcal{C}\|$ of the
$\omega$-roc automaton $\mathcal{C}$. The construction of the mixed context-
free grammar from the $\omega$-roc automaton $\mathcal{C}$ is a generalization
of the well-known triple construction in case of roc automata and is called
now _triple-pair construction for $\omega$-roc automata_. We will consider the
commutative complete star-omega semirings
$\mathbb{B}=(\\{0,1\\},\vee,\land,*,0,1)$ with $0^{*}=1^{*}=1$ and
$\mathbb{N}^{\infty}=(\mathbb{N}\cup\\{\infty\\},+,\cdot,^{*},0,1)$ with
$0^{*}=1$ and $a^{*}=\infty$ for $a\neq\infty$.

If $S=\mathbb{B}$ or $S=\mathbb{N}^{\infty}$ and $1\leq k\leq n$, then we
associate to the mixed algebraic system (6) over
$((S\ll\Sigma^{*}\gg),(S\ll\Sigma^{\omega}\gg))$ the _mixed context-free
grammar_

$G_{k}\ =\ (X,Z,\Sigma,P_{X},P_{Z},x_{0},z_{0},k)\,.$

(See also Ésik, Kuich [11, page 139].) Here

  1. (i)

$X=\\{x_{0}\\}\cup\\{[i,p,j]\mid 1\leq i,j\leq n\\}$ is a set of _variables
for finite derivations_ ;

  2. (ii)

$Z=\\{z_{0}\\}\cup\\{[i,p]\mid 1\leq i\leq n\\}$ is a set of _variables for
infinite derivations_ ;

  3. (iii)

$\Sigma$ is an alphabet of _terminal symbols_ ;

  4. (iv)

$P_{X}$ is a finite set of _productions for finite derivations_ given below;

  5. (v)

$P_{Z}$ is a finite set of _productions for infinite derivations_ given below;

  6. (vi)

$x_{0}$ is the _start variable for finite derivations_ ;

  7. (vii)

$z_{0}$ is the _start variable for infinite derivations_ ;

  8. (viii)

$\\{[i,p]\mid 1\leq i\leq k\\}$ is the set of _repeated variables for infinite
derivations_.

In the definition of $G_{k}$ the sets $P_{X}$ and $P_{Z}$ are as follows:

$\displaystyle P_{X}=\ $ $\displaystyle\\{x_{0}\to a[m_{1},p,m_{2}]b\mid$
$\displaystyle\ \ (I_{m_{1}},a)\cdot(P_{m_{2}},b)\neq
0,a,b\in\Sigma\cup\\{\varepsilon\\},1\leq m_{1},m_{2}\leq n\\}\ \cup$
$\displaystyle\\{[i,p,j]\to a[m_{1},p,m_{2}][m_{2},p,j]\mid$ $\displaystyle\ \
(a_{im_{1}},a)\neq 0,a\in\Sigma\cup\\{\varepsilon\\},1\leq i,j,m_{1},m_{2}\leq
n\\}\ \cup$ $\displaystyle\\{[i,p,j]\to a[m,p,j]\mid(c_{im},a)\neq
0,a\in\Sigma\cup\\{\varepsilon\\},1\leq i,j,m\leq n\\}\ \cup$
$\displaystyle\\{[i,p,j]\to a\mid(b_{ij},a)\neq
0,a\in\Sigma\cup\\{\varepsilon\\},1\leq i,j\leq n\\}\,,$ $\displaystyle
P_{Z}=\ $ $\displaystyle\\{z_{0}\to a[m,p]\mid(I_{m},a)\neq
0,a\in\Sigma\cup\\{\varepsilon\\},1\leq m\leq n\\}\ \cup$
$\displaystyle\\{[i,p]\to a[m,p]\mid(a_{im},a)\neq
0,a\in\Sigma\cup\\{\varepsilon\\},1\leq i,m\leq n\\}\ \cup$
$\displaystyle\\{[i,p]\to a[m_{1},p,m_{2}][m_{2},p]\mid$ $\displaystyle\ \
(a_{im_{1}},a)\neq 0,a\in\Sigma\cup\\{\varepsilon\\},1\leq i,m_{1},m_{2}\leq
n\\}\ \cup$ $\displaystyle\\{[i,p]\to a[m,p]\mid(c_{im},a)\neq
0,a\in\Sigma\cup\\{\varepsilon\\},1\leq i,m\leq n\\}\,.$

A _finite leftmost derivation_ $\alpha_{1}\Rightarrow_{\\!L}^{*}\alpha_{2}$,
where $\alpha_{1},\alpha_{2}\in(X\cup\Sigma)^{*}$, by productions in $P_{X}$
is defined as usual. An _infinite (leftmost) derivation_
$\pi:z_{0}\Rightarrow_{\\!L}^{\omega}w$, for $z_{0}\in Z,w\in\Sigma^{\omega}$,
is defined as follows:

$\displaystyle\pi:\ $ $\displaystyle
z_{0}\Rightarrow_{\\!L}\alpha_{0}[{i_{0}},p]\Rightarrow_{\\!L}^{*}w_{0}[i_{0},p]\Rightarrow_{\\!L}w_{0}\alpha_{1}[i_{1},p]\Rightarrow_{\\!L}^{*}w_{0}w_{1}[{i_{1}},p]\Rightarrow_{\\!L}\dots$
$\displaystyle\Rightarrow_{\\!L}^{*}w_{0}w_{1}\dots
w_{m}[{i_{m}},p]\Rightarrow_{\\!L}w_{0}w_{1}\dots
w_{m}\alpha_{m+1}[{i_{m+1}},p]\Rightarrow_{\\!L}^{*}\dots\,,$

where
$z_{0}\to\alpha_{0}[{i_{0}},p],[{i_{0}},p]\to\alpha_{1}[{i_{1}},p],\dots,[{i_{m}},p]\to\alpha_{m+1}[{i_{m+1}},p],\dots$
are productions in $P_{Z}$ and $w=w_{0}w_{1}\dots w_{m}\dots$.

We now define an infinite derivation
$\pi_{k}:z_{0}\Rightarrow_{\\!L}^{\omega,k}w$ for $0\leq k\leq n$, $z_{0}\in
Z$, $w\in\Sigma^{\omega}$: We take the above definition
$\pi:z_{0}\Rightarrow^{\omega}w$ and consider the sequence of the first
elements of the variables of $X$ that are rewritten in the finite leftmost
derivation $\alpha_{m}\Rightarrow_{L}^{*}w_{m}$, $m\geq 0$. Assume this
sequence is $i_{m}^{1},i_{m}^{2},\dots,i_{m}^{t_{m}}$ for some $t_{m}$, $m\geq
1$. Then, to obtain $\pi_{k}$ from $\pi$, the condition
$i_{0},i_{1}^{1},\dots,i_{1}^{t_{1}},i_{1},i_{2}^{1},\dots,i_{2}^{t_{2}},i_{2},\dots,i_{m},i_{m+1}^{1},\dots,i_{m+1}^{t_{m+1}},i_{m+1},\dots\in
P_{k}$ has to be satisfied.

Then

$L(G_{k})=\\{w\in\Sigma^{*}\mid x_{0}\Rightarrow_{\\!L}^{*}w\\}\ \cup\
\\{w\in\Sigma^{\omega}\mid\pi:z_{0}\Rightarrow_{\\!L}^{\omega,k}w\\}\,.$

Observe that the construction of $G_{k}$ from $\mathcal{C}$ is nothing else
than a generalization of the triple construction in the case of a roc-
automaton, if $\mathcal{C}$ is viewed as a pushdown automaton, since the
construction of the context-free grammar $G=(X,\Sigma,P_{X},x_{0})$ is the
triple construction. (See Harrison [14], Theorem 5.4.3; Bucher, Maurer [3],
Sätze 2.3.10, 2.3.30; Kuich, Salomaa [16], pages 178, 306; Kuich [15], page
642; Ésik, Kuich [11], pages 77, 78.)

We call the construction of the mixed context-free grammar $G_{k}$, for $0\leq
k\leq n$, from $\mathcal{C}$ the _triple-pair construction for $\omega$-roc
automata_. This is justified by the definition of the sets of variables
$\\{[i,p,j]\mid 1\leq i,j,\leq n\\}$ and $\\{[i,p]\mid 1\leq i\leq n\\}$ of
$G_{k}$ and by the forthcoming Corollary 16.

In the next theorem we use the isomorphism between
${\mathbb{B}\ll\Sigma^{*}\gg}\times{\mathbb{B}\ll\Sigma^{\omega}\gg}$ and
$2^{\Sigma^{*}}\times 2^{\Sigma^{\omega}}$.

######  Theorem 15.

Assume that $(\sigma,\tau)$ is the solution of order $k$ of the mixed
algebraic system (6) over
$(\mathbb{B}\ll\Sigma^{*}\gg,\mathbb{B}\ll\Sigma^{\omega}\gg)$ for
$k\in\\{0,\dots,n\\}$. Then

$L(G_{k})\ =\ \sigma_{x_{0}}\cup\tau_{z_{0}}\,.$

######  Proof 5.1.

By Theorem<EMAIL_ADDRESS>of Salomaa, Soittola [18] and by Theorem 14, we obtain
$\sigma_{x_{0}}=\\{w\in\Sigma^{*}\mid x_{0}\Rightarrow_{\\!L}^{*}w\\}$. We now
show that $\tau_{z_{0}}$ is generated by the infinite derivations
$\Rightarrow_{\\!L}^{\omega,k}$ from $z_{0}$. First observe that the rewriting
by the typical $[i,p,j]$\- and $[i,p]$\- production corresponds to the
situation that in the graph of the $\omega$-restricted one counter automaton
$\mathcal{C}$ the edge from $(p\rho,i)$ to $(pp\rho,j),(p\rho,j)$ or
$(\rho,j)$, $\rho=p^{t}$ for some $t\geq 0$ is passed after the state $i$ is
visited. The first step of the infinite derivation $\pi_{k}$ is given by
$z_{0}\Rightarrow_{\\!L}\alpha_{0}[i_{0},p]$ and indicates that the path in
the graph of $\mathcal{C}$ corresponding to $\pi_{k}$ starts in state $i_{0}$.
Furthermore, the sequence of the first elements of variables that are
rewritten in $\pi_{k}$, i.e.,
$i_{0},i_{1}^{1},\dots,i_{1}^{t_{1}},i_{1},i_{2}^{2},\dots,i_{2}^{t_{2}},i_{2},\dots,i_{m},i_{m+1}^{1},\dots,i_{m+1}^{t_{m+1}},i_{m+1},\dots$
indicates that the path in the graph of $\mathcal{C}$ corresponding to
$\pi_{k}$ visits these states. Since this sequence is in $P_{k}$ the
corresponding path contributes to $\|\mathcal{C}\|$. Hence, by Theorem 14 we
obtain

$\tau_{z_{0}}=\\{w\in\Sigma^{\omega}\mid\pi:z_{0}\Rightarrow_{\\!L}^{*}w\\}\,.$

######  Corollary 16.

Assume that, for some $k\in\\{0,\dots,n\\}$, the mixed context free grammar
$G_{k}$ associated to the mixed algebraic system (6) is constructed from the
$\mathbb{B}\langle\Sigma\cup\\{\varepsilon\\}\rangle$-$\omega$-roc automaton
$\mathcal{C}$. Then

$L(G_{k})=\|\mathcal{C}\|\,.$

######  Proof 5.2.

By Theorems 14 and 15.

For the remainder of this section our basic semiring is $\mathbb{N}^{\infty}$,
which allows us to draw some stronger conclusions.

######  Theorem 17.

Assume that $(\sigma,\tau)$ is the solution of order $k$ of the mixed
algebraic system (6) over
$(\mathbb{N}^{\infty}\ll\Sigma^{*}\gg,\mathbb{N}^{\infty}\ll\Sigma^{\omega}\gg)$,
$k\in\\{0,\dots,n\\}$, where
$I_{m_{1}},P_{m_{1}},a_{m_{1}m_{2}},b_{m_{1}m_{2}},c_{m_{1}m_{2}}$, $1\leq
m_{1},m_{2}\leq n$ are in
$\\{0,1\\}\langle\Sigma\cup\\{\varepsilon\\}\rangle$. Denote by $d(w)$, for
$w\in\Sigma^{*}$, the number (possibly $\infty$) of distinct finite leftmost
derivations of $w$ from $x_{0}$ with respect to $G_{k}$; and by $c(w)$, for
$w\in\Sigma^{\omega}$, the number (possibly $\infty$) of distinct infinite
leftmost derivations $\pi$ of $w$ from $z_{0}$ with respect to $G_{k}$. Then

$\sigma_{x_{0}}=\sum_{w\in\Sigma^{*}}d(w)w\qquad\text{\ and \
}\qquad\tau_{z_{0}}=\sum_{w\in\Sigma^{\omega}}c(w)w\,.$

######  Proof 5.3.

By Theorem<EMAIL_ADDRESS>of Salomaa, Soittola [18], Theorems 5.5.9 and 5.6.3 of
Ésik, Kuich [11] and Theorem 14.

In the forthcoming Corollary 18 we consider, for a given
$\\{0,1\\}\langle\Sigma\cup\\{\varepsilon\\}\rangle$-$\omega$-roc automaton
$\mathcal{C}=(n,I,M,P,k)$ the number of distinct computations from an initial
instantaneous description $(i,w,p)$ for $w\in\Sigma^{*}$, $I_{i}\neq 0$, to an
accepting instantaneous description $(j,\varepsilon,\varepsilon)$, with
$P_{j}\neq 0$, $i,j\in\\{0,\dots,n\\}$.

Here $(i,w,p)$ means that $\mathcal{C}$ starts in the initial state $i$ with
$w$ on its input tape and $p$ on its pushdown tape; and
$(j,\varepsilon,\varepsilon)$ means that $\mathcal{C}$ has entered the final
state $j$ with empty input tape and empty pushdown tape.

Furthermore, we consider the number of distinct infinite computations starting
in an initial instantaneous description $(i,w,p)$ for $w\in\Sigma^{\infty}$,
$I_{i}\neq 0$.

######  Corollary 18.

Assume that, for some $k\in\\{0,\dots,n\\}$, the mixed context-free grammar
$G_{k}$ associated to the mixed algebraic system (6) is constructed from the
$\\{0,1\\}\langle\Sigma\cup\\{\varepsilon\\}\rangle$-$\omega$-roc automaton
$\mathcal{C}$. Then the number (possibly $\infty$) of distinct finite leftmost
derivations of $w\in\Sigma^{*}$ from $x_{0}$ equals the number of distinct
finite computations from an initial instantaneous description for $w$ to an
accepting instantaneous description; moreover, the number (possibly $\infty$)
of distinct infinite (leftmost) derivations of $w\in\Sigma^{\omega}$ from
$z_{0}$ equals the number of distinct infinite computations starting in an
initial instantaneous description for $w$.

######  Proof 5.4.

By Corollary 3.4.12 of Ésik, Kuich [11, Theorem 4.3] and the definition of
infinite derivations with respect to $G_{k}$.

The context-free grammar $G_{k}$ associated to (6) is called _unambiguous_ if
each $w\in L(G)$, $w\in\Sigma^{*}$ has a unique finite leftmost derivation and
each $w\in L(G)$, $w\in\Sigma^{\omega}$, has a unique infinite (leftmost)
derivation.

An $\mathbb{N}^{\infty}\langle\Sigma\cup\\{\varepsilon\\}\rangle$-$\omega$-roc
automaton $\mathcal{C}$ is called _unambiguous_ if
$(\|\mathcal{C}\|,w)\in\\{0,1\\}$ for each
$w\in\Sigma^{*}\cup\Sigma^{\omega}$.

######  Corollary 19.

Assume that, for some $k\in\\{0,\dots,n\\}$, the mixed context-free grammar
$G_{k}$ associated to the mixed algebraic system (6) is constructed from the
$\\{0,1\\}\langle\Sigma\cup\\{\varepsilon\\}\rangle$-$\omega$-roc automaton
$\mathcal{C}$. Then $G_{k}$ is unambiguous iff $\|\mathcal{C}\|$ is
unambiguous.

In the forthcoming paper Droste, Ésik, Kuich [5] we extend the results of this
paper to weighted $\omega$-pushdown automata and obtain the triple-pair
construction for them. In the classical theory this triple-pair constructions
extends the well-known triple construction that, given an $\omega$-pushdown
automaton, yields an equivalent context-free grammar.

## Acknowledgment

The ideas of and personal discussions with Zoltán Ésik were of great influence
in preparing this paper. Thanks are due to two unknown referees for their
helpful remarks.

## References

  * [1] Berstel, J.: Transductions and Context-Free Languages. Teubner, 1979.
  * [2] Bloom, S. L., Ésik, Z.: Iteration Theories. EATCS Monographs on Theoretical Computer Science. Springer, 1993.
  * [3] Bucher, W., Maurer, H.: Theoretische Grundlagen der Programmiersprachen. B. I. Wissenschaftsverlag, 1984.
  * [4] Conway, J. H.: Regular Algebra and Finite Machines. Chapman & Hall, 1971\.
  * [5] Droste, M., Ésik, Z., Kuich, W.: The triple-pair construction for weighted $\omega$-pushdown automata. In: Automata and Formal Languages (AFL 2017), EPTCS (2017) 101-113.
  * [6] Eilenberg, S.: Automata, Languages and Machines. Vol. A. Academic Press, 1974.
  * [7] Ésik, Z., Kuich, W.: A semiring-semimodule generalization of $\omega$-context-free languages. In: Theory is Forever (Eds.: J. Karhumäki, H. Maurer, G. Paun, G. Rozenberg), LNCS 3113, Springer, 2004, 68–80.
  * [8] Ésik, Z., Kuich, W.: A semiring-semimodule generalization of $\omega$-regular languages II. Journal of Automata, Languages and Combinatorics 10 (2005) 243–264.
  * [9] Ésik, Z., Kuich, W.: On iteration semiring-semimodule pairs. Semigroup Forum 75 (2007), 129–159.
  * [10] Ésik, Z., Kuich, W.: A semiring-semimodule generalization of transducers and abstract $\omega$-families of power series. Journal of Automata, Languages and Combinatorics, 12 (2007), 435–454.
  * [11] Ésik, Z., Kuich, W.: Modern Automata Theory. http://www.dmg.tuwien.ac.at/kuich
  * [12] Ésik, Z., Kuich, W.: Continuous semiring-semimodule pairs and mixed algebraic systems. Acta Cybernetica 252 (2017) 43-59.
  * [13] Greibach S. A.: An infinite hierarchy of context-free languages. Journal of the ACM 16 (1969) 91–106.
  * [14] Harrison, M. A.: Introduction to Formal Language Theory. Addison-Wesley, 1978.
  * [15] Kuich, W.: Semirings and formal power series: Their relevance to formal languages and automata theory. In: Handbook of Formal Languages (Eds.: G. Rozenberg and A. Salomaa), Springer, 1997, Vol. 1, Chapter 9, 609–677.
  * [16] Kuich, W., Salomaa, A.: Semirings, Automata, Languages. EATCS Monographs on Theoretical Computer Science, Vol. 5. Springer, 1986.
  * [17] Perrin, D., Pin, J. - E.: Infinite Words – Automata, Semigroups, Logic and Games, Elsevier, 2004.
  * [18] Salomaa, A., Soittola, M.: Automata - Theoretic Aspects of Formal Power Series, Springer, 1978.