[fill = gray] (+0+,+0+) rectangle
[fill = white] (+0,+0) rectangle (+0.5,+0.8);
[fill = black] (+0.3,+0.6) rectangle (+0.5,+0.8);
(alpha) at (+0.25,+0.4) $\alpha$;
[-] (-0.4,+0.6) – (,+0.6);
[-] (-0.4,+0.3) – (,+0.3);
[-] (+0.5,+0.3) – (+1,+0.3);
[rounded corners=4pt,-] (-0.4,+-0.2) – (+1,+-0.2) ;
[-] (+0.5,+0.6) – (+1,+0.6);

[rounded corners=4pt,-] (+-0.2,+-0.2) – (+0.5,+-0.2) ;
[rounded corners=2pt,-] (+0.5,+0.1) – (+0.7,+0.1)

[-] (-0.4,+0.6) – (+0.3,+0.6);
[fill = black] (+0.3,+0.6) circle (0.1);
[-] (-0.4,+0.3) – (+0.3,+0.3);
[fill = black] (+0.3,+0.3) circle (0.1);
[rounded corners=4pt,-] (-0.4,+-0.2) – (+0.4,+-0.2) ;

[fill = white] (+0.8,+0.2) circle (0.15);
(v) at  (+0.8,+0.2) $\vee$;

[-] (-0.4,+0.6) – (+1,+0.6);
[-] (-0.4,+0.3) – (+1,+0.3);
[rounded corners=4pt,-] (-0.4,+-0.2) – (,+-0.2)–
(+0.5,+0.6)– (+1,+0.6);

[fill = gray] (+0+,+0+) rectangle
[fill = white] (+0,+0) rectangle (+0.5,+0.8);
[fill = black] (+0.3,+0.6) rectangle (+0.5,+0.8);
(alpha) at (+0.25,+0.4) $\alpha$;
[-] (-0.4,+0.6) – (,+0.6);
[-] (-0.4,+0.3) – (,+0.3);
[-] (+0.5,+0.3) – (+1,+0.3);

[-] (+0.5,+0.6) – (+1,+0.6);

[rounded corners=2pt,-] (+0.5,+0.1) – (+0.7,+0.1)

[-] (-0.4,+0.6) – (+0.3,+0.6);
[fill = black] (+0.3,+0.6) circle (0.1);
[-] (-0.4,+0.3) – (+0.3,+0.3);
[fill = black] (+0.3,+0.3) circle (0.1);
[rounded corners=4pt,-] (-0,+-0.2) – (+0.4,+-0.2) ;

Hence, by right distributivity w.r.t. the base morphisms we have
$[\perp,\mathsf{id}_{m}]\cdot \gamma '^2\cdot \mathsf{in}^{m}_{n+m} =
\mathsf{id}_{m} \vee r$ and $[\perp,\mathsf{id}_{m}]\cdot \gamma '^2\cdot
\mathsf{in}^{n} = [\perp,\mathsf{id}_{m}]\cdot \gamma '\cdot \mathsf{in}^{n}$.
Since $[\perp,\mathsf{id}_{m}]\cdot \gamma '\cdot \mathsf{in}^{m}_{n+m}
=\mathsf{id}_{m}$ we conclude that:

[\perp,\mathsf{id}_{m}]\cdot \gamma '^2\leq (\mathsf{id}\vee r)\cdot
[\perp,\mathsf{id}_{m}]\cdot \gamma'.

[\perp,\mathsf{id}_{m}]\cdot \gamma '^2  = [r',\mathsf{id}\vee r] \geq
[\perp,\mathsf{id}_{m} \vee r] = (\mathsf{id}\vee r)\cdot

for $r' \defeq [\perp,\mathsf{id}]\cdot\alpha^\ast$.
Note that $r'\cdot \mathsf{in}^{m}_{n} = r$.
Hence, to summarize:

(\mathsf{id}\vee r)\cdot [\perp,\mathsf{id}]=[\perp,\mathsf{id}\vee r] \leq
[r',\mathsf{id}\vee r]  \leq [\perp,\mathsf{id}]\cdot \gamma '^2 \leq
(\mathsf{id}\vee r)\cdot [\perp,\mathsf{id}]\cdot \gamma'.

If we let $f = [\perp,\mathsf{id}]$ and $g= f\cdot \gamma'$ then the above inequalities
are rephrased as follows:

(\mathsf{id}\vee r) \cdot f \leq f\cdot (\gamma')^2 \text{ and } g\cdot \gamma'
\leq (\mathsf{id} \vee r) \cdot g.

By (<ref>) in Lemma <ref>, (<ref>)
in Assumptions <ref> and  $\mathsf{id}\leq \gamma'$ we get:

r^\ast \cdot f \leq f\cdot \gamma'^\ast = g\cdot \gamma'^\ast \leq r^\ast \cdot g.

Since $f\cdot \mathsf{in}^m_{n+m} = g\cdot \mathsf{in}^m_{n+m} =\mathsf{id}_m$ and
$\gamma^\ast = \gamma'^\ast$ we get:
r^\ast = [\perp,\mathsf{id} ]\cdot  \gamma^\ast \cdot \mathsf{in}^m_{n+m}.
Similarily, we show
r^+ = [\perp,\mathsf{id}] \cdot
\gamma^\ast \cdot \mathsf{in}^n_{n+m} \cdot \mathsf{in}^m_n.
This proves that $r^+,r^\ast \in NF(\mathcal{A})$.

We are now ready to present the following proof.

(Theorem <ref>)
Note that all maps from $NF(\mathcal{A})$ are regular and
all regular maps are in $\mathfrak{Rat}(\mathcal{A})$.
By Lemma <ref>
morphisms from $NF(\mathcal{A})$ form a theory closed under
finite suprema and saturation. Hence,
$NF(\mathcal{A}) = \mathfrak{Reg}(\mathcal{A}) = \mathfrak{Rat}(\mathcal{A})$.
This completes the proof.

Before we proceed with the proof of Theorem <ref>
we require one extra statement. Let us define:

\begin{align*}
\omega\mathfrak{Rat}(\mathcal{A})(n) \defeq & \{ [r_1,\ldots, r_{m}]^\omega  \cdot r
\mid r\in \mathfrak{Reg}(n,m), r_i \in \mathfrak{Reg}(1,m)   \text{ for } m
<\omega   \},\\
\omega\mathfrak{Reg}(\mathcal{A})(n) \defeq & \{
||\alpha,\mathfrak{F}||_{\omega}\cdot \mathsf{in}^n_m:n\rightdcirc 0 \mid
(\alpha,\mathfrak{F}) \text{ is } \mathcal{A}\text{-aut.} \text{ with } \alpha:m\rightdcirc m\}.
\end{align*}

and  note that $\omega\mathfrak{Rat}(\mathcal{A}) = \omega\mathfrak{Rat}(\mathcal{A})(1)$ and
$\omega\mathfrak{Reg}(\mathcal{A})= \omega\mathfrak{Reg}(\mathcal{A})(1)$. Additionally,
the following holds.

For any $r\in \mathfrak{Reg}(m,m)$ we have:

$$r^\omega \in \omega\mathfrak{Reg}(\mathcal{A})(m).$$

All regular maps can be given in their normal form. Hence, we have

r=[\perp,\mathsf{id}_{m}]\cdot \alpha^\ast \cdot \mathsf{in}^{m}_n$$

for $\alpha:n\to n+m$, where
$m\leq n$. We depict $r$ by .08!

[fill = gray] (+0+,+0+) rectangle
[fill = white] (+0,+0) rectangle (+0.5,+0.8);
[fill = black] (+0.3,+0.6) rectangle (+0.5,+0.8);
[-] (-0.5,+0.6) – (,+0.6);

[-] (-0.4,+0.3) – (,+0.3);

[-] (+0.5,+0.3) – (+1,+0.3);
[fill = black] (+1,+0.3) circle (0.1);
[rounded corners=4pt,-] (-0.4,+-0.2) – (+1,+-0.2) ;
[-] (+0.5,+0.6) – (+1,+0.6);
[fill = black] (+1,+0.6) circle (0.1);
(alpha) at (+0.25,+0.4) $\alpha$;
[rounded corners=4pt,-] (+-0.2,+-0.2) – (+0.5,+-0.2) ;
[rounded corners=2pt,-] (+0.5,+0.1) – (+0.7,+0.1)

[fill = white] (-0.3,+0.3) circle (0.1);
[fill = white] (-0.3,-0.2) circle (0.1);

. Consider $\gamma$ defined by the following diagram:

[fill = gray] (+0+,+0+) rectangle
[fill = white] (+0,+0) rectangle (+0.5,+0.8);
(alpha) at (+0.25,+0.4) $\alpha$;
[-] (-0.4,+0.6) – (,+0.6);
[-] (-0.4,+0.3) – (,+0.3);
[-] (+0.5,+0.3) – (+1,+0.3);
[rounded corners=4pt,-] (-0.4,+-0.2) – (+1,+-0.2) ;
[-] (+0.5,+0.6) – (+1,+0.6);

[rounded corners=4pt,-] (+-0.2,+-0.2) – (+0.5,+-0.2) ;
[rounded corners=2pt,-] (+0.5,+0.1) – (+0.7,+0.1)

[fill = white] (+1.2,+0.2) circle (0.15);
(v) at  (+1.2,+0.2) $\vee$;

[-] (-0.4,+0.6) – (+1,+0.6);
[-] (-0.4,+0.3) – (+1,+0.3);
[rounded corners=4pt,-] (-0.4,+-0.2) – (,+-0.2)–
(+0.5,+0.6)– (+1,+0.6);

[rounded corners=4pt,-] (+0.5,+-0.2) – (+1,+-0.2);
[fill = white] (+0.5,-0.2) circle (0.1);

and note that this is exactly the same transition map as in
Part 3. of the proof of Lemma <ref>.
Hence, by
the properties listed in that part of the proof we have:

r^+ = [\perp,\mathsf{id}] \cdot \gamma^\ast \cdot
\mathsf{in}^{n}_{n+m}\cdot \mathsf{in}^{m}_{n}.

Moreover, let $\xi$ be defined by

[fill = gray] (+0+,+0+) rectangle
[fill = white] (+0,+0) rectangle (+0.5,+0.8);
(alpha) at (+0.25,+0.4) $\alpha$;
[-] (-0.4,+0.6) – (,+0.6);
[-] (-0.4,+0.3) – (,+0.3);
[-] (+0.5,+0.3) – (+1,+0.3);
[rounded corners=4pt,-] (-0.4,+-0.2) – (+1,+-0.2) ;
[-] (+0.5,+0.6) – (+1,+0.6);

[rounded corners=4pt,-] (+-0.2,+-0.2) – (+0.5,+-0.2) ;
[rounded corners=2pt,-] (+0.5,+0.1) – (+0.7,+0.1)

(v) at  (+1.2,+0.2) $;$;

[-] (-0.4,+0.6) – (+1,+0.6);
[-] (-0.4,+0.3) – (+1,+0.3);
[rounded corners=4pt,-] (-0.4,+-0.2) – (,+-0.2)–
(+0.5,+0.6)– (+1,+0.6);

[rounded corners=4pt,-] (+0.5,+-0.2) – (+1,+-0.2);
[fill = white] (+0.5,-0.2) circle (0.1);
(v) at  (+1.2,+0.2) $=$;

[fill = gray] (+0+,+0+) rectangle
[fill = white] (+0,+0) rectangle (+0.5,+0.8);
(alpha) at (+0.25,+0.4) $\alpha$;
[-] (-0.4,+0.6) – (,+0.6);
[-] (-0.4,+0.3) – (,+0.3);
[-] (+0.5,+0.3) – (+1,+0.3);
[rounded corners=4pt,-] (-0.4,+-0.2) – (+1,+-0.2) ;
[-] (+0.5,+0.6) – (+1,+0.6);

[rounded corners=4pt,-] (+-0.2,+-0.2) – (+0.5,+-0.2) ;
[rounded corners=2pt,-] (+0.5,+0.1) – (+0.7,+0.1)

[-] (-0.4,+0.6) – (+1,+0.6);
[-] (-0.4,+0.3) – (+1,+0.3);
[rounded corners=4pt,-] (-0.4,+-0.2) – (,+-0.2)–
(+0.5,+0.6)– (+1,+0.6);

[rounded corners=4pt,-] (+0.5,+-0.2) – (+1,+-0.2);
[fill = white] (+0.5,-0.2) circle (0.1);

The map $\xi$ is a $[\mathcal{A}]$-map which satisfies $\xi^\ast =
\gamma^\ast$. Then

\begin{align*}
& r^+ = [\perp,\mathsf{id}] \cdot \xi^\ast \cdot
\mathsf{in}^{n}_{n+m}\cdot \mathsf{in}^{m}_n= \\
& [\perp,\mathsf{id}_{m}] \cdot \xi^\ast \cdot \xi\cdot
\mathsf{in}^{m}_{n+m}= \\
& [\perp,\mathsf{id}_{m}] \cdot \xi^+\cdot
\mathsf{in}^{m}_{n+m}.
\end{align*}

$(\perp+\mathsf{id})=\mathsf{in}^{m}_{n+m}\cdot [\perp,\mathsf{id}]$ we get that

\mathsf{in}^{m}_{n+m} \cdot r^+= \mathsf{in}^{m}\cdot [\perp,\mathsf{id}_{m}] \cdot
\xi^+\cdot \mathsf{in}^{m}_{n+m}= (\perp+\mathsf{id}_{m}) \cdot \xi^+\cdot
\mathsf{in}^{m}_{n+m}.

From the above we get:

r^\omega \stackrel{\diamond}{=} (r^+)^\omega \stackrel{\dagger}{=}
((\perp+\mathsf{id}_{m})\cdot \xi^+)^\omega\cdot
\mathsf{in}^{m}_{n+m}.

The identity $(\diamond)$ follows by Lemma <ref>.
The identity $(\dagger)$ follows from a more general property:
given two coalgebras $\alpha:X\rightdcirc X=X\to TX$ and $\beta:Y\rightdcirc Y=Y\to TY$
and a $\mathsf{Set}$-map $j:X\to Y$ which is a coalgebra homomomorphism (or, equivalently,
$j^\sharp \cdot \alpha = \beta \cdot j^\sharp$ in $\mathcal{K}l(T)$)
we have: $\alpha^\omega = \beta^\omega \cdot j^\sharp = \beta^\omega \circ j$.
This property known as
uniformity of $(-)^\omega$ w.r.t. the base maps (see e.g.
In our setting, the fixpoint operator $(-)^\omega$ is uniform w.r.t. the base maps
since the order of $\mathcal{K}l(T)$ is pointwise induced
and since $\alpha^\omega =\bigwedge_{\kappa \in \mathsf{Ord}}(x\mapsto x\cdot \alpha)^\kappa(\top)$
(see Remark <ref>).

This completes the proof of the lemma.

We are now ready to proceed with the proof of Theorem <ref>.

(Theorem <ref>)
We have

$$\omega\mathfrak{Rat}(\mathcal{A}) \supseteq \omega\mathfrak{Reg}(\mathcal{A})$$
as it is
enough to note that

$$||\alpha,\mathfrak{F}||_{\omega}\cdot i_n = (\mathfrak{f_F}\cdot
\alpha^+)^\omega \cdot i_n = (\mathfrak{f_F}\cdot \alpha^+)^\omega \cdot
\mathfrak{f_F}\cdot  \alpha^+ \cdot i_n$$
and take $r= \mathfrak{f_F} \cdot
\alpha^+\cdot  i_n$, $r_k =  \mathfrak{f_F} \cdot  \alpha^+ \cdot k_n$.

Conversely, let $r, r_i \in \mathfrak{Reg}(1,m)$. Put $s=[r_1,\ldots,r_m]$ and
consider any regular morphism $s'\in \mathfrak{Reg}(m,m)$ such that $r = s'\cdot
1_m$. For sake of clarity of notation let $m_1\defeq m$ and $m_2\defeq m$.
Consider the map $\gamma$
defined by:

[-] (-0.5,+0.25) – (+1,+0.25);
[fill = white] (+0,+0) rectangle (+0.5,+0.5);
(alpha) at (+0.25,+0.25) $s'$;

[-] (-0.5,+0.25) – (+1,+0.25);
[fill = white] (+0,+0) rectangle (+0.5,+0.5);
(alpha) at (+0.25,+0.25) $s$;

[-] [rounded corners=4pt,-] (+0.5,+0.25) – (+1,+.25);
[fill = white] (+0.6,+0.25) circle (0.1);
[-] [rounded corners=4pt,-] (,+0.25)–(+0.1,+0.25)–(+0.2,-0.45)– (+0.5,-0.45);

[-] (,+0.25) – (+1,+0.25);

Note that this map is a regular morphism, so the map $ \gamma ^\omega
\cdot 1_{m_1+m_2}$ is $\omega$-regular. Moreover, we get:

\begin{align*}
&\gamma ^\omega \cdot 1_{m_1+m_2} = \gamma ^\omega \cdot  \gamma \cdot
1_{m_1+m_2}  =    \gamma^\omega \cdot \mathsf{in}^{m_2}\cdot  s' \cdot 1_{m_1} =
[r_1,\ldots,r_m]^\omega \cdot r.
\end{align*}

This completes the proof.

§ PROBABILISTIC AUTOMATA

The main purpose of this section is to put probabilistic systems
[5, 47, 46, 49, 3, 4]
into the framework of Section <ref>. Here, we focus our attention
on probabilistic automata which are akin to
fully probabilistic systems from
Example <ref>[5, 13, 2, 46].

§.§ Preliminaries

A probabilistic
automaton is a tuple
$$(X,\Sigma,P:X\times \Sigma \times X\to [0,1],\mathfrak{F}),$$

where $X$ is a set of states, $\Sigma$ an alphabet,
$P$ is a probability transition function,
i.e. a function such that
for any $x\in X$ we have $\sum_{(a,y)\in \Sigma\times X} P(x,a,y) = 1$,
and $\mathfrak{F}\subseteq X$ the set of accepting states.

For $C\subseteq X$ we define
$P(x,a,C) \defeq \sum_{y\in C} P(x,a,y)$. An execution fragment is a finite sequence
$\mathfrak{s} = x_0\stackrel{a_0}{\to} x_1 \stackrel{a_1}{\to}x_2 \ldots x_{n-1}\stackrel{a_{n-1}}{\to} x_n$ such
that $P(x_i,a_i,x_{i+1}) > 0$. We define $first (\mathfrak{s} ) = x_0$,
$last (\mathfrak{s}) = x_n$, $length(\mathfrak{s}) = n$, $trace(\mathfrak{s}) = a_0\ldots a_{n-1}$ and
$P(\mathfrak{s}) = \prod_{i=0,\ldots,n-1} P(x_i,a_i,x_{i+1})$. An execution is an infinite sequence
$\mathfrak{p} = x_0\stackrel{a_0}{\to} x_1\stackrel{a_1}{\to} x_2 \stackrel{a_2}{\to}\dots$
with $P(x_i,a_i,x_{i+1})>0$.

Let $first(\mathfrak{p}) \defeq  x_0$, $trace(\mathfrak{p}) \defeq a_0
$\mathfrak{p}^{(n)} \defeq x_0\stackrel{a_0}{\to} \ldots \stackrel{a_{n-1}}{\to}x_n$ and $\mathfrak{p}_n \defeq x_n$.
For an execution fragment
$\mathfrak{s}$ of length $n$ let $\mathfrak{s}\uparrow$ denote the set of all executions
$\mathfrak{p}$ such that $\mathfrak{p}^{(n)} = \mathfrak{s}$.

Let $Exec(x)$ denote the set of all executions $\mathfrak{p}$ such that $first (\mathfrak{p})=x$.
Let $\Sigma(x)$ be the smallest sigma field on $Exec(x)$ which contains all sets $\mathfrak{s}\uparrow$ for any
execution fragment $\mathfrak{s}$ with $first(\mathfrak{s}) = x$. Finally, let $\mathcal{Q}_x$ denote the unique
probability measure on $\Sigma(x)$ such that
$\mathcal{Q}_x(\mathfrak{s}\uparrow) = P(\mathfrak{s})$ for any execution
fragment $\mathfrak{s}$ with $first(\mathfrak{s}) = x$. We will often drop the subscript
and write $\mathcal{Q}$ instead of $\mathcal{Q}_x$ if the measure can be deduced from the context.

For $\Lambda \subseteq \Sigma^\ast$ and $C\subseteq X$ define $Exec(\Lambda,C)$ to be the set of all
executions $\mathfrak{p}=x_0\stackrel{a_0}{\to}x_1\ldots $ for which there is $n$ with $trace(\mathfrak{p}^{(n)})
\in \Lambda$ and $x_n\in C$ and consider $Exec(x,\Lambda, C) \defeq Exec(\Lambda,C)\cap Exec(x)$.
As stated in [5] the set $Exec(x,\Lambda,C)$ is $\Sigma(x)$-measurable. Additionally,
put $Exec(\Lambda) \defeq Exec(\Lambda,X)$ and $Exec(x,\Lambda) \defeq Exec(x,\Lambda,X)$.

An execution $\mathfrak{p}=x=x_0\stackrel{a_0}{\to}x_1\stackrel{a_1}{\to}\ldots $
starting at $x$ is called $C$-accepting provided that it visists $C$ infinitely often, i.e.
the set $\{i<\omega \mid x_i \in C\}$ is infinite. Let $AccExec(C)$ denote all $C$-accepting executions and let
$AccExec(x,C) = AccExec(C) \cap Exec(x)$. The set $AccExec(x,C)$ is $\Sigma(x)$-measurable as

\begin{align*}
& AccExec(x,C) = \bigcap_{n\geq 0}\bigcup_{k\geq n}
\{\mathfrak{p}\in Exec(x) \mid \mathfrak{p}_k \in C \}=\\
& \bigcap_{n\geq 0}\bigcup_{k\geq n}
Exec(x,\{ \sigma\in \Sigma^\ast \mid \text{ length of }\sigma = k\} ,C)=\\
& \bigcap_{n\geq 0} Exec(x, \{\sigma\in \Sigma^\ast \mid \text{ length of }\sigma \geq n\},C).
\end{align*}

A curious reader is referred to e.g.
[2, 5] for more details on fully probabilistic systems
and probability measures they induce.

Consider the automaton $(\{s_0,s_1\},\Sigma = \{0,1\},P, \mathfrak{F}=\{s_1\})$, where
$P$ is the probability transition function given by the diagram below:

[shorten >=1pt,node distance=2cm,on grid]
[state]   (q_0)                $s_0$;
[state,accepting] (q_2) [right=of q_0] $s_1$;
[->] (q_0) edge[bend right] node [below] $1,\frac12$
(q_2) edge[loop above] node         $0,\frac12$ ()
(q_2) edge[bend right] node [above] $0,\frac12$ (q_0);
[->] (q_2) edge[loop above] node         $1,\frac12$ ();

Let $\Lambda \subseteq \Sigma^\ast$. Then
$Exec(s_0,\Lambda, \mathfrak{F})$ consists of all executions
$\mathfrak{p}$ such that $\mathfrak{p} =
x_0 \stackrel{a_0}{\to} x_1\stackrel{a_1}{\to} x_2 \stackrel{a_2}{\to} \ldots$
for which $x_0 = s_0$,

\begin{align}
(x_i,a_i,x_{i+1}) \text{ is from }
\{(s_0,0,s_0), (s_0,1,s_1), (s_1,0,s_0), (s_1,1,s_1)\}, \label{condition:exec}
\end{align}

and such that there is $n$ with $a_0\ldots a_n\in \Lambda$ and $a_n=1$.
Similarily, $Exec(s_1,\Lambda,\mathfrak{F})$
contains all executions $\mathfrak{p}$ such that
$first(\mathfrak{p}) = s_1$, satisfying (<ref>)
and whose $trace(\mathfrak{p}^{(n)})\in \Lambda$ with its last
letter equal to $1$ for some $n\in\mathbb{N}$. In particular this means that
$\mathcal{Q}(Exec(s_i,\{w0\},\mathfrak{F})) = 0$ and
$\mathcal{Q}(Exec(s_i,\{w1\},\mathfrak{F})) = \left(\frac12 \right)^{n+1}$
for any $w\in \Sigma^\ast$ whose length equals to $n$.

Now, $AccExec(s_0,\mathfrak{F})$ is the set of all executions
$\mathfrak{p} = s_0 = x_0 \stackrel{a_0}{\to} x_1\stackrel{a_1}{\to} x_2
\stackrel{a_2}{\to} \ldots$
such that it satisfies (<ref>)
and for any $n\in \mathbb{N}$
there is $i_n\geq n$ such that $(x_{i_n},a_{i_n}, x_{i_n+1})$ equals to
Similarily, $AccExec(s_1, \mathfrak{F})$ is the set of all
executions whose first state is $s_1$ which
satisfy the same argument as above. It is easy to see that
[This follows by the fact that any execution
$\mathfrak{p}=x_0\stackrel{a_0}{\to}x_1\stackrel{a_1}{\to}\ldots$ satisfying
(<ref>) that is not a member of $AccExec(s_i, \mathfrak{F})$
satisfies the following condition: there is a natural number
$n$ such that for all $i\geq n$ we have $x_i = s_0$ and $a_i = 0$.
Hence, the probability of the set of all such executions equals $0$.

The remaining part of this section will focus on finding a suitable setting in
which we can model probabilistic automata and their (in)finite behaviour using
the framework presented in the previous section.

Any probabilistic automaton can be modelled coalgebraically as a pair
$(\alpha: X \to \mathcal{D}(\Sigma \times X),\mathfrak{F}\subseteq X)$,
where $\mathcal{D}$ is the subdistribution monad from Example <ref>
and $\alpha$ is given by (see e.g. [47, 9]):

\[
\alpha(x)(a,y) \defeq P(x,a,y).
\]

The Kleisli category associated with the monad
$\mathcal{D}(\Sigma^\ast \times\mathcal{I}d+\Sigma^\omega )$
[By applying the construction from
Section <ref> to $T=\mathcal{D}$ and
$F=\Sigma\times \mathcal{I}d$ we obtain a monadic structure
on the aforementioned functor.]
is order enriched with the hom-set ordering given for
$f,g:X\to \mathcal{D}(\Sigma^\ast\times Y +\Sigma^\omega) $ by:

\[
f\leq g \iff f(x)(y)\leq g(x)(y).
\]

Although the Kleisli category for this monad is $\cpo$-enriched,
its hom-posets do not admit arbitrary finite suprema
[27, 13]. In other words, the setting
is incompatible with the setting from the previous section. Hence, the remaining
part of this section is focused on solving this issue based on ideas given in
[23, 13].

§.§ Choosing the right monad

Here, we introduce a monad which is a suitable replacement for $\mathcal{D}$, i.e.
it satisfies the desired properties to make it
suitable for modeling (in)finite behaviours of probabilistic automata.
Inspired by [23] we consider the continuous continuation
monad parametrized by the set $[0,1]$ whose functorial part is
defined for any set $X$ by:

\[
\mathfrak{D} X \defeq (X\to [0,1])\to_\omega [0,1],
\]

where $P\to_\omega Q$ denotes the set of functions between two
's $P$ and $Q$ which preserve suprema of $\omega$-chains.
The identity maps and the composition in the Kliesli category for
$\mathfrak{D}$ are as follows:

\begin{align*}
& \mathsf{id}:X\to (X\to [0,1])\to_\omega [0,1]; x\mapsto \Delta_x,
\text{ where } \Delta_x(d) \defeq d (x). \\
& g\cdot f: X\to (Z\to [0,1])\to_\omega [0,1],
\text{ where } (g\cdot f)(x)( d ) \defeq f(x)(y\mapsto g(y)(d))
\end{align*}

with  $f:X\to (Y\to [0,1])\to_\omega [0,1]$ and
$g:Y\to (Z\to [0,1])\to_\omega [0,1]$. Note that any
$d:X\to [0,1]\in \mathcal{D}X$ can be assigned a function
$\nu_X(d):(X\to [0,1])\to_\omega [0,1]$
which maps any $d':X\to [0,1]$ onto

\begin{align}
\nu_X(d)(d')=\sum_{x\in X} d'(x)\cdot d(x).\label{formula_natural_transformation_probabilistic}
\end{align}

It is not hard to see that this turns the family $\{\nu_X:\mathcal{D}X\to \mathfrak{D} X\}$
into a natural transformation $\nu:\mathcal{D}\implies \mathfrak{D}$
which is a monad morphism between the monads $\mathcal{D}$ and $\mathfrak{D}$.
Additionally, it is easy to see that there is a natural ordering of arrows in
$\mathcal{K}l(\mathfrak{D})$ which share the same domain and codomain.
Indeed, for $f,g:X\to \mathfrak{D} Y$ we have:

\[
f\leq g \iff f(x)(d)\leq g(x)(d) \text{ for any }x\in X \text{ and } d:Y\to [0,1].
\]

This turns the Kleisli category for the monad  $\mathfrak{D}$ into an
order enriched category. Moreover, the following theorem is true.

The order enrichment of $\mathcal{K}l(\mathfrak{D})$ is pointwise induced,
every hom-set of $\mathcal{K}l(\mathfrak{D})$ is a complete lattice and
the category is $\cpo$-enriched and left distributive.

The fact that the partial order is a complete lattice order is a direct corollary from the definition
of $\mathfrak{D}$.
We will now prove that Kleisli category for $\mathfrak{D}$ is $\cpo$-enriched.
Take any ascending chain $\{f_i:X\to \mathfrak{D}Y\}_{i<\omega}$ of morphisms and note that

\begin{align*}
& [g\cdot (\bigvee_i f_i)](x)(d) = (\bigvee_i f_i)(x)(y\mapsto g(y)(d)) =  \\
& \bigvee_i f_i (x)(y\mapsto g(y)(d)) = \bigvee_i g\cdot f_i(x)(d) \text{ and }\\
& [(\bigvee_i f_i)\cdot h](z)(d) = h(z)(x\mapsto \bigvee_i f_i(x)(d)) \stackrel{\diamond}{=}\\
& \bigvee_i h(z)(x\mapsto f_i(x)(d)) = \bigvee_i (h\cdot f_i)(z)(d),
\end{align*}

where the equality marked with ($\diamond$) follows from the fact that $\mathfrak{D}X$ consists
of functions $(X\to [0,1])\to_\omega [0,1]$ that preserve $\omega$-chains.
In order to see left distributivity consider
morphisms $\{f_i\}_{i\in I}:X\to \mathfrak{D} Y $ and $g:Y\to
\mathfrak{D} Z$ and note that

\begin{align*}
& [g\cdot (\bigvee_i f_i)](x)(d) = (\bigvee_i f_i)(x)(y\mapsto g(y)(d)) =  \\
& \bigvee_i f_i (x)(y\mapsto g(y)(d)) =
\bigvee_i g\cdot f_i(x)(d).
\end{align*}

This proves the assertion.

From the above it follows that $\mathcal{K}l(\mathfrak{D})$ satisfies (<ref>)-(<ref>)
from Section <ref>.

§.§.§  The monad $\mathfrak{D}(\Sigma^\ast \times \mathcal{I}d+\Sigma^\omega)$

By instantiating the construction from Section <ref>
for $T=\mathfrak{D}$ and $F=\Sigma\times \mathcal{I}d$ we obtain
the monad $\mathfrak{D}(\Sigma^\ast \times \mathcal{I}d + \Sigma^\omega)$.
We explicitly spell out the formula for the identity maps and the composition in
$\mathcal{K}l(\mathfrak{D}(\Sigma^\ast\times \mathcal{I}d+\Sigma^\omega))$ as it
will be used throughout the remaining part of this section.
For any set $X$ the identity map $\mathsf{id}$ is given by:

\begin{align*}
& \mathsf{id}:X\to (\Sigma^\ast \times X +\Sigma^\omega\to [0,1])\to_\omega [0,1], \\
& \mathsf{id}(x)(d) = d(\varepsilon,x).
\end{align*}

Moreover, for $f:X\to \mathfrak{D}(\Sigma^\ast \times Y+\Sigma^\omega)$ and
$g:Y\to \mathfrak{D}(\Sigma^\ast\times Z+\Sigma^\omega)$ the map
$g\cdot f: X\to \mathfrak{D}(\Sigma^\ast \times Z+\Sigma^\omega)$ is:

\begin{align*}
& g\cdot f :X\to (\Sigma^\ast \times Z+\Sigma^\omega\to [0,1])\to_\omega [0,1], \\
& (g\cdot f) (x)(d) = f(x)((\sigma,y) \mapsto g(y)(d_{|\sigma}) \text{ and }  v\mapsto d(v) ),
\end{align*}

where for $d:\Sigma^\ast\times Z+\Sigma^\omega \to [0,1]$ and $\sigma\in \Sigma^\ast$
the map $d_{|\sigma}:\Sigma^\ast\times Z+\Sigma^\omega\to [0,1]$ is given by
$d_{|\sigma}(\tau,z) = d(\sigma\tau,z)$ for $\tau\in \Sigma^\ast$, $z\in Z$ and
$d_{|\sigma}(v) = d(\sigma v)$ for $v\in \Sigma^\omega$.

The following statement is a direct consequence of the definition of the monad
$\mathfrak{D}(\Sigma^\ast\times \mathcal{I}d+\Sigma^\omega)$ and the properties
of $\mathfrak{D}$ from the previous subsection.

$\mathcal{K}l(\mathfrak{D}(\Sigma^\ast \times \mathcal{I}d +
\Sigma^\omega))$ satisfies (<ref>)-(<ref>) from Section <ref>.

§.§ (In)finite behaviour for probabilistic automata

Let $(\alpha,\mathfrak{F})$ be a pair as in Remark
and consider

\[
(\widehat{\alpha}:X\stackrel{\alpha}{\to}\mathcal{D}(\Sigma\times X)
\stackrel{\nu_{\Sigma\times X}}{\to} \mathfrak{D}
(\Sigma \times X)
\hookrightarrow \mathfrak{D}(\Sigma^\ast \times X+\Sigma^\omega),\mathfrak{F}),
\]

where $\nu$ is given
by (<ref>). We see that the map
$\widehat{\alpha}$ can be viewed as an endomorphism in the Kleisli category for the monad
$\mathfrak{D} (\Sigma^\ast \times \mathcal{I}d +\Sigma^\omega)$.

The rest of this section is devoted to presenting some properties of
$||\widehat{\alpha},\mathfrak{F}||$ and $||\widehat{\alpha},\mathfrak{F}||_\omega$ for the pair
$(\widehat{\alpha},\mathfrak{F})$. As it turns out below the values $||\widehat{\alpha},\mathfrak{F}||(x)$
and $||\widehat{\alpha},\mathfrak{F}||_\omega(x)$ encode probabilities of certain events from $\Sigma(x)$.

§.§.§ Finite behaviour

The following lemma is a direct consequence of the definition of
and the composition in $\mathcal{K}l(\mathfrak{D}(\Sigma^\ast\times \mathcal{I}d+\Sigma^\omega))$.

We have:

\begin{align*}
& \widehat{\alpha}^+,\widehat{\alpha}^\ast:X\to (\Sigma^\ast \times X +\Sigma^\omega\to [0,1])
\to_\omega [0,1]; \\
& \widehat{\alpha}^+(x)(d) =
\sum_{(a,y)\in \Sigma \times X} \widehat{\alpha}^\ast(y)(d_{|a})\cdot \alpha(x)(a,y)\\
& \widehat{\alpha}^\ast (x)(d) =
\max \{d(\varepsilon,x) \ , \   \sum_{(a,y)\in \Sigma \times X }
\widehat{\alpha}^\ast (y)(d_{|a}) \cdot \alpha(x)(a,y) \}.
\end{align*}

For $\mathfrak{F}\subseteq X$ we have:

\begin{align*}
& \mathfrak{f}_{\mathfrak{F}}:X\to (\Sigma^\ast\times X+\Sigma^\omega\to
[0,1])\to_\omega [0,1], \\
& \mathfrak{f}_{\mathfrak{F}}(x)(d) =\left \{
\begin{array}{cc} d(\varepsilon,x) & \text{ for }x\in \mathfrak{F},\\
0       & \text{ otherwise.}
\end{array} \right.
\end{align*}

Hence, the map $!\cdot \mathfrak{f_{{F}}}:X\to (\Sigma^\ast\times
1+\Sigma^\omega\to [0,1])\to_\omega [0,1]$ is given by:

\begin{align*}
& (!\cdot \mathfrak{f}_{\mathfrak{F}})(x)(d) =\left \{
\begin{array}{cc} d(\varepsilon,1) & \text{ for }x\in \mathfrak{F},\\
0       & \text{ otherwise.}
\end{array} \right.
\end{align*}

Therefore, the finite behaviour of $(\widehat{\alpha},\mathfrak{F})$ is given by

\begin{align*}
& ||\widehat{\alpha},\mathfrak{F}||:X\to
(\Sigma^\ast\times 1 +\Sigma^\omega\to [0,1])\to_\omega [0,1] \\
& ||\widehat{\alpha},\mathfrak{F} ||(x)(d) = (!\cdot \mathfrak{f_F}\cdot \widehat{\alpha}^*)(x)(d) =  \\
& \widehat{\alpha}^\ast (x) \left (
(\sigma, y)\mapsto \left \{ \begin{array}{cc}
d(\sigma,1) & y\in \mathfrak{F}, \\
0 & \text{otherwise}
\end{array}
\right. \text{ and } v\mapsto 0
\right ).
\end{align*}

For $\Lambda \subseteq \Sigma^\ast$ and $\sigma \in \Sigma$
put  $\Lambda/\sigma \defeq \{ \tau \mid \sigma \tau \in \Lambda\}$ and consider a mapping
$\chi_{\Lambda}:\Sigma^\ast \times 1+\Sigma^\omega \to [0,1]$ given by:

\begin{align}
\chi_\Lambda (x) = \left \{
\begin{array}{cc} 1 & x=(\sigma,1) \text{ and }\sigma\in \Lambda \\ 0
& \text{ otherwise}.
\end{array} \right. \label{equation_chi}
\end{align}

If we define a function
$\chi_{\mathfrak{F},\Lambda}:\Sigma^\ast\times X+\Sigma^\omega \to [0,1]$

\begin{align}
\chi_{\mathfrak{F},\Lambda}(\tau,y) = \left \{ \begin{array}{cc}
1 & y\in \mathfrak{F}\text{ and
}\tau \in \Lambda, \\
0 & \text{otherwise}
\end{array}
\right. \text{ and } \chi_{\mathfrak{F},\Lambda}(v)= 0.
\label{equation:chi_extended}
\end{align}

then $||\widehat{\alpha},\mathfrak{F}||(x)(\chi_{\Lambda}) =
\widehat{\alpha}^\ast(x)(\chi_{\mathfrak{F},\Lambda})$ and:

\begin{align}
& ||\widehat{\alpha},\mathfrak{F}||(x)(\chi_{\Lambda}) =
& \left \{ \begin{array}{cc}
1 &  \varepsilon\in \Lambda \text{ and }x\in \mathfrak{F} \\
\sum_{(a,y)\in \Sigma \times X }
\widehat{\alpha}^\ast (y) (\chi_{\mathfrak{F},\Lambda/a} ) \cdot \alpha(x)(a,y)  &
\text{ otherwise.}
\end{array}
\right. \label{equation:behaviour}
\end{align}

A careful analysis of the formulae from
[5, 13] describing the value
$\mathcal{Q}(Exec(x,\Lambda,C))$ allows us to see that the following statement holds:

We have:

\begin{align*}
& ||\widehat{\alpha},\mathfrak{F}||(x)(\chi_\Lambda)
= \mathcal{Q}(Exec(x,\Lambda,\mathfrak{F})),
\end{align*}

i.e. $||\widehat{\alpha},\mathfrak{F}||(x)(\chi_\Lambda)$ is
the probability of reaching a state in $\mathfrak{F}$  from $x$
via an execution fragment whose trace is a member of $\Lambda$.

§.§.§ Infinite behaviour

Let us focus on the infinite behaviour of $(\widehat{\alpha},\mathfrak{F})$ introduced in the previous section
given by
$$||\widehat{\alpha},\mathfrak{F}||_\omega = (\mathfrak{f_F}\cdot
\widehat{\alpha}^+)^\omega: X\to \mathfrak{D}(\Sigma^\omega).$$

For any $\Lambda \subseteq \Sigma^\ast$ we have:

\begin{align*}
& ||\widehat{\alpha},\mathfrak{F}||_\omega : X\to (\Sigma^\omega \to [0,1])\to_\omega [0,1], \\
& ||\widehat{\alpha},\mathfrak{F}||_\omega(x)(\chi_{\Lambda \cdot \Sigma^\omega }) =
\mathcal{Q}(Exec(x,\Lambda) \cap AccExec(x,\mathfrak{F})),
\end{align*}

where $\Lambda \cdot \Sigma^\omega \defeq \{wv\in \Sigma^\omega \mid  w \in \Lambda\text{ and } v \in \Sigma^\omega \}$.

The proof is divided into three parts.

Part 1.
We will first show the statement holds for $\Lambda = \{\varepsilon\}$, i.e. we prove that
$ ||\widehat{\alpha},\mathfrak{F}||_\omega(x)(\chi_{\Sigma^\omega}) =
\mathcal{Q}(AccExec(x,\mathfrak{F}))$. Indeed,

\[
AccExec(x,\mathfrak{F}) = \bigcap_{n\geq 0}\bigcup_{k\geq n} \{\mathfrak{p}\in Exec(x) \mid \mathfrak{p}_k \in \mathfrak{F} \}
\]

we have:

\[
\mathcal{Q}(AccExec(x,\mathfrak{F}) )= \lim_{n\to \infty} \mathcal{Q}(A_n^x),
\]

where $A_n^x \defeq \bigcup_{k\geq n} \{\mathfrak{p}\in Exec(x) \mid \mathfrak{p}_k \in \mathfrak{F} \}=
Exec(x,\{\sigma\in \Sigma^\ast \mid \text{ length of }\sigma \geq n
\},\mathfrak{F})$
is a descending chain of $\Sigma(x)$-measurable sets. Let us now consider a family of maps $\{G_n:X\to (\Sigma^\omega \to
[0,1])\to_{\omega} [0,1]\}_n$ defined inductively as follows:

\begin{align*}
G_0(x)(d) = 1 \text{ and } G_{n+1} = G_{n} \cdot \mathfrak{f_F}\cdot \widehat{\alpha}^+.
\end{align*}

Note that the sequence $\{G_n(x)(d)\}_n$ is descending for any fixed $x\in X$
and $d$ and that

\begin{align}
||\widehat{\alpha},\mathfrak{F}||_\omega(x)(d) = \lim_{n\to \infty} G_n(x)(d).
\label{equation:limit_omega}
\end{align}

We will now show that $G_n(x)(\chi_{\Sigma^\omega}) = \mathcal{Q}(A_{n}^x)$ for $n\geq 1$. For $G_1$ we have:

\begin{align}
&  G_{1}(x)(\chi_{\Sigma^\omega}) = (G_0\cdot \mathfrak{f_F}\cdot \widehat{\alpha}^+)(x)(\chi_{\Sigma^\omega})=  \\
&  \widehat{\alpha}^+(x)((\sigma,y) \mapsto G_0\cdot \mathfrak{f_F}(y)(\chi_{\Sigma^\omega | \sigma})
\text{ and }v\mapsto \chi_{\Sigma^\omega}(v)   ) = \\
&  \widehat{\alpha}^+(x)((\sigma,y) \mapsto G_0\cdot \mathfrak{f_F}(y)(\chi_{\Sigma^\omega})
\text{ and }v\mapsto \chi_{\Sigma^\omega}(v)   ).\label{formula_conditional_probability_0}
\end{align}

In the above

\begin{align*}
& G_0\cdot \mathfrak{f_F}(y)(\chi_{\Sigma^\omega}) =
\mathfrak{f_F}(y)((\tau,z)\mapsto G_0(z)(\chi_{\Sigma^\omega | \tau})
\text{ and } v\mapsto \chi_{\Sigma^\omega}(v) ) =\\
& \mathfrak{f_F}(y)((\tau,z)\mapsto 1 \text{ and } v\mapsto 1 ) =
\left \{ \begin{array}{cc} 1 & y\in \mathfrak{F} \\ 0 & \text{ otherwise.} \end{array} \right.
\end{align*}

Hence, if we continue with (<ref>) we get:

\begin{align*}
\widehat{\alpha}^+(x)\left ((\sigma,y) \mapsto \left \{ \begin{array}{cc} 1 & y\in \mathfrak{F} \\ 0 & \text{ otherwise} \end{array} \right.
\text{ and }v\mapsto 1   \right ) = \mathcal{Q}(A_1^x).
\end{align*}

If we now assume by induction that the statement holds for some $n>1$ then

\begin{align*}
G_n\cdot \mathfrak{f_F} (y)(\chi_{\Sigma^\omega}) = \mathfrak{f_F}(y)((\tau,z)\mapsto \mathcal{Q}(A_n^z) \text{ and } v\mapsto 1) =
\left \{
\begin{array}{cc}
\mathcal{Q}(A_n^y) & y\in \mathfrak{F} \\
0 & \text{ otherwise}.
\end{array}
\right.
\end{align*}

Hence, by following a similar reasoning to the one applied to $G_1$ we get:

\begin{align*}
G_{n+1}(x)(\chi_{\Sigma^\omega}) = \widehat{\alpha}^+
\left (
\left \{
\begin{array}{cc}
\mathcal{Q}(A_n^y) & y\in \mathfrak{F} \\
0 & \text{ otherwise}
\end{array}
\right.
\text{ and }
v\mapsto 1
\right )  = \mathcal{Q}(A_{n+1}^x).
\end{align*}

Part 2. We will now show that the following holds:

\[
||\widehat{\alpha},\mathfrak{F}||_\omega(x)(\chi_{\{a_0a_1\ldots a_n\}\cdot \Sigma^\omega}) =
\mathcal{Q}(Exec(x,\{a_0\ldots a_n\}) \cap AccExec(x,\mathfrak{F})).
\]

Assume $\mathfrak{s}=x=x_0\stackrel{a_0}{\to}\ldots \stackrel{a_{n-1}}{\to} x_n  \stackrel{a_{n}}{\to} x_{n+1}=x'$.

Then for
$\sigma \in \Sigma^\ast$ of length less than or equal to $n$ we have
$\chi_{\{a_0 a_1\ldots a_{n}\}\cdot \Sigma^\omega | \sigma}$
is equal $\chi_{\{a_k\ldots a_{n}\}\cdot \Sigma^\omega}$
if $\sigma = a_0\ldots a_{k-1}$ and it is the constantly equal to zero function otherwise.
This observation together with the fact that

\begin{align*}
& \mathcal{Q}(\mathfrak{s}\uparrow \cap AccExec(x,\mathfrak{F}))=
\mathcal{Q}(AccExec(x,\mathfrak{F})\mid \mathfrak{s}\uparrow )\cdot Q(\mathfrak{s}\uparrow)=\\
& \mathcal{Q}(AccExec(x',\mathfrak{F}))\cdot \mathcal{Q}(\mathfrak{s}\uparrow)
\end{align*}

and induction allows us to prove the assertion.

Part 3. The statement from Part 2. can be easily generalized to

\[
\chi_{
\{w_1\}\cdot \Sigma^\omega\cup \{w_2\}\cdot \Sigma^\omega
) =
\mathcal{Q}(Exec(x,\{w_1,w_2\}) \cap AccExec(x,\mathfrak{F})),
\]

for any pair of incomparable words $w_1,w_2\in \Sigma^\ast$ with respect to lexicographic
ordering on $\Sigma^\ast$. Indeed, in this case the sets $\{w_1\}\cdot \Sigma^\omega$
and $\{w_2\}\cdot \Sigma^\omega$ are disjoint. If
$\sigma$ is not comparable with $w_1$ and $w_2$ then
$\chi_{ \{w_1\}\cdot \Sigma^\omega\cup \{w_2\}\cdot \Sigma^\omega |\sigma} $ is
constantly equal to zero function. However, if $\sigma$ is comparable wit $w_i$ then
for all such $\sigma$ which are sufficiently long we have:
$\chi_{ \{w_1\}\cdot \Sigma^\omega\cup \{w_2\}\cdot \Sigma^\omega |\sigma}
= \chi_{\{w_i\}\cdot \Sigma^\omega |\sigma} $. Hence, by the same argument as before we prove
the desired assertion. Note that the equation generalizes to any finite
set of incomparable words $\{w_1,\ldots,w_n\}$.

Finally, the general statement holds since the function

||\widehat{\alpha},\mathfrak{F}||_\omega(x): (\Sigma^\omega \to [0,1]) \to_\omega [0,1]

preserves suprema of $\omega$-chains. Indeed, let $\Lambda \subseteq \Sigma^\ast$ and note
that $\Lambda \cdot \Sigma^\omega = \Lambda'\cdot \Sigma^\omega$ for a countable subset
$\Lambda'\subseteq \Lambda$ of incomparable words $\Lambda'=\{w_1,w_2,\ldots\}$. Then

\chi_{\Lambda\cdot \Sigma^\ast} = \chi_{\Lambda'\cdot \Sigma^\omega} =
\bigvee_n \chi_{\{w_1,\ldots,w_n\}\cdot \Sigma^\omega}.

\begin{align*}
& ||\widehat{\alpha},\mathfrak{F}||_\omega(x)(
\chi_{
\Lambda\cdot \Sigma^\omega
) =
\chi_{
\Lambda'\cdot \Sigma^\omega
) =
\bigvee_n \chi_{
\{w_1,\ldots,w_n\}\cdot \Sigma^\omega
) = \\
& \bigvee_n ||\widehat{\alpha},\mathfrak{F}||_\omega(x)(
\chi_{
\{w_1,\ldots,w_n\}\cdot \Sigma^\omega
) =
\bigvee_n  \mathcal{Q}(Exec(x,\{w_1,\ldots, w_n\}) \cap AccExec(x,\mathfrak{F})) = \\
&  \mathcal{Q}(Exec(x,\Lambda') \cap AccExec(x,\mathfrak{F}))=
\mathcal{Q}(Exec(x,\Lambda) \cap AccExec(x,\mathfrak{F})).
\end{align*}

Let us consider the probabilistic automaton from
Example <ref> and put it
into the framework of the Lawvere theory for the monad
$\mathfrak{D}(\Sigma^\ast\times \mathcal{I}d+\Sigma^\omega)$.
Below, we calculate (some values of) finite and infinite
behaviours of the automaton derived from Example <ref>
in a direct manner (i.e. without applying Theorem <ref> or
Theorem <ref>).  By following the guidelines of
Remark <ref>
we obtain $(\alpha,\mathfrak{F})$,
where $\alpha : X\to \mathcal{D}(\Sigma\times X)$ given  by $\alpha(s_0) = P(s_0,-,-)$ and
$\alpha(s_1) = P(s_1,-,-)$. Moreover, $\widehat{\alpha}: X\to
\mathfrak{D}(\Sigma^\ast \times X+\Sigma^\omega)$ is defined by

\begin{align*}
& \widehat{\alpha}(s_0) : (\Sigma^\ast \times \{s_0,s_1\}
+\Sigma^\omega \to [0,1]) \to_\omega [0,1];
d\mapsto \frac12 \cdot d(0,s_0) + \frac12\cdot  d(1,s_1)
\end{align*}

and $\widehat{\alpha}(s_1) = \widehat{\alpha}(s_0)$.
Next, observe that by Lemma <ref> the
morphisms  $\widehat{\alpha}^+$
and $\widehat{\alpha}^\ast$ are the least solutions to:

\begin{align*}
\widehat{\alpha}^+(s_0)(d) &  =  \widehat{\alpha}^+(s_1)(d)  =
\frac12 \cdot \widehat{\alpha}^\ast(s_0)(d_{|0})
+ \frac12 \cdot \widehat{\alpha}^\ast(s_1)(d_{|1}) \\
\widehat{\alpha}^\ast (s_0)(d) & =
\max \{
\frac12 \cdot \widehat{\alpha}^\ast(s_0)(d_{|0})
+ \frac12 \cdot \widehat{\alpha}^\ast(s_1)(d_{|1})
\} \\
\widehat{\alpha}^\ast(s_1)(d)  & =
\max \{
\frac12 \cdot \widehat{\alpha}^\ast(s_0)(d_{|0})
+ \frac12 \cdot \widehat{\alpha}^\ast(s_1)(d_{|1})
\}.
\end{align*}

Consider $w=a_0 a_1\ldots a_n\in \Sigma^\ast$, $\chi_{\{w0\}}$, $\chi_{\{w1\}}$
as in (<ref>) and
$\chi_{\mathfrak{F},\{w0\}}$, $\chi_{\mathfrak{F},\{w1\}}$ as
in (<ref>). Then by (<ref>)

\begin{align*}
||(\widehat{\alpha},\mathfrak{F})||(s_0)(\chi_{\{w0\}}) =
\frac12 \cdot \widehat{\alpha}^\ast (s_0)( \chi_{\mathfrak{F},\{w0\}_{/0}})+
\frac12 \cdot \widehat{\alpha}^\ast (s_1)(\chi_{\mathfrak{F},\{w0\}_{/1}})
\end{align*}

By carefully analysing the formula for $\widehat{\alpha}^\ast$ we conclude that, in our case,

||\widehat{\alpha},\mathfrak{F}||(s_0)(\chi_{\{w0\}}) = 0.

Similarily, by (<ref>) we have

\begin{align*}
||\widehat{\alpha},\mathfrak{F}||(s_0)(\chi_{\{w1\}}) =
\frac12 \cdot \widehat{\alpha}^\ast (s_0)( \chi_{\mathfrak{F},\{w1\}_{/0}})+
\frac12 \cdot \widehat{\alpha}^\ast (s_1)( \chi_{\mathfrak{F},\{w1\}_{/1}}).
\end{align*}

In this case, however, a thorough analysis of the formula for $\widehat{\alpha}^\ast$ leads
us to the following conclusion:

||\widehat{\alpha},\mathfrak{F}||(s_0)(\chi_{\{w1\}})=\left (\frac12\right)^{n+1}.

Now, in order to compute $||\widehat{\alpha},\mathfrak{F}||_\omega$ first consider
$\mathfrak{f_F}\cdot \widehat{\alpha}^+$ which is given by:

\[
\mathfrak{f_F}\cdot \widehat{\alpha}^+(s_i)(d) =
\widehat{\alpha}^+(s_i)\left( (\sigma,s_0)\mapsto 0 \text{ and }
(\sigma,s_1)\mapsto d(\sigma,s_1) \text{ and } v\mapsto d(v) \right).
\]

The morphism
$||\widehat{\alpha},\mathfrak{F}||_\omega=(\mathfrak{f_F}\cdot \widehat{\alpha}^+)^\omega:
X\to ( \Sigma^\omega \to [0,1]) \to_\omega [0,1]$
is the greatest map satisfying
$(\mathfrak{f_F}\cdot \widehat{\alpha}^+)^\omega =
(\mathfrak{f_F} \cdot \widehat{\alpha}^+)^\omega
\cdot \mathfrak{f_F}\cdot \widehat{\alpha}^+$. In particular, this means that

\begin{align*}
& (\mathfrak{f_F}\cdot \widehat{\alpha}^+)^\omega (s_i) (d) =
(\mathfrak{f_F}\cdot \widehat{\alpha}^+)^\omega\cdot
\mathfrak{f_F}\cdot \widehat{\alpha}^+ (s_i) (d) = \\
& (\mathfrak{f_F}\cdot \widehat{\alpha}^+)(s_i)( (\sigma,s_j)\mapsto
(\mathfrak{f_F}\cdot \widehat{\alpha}^+)^\omega (s_j) (d_{|\sigma})\text{ and }v\mapsto d(v)  )
\end{align*}

For $d=\chi_{\Sigma^\omega}$ we have $d_{|\sigma} = \chi_{\Sigma^\omega}$ and hence
$(\mathfrak{f_F}\cdot \widehat{\alpha}^+)^\omega$ solves to the following equation for $x$:

\begin{align}
& x (s_i) (\chi_{\Sigma^\omega}) =
(\mathfrak{f_F}\cdot \widehat{\alpha}^+)(s_i)( (\sigma,s_j)\mapsto
x (s_j)
(\chi_{\Sigma^\omega})\text{ and }v\mapsto 1  ). \label{equation:fixpoint}
\end{align}

In order to compute
$(\mathfrak{f_F}\cdot \widehat{\alpha}^+)^\omega (s_i) (\chi_{\Sigma^\omega})$
take  $d':\Sigma^\ast \times X+\Sigma^\omega\to [0,1]$ given by
$(\sigma,s_0)\mapsto 0 \text{ and } (\sigma,s_1)\mapsto 1 \text{ and } v\mapsto 1$
and note that it satisfies $d'_{|\sigma} = d'$. Moreover, it is not hard to see that
$\widehat{\alpha}^\ast(s_i)(d')=1$[Indeed, $\widehat{\alpha}^\ast(s_1)(d')=1$
follows trivially from the fact that $d'(\varepsilon,s_1){=}1$.
By the recursive formula describing $\widehat{\alpha}^\ast$ and by induction
we show that
$\widehat{\alpha}^\ast (s_0)(d') \geq \frac12 + \frac14+\ldots + \frac{1}{2^n}$
for any $n\in \mathbb{N}$. This proves the assertion.]. Therefore, the following equation holds:

\begin{align*}
& 1= \frac12 \cdot 1 + \frac12 \cdot 1 = \\
\frac12 \cdot \widehat{\alpha}^\ast(s_0)(d') + \frac12 \cdot \widehat{\alpha}^\ast (s_1)(d')
= \widehat{\alpha}^+(s_i) (d') = \\
& (\mathfrak{f_F}\cdot \widehat{\alpha}^+)(s_i)( (\sigma,s_j)\mapsto
1\text{ and }v\mapsto 1  ).
\end{align*}

This proves that if we put
$(\mathfrak{f_F}\cdot \widehat{\alpha}^+)^\omega (s_i) (\chi_{\Sigma^\omega})=1$
then it satisfies (<ref>). Thus,
$||\widehat{\alpha},\mathfrak{F}||_\omega (s_i)(\chi_{\Sigma^\omega}) =1$.

By  Theorem <ref> probabilistic automata
can be put into the framework of Section <ref>. Hence, Kleene theorems
hold for any suitable choice of $\mathcal{A}$. In particular, we may take
$\mathcal{A}$ to be the least set of maps containing all morphisms of the form

\[
n\stackrel{\alpha}{\to}\mathcal{D}(\Sigma\times n)
\stackrel{\nu_{\Sigma\times n}}{\to }
\mathfrak{D}(\Sigma\times n)
\hookrightarrow \mathfrak{D}(\Sigma^\ast\times n+\Sigma^\omega)
\]

and satisfying the properties listed in the beginning of
Subsection <ref>.

§.§ Summary

The purpose of this section was to put probabilistic automata into
a monadic framework from Section <ref> and reason
about their (in)finite behaviours. We achieved this by introducing the
continuous continuation monad $\mathfrak{D}$ and viewing probabilistic automata
transition maps as coalgebras

X\to \mathfrak{D}(\Sigma^\ast \times X+\Sigma^\omega).

The monad $\mathfrak{D}(\Sigma^\ast \times \mathcal{I}d+\Sigma^\omega)$ gives rise
to a Kleisli category which satisfies (<ref>)-(<ref>) from
Section <ref> making
it possible to consider finite and infinite behaviours of automata taken
into consideration. We proved that the behaviour maps encode probabilities of certain
events from the execution space. These probabilities were attained without changing the
underlying category: the type monad and the automata taken into consideration
are $\mathsf{Set}$-based. Additionally, Theorem <ref>
suggests that our infinite behaviour with BAC for probabilistic automata is
similar to the one presented in [49]. However,
in loc. cit. the base category for probabilistic systems was the category
of measurable spaces and measurable functions. Hence,
by Remark <ref>, Kleene theorems can be instantiated in
our setting directly, but it is not possible to do so in the
setting from [49].

§ SUMMARY

The purpose of this paper was to develop a coalgebraic (categorical) framework
to reason about abstract automata and their finite and infinite behaviours
satisfying BAC. We achieved this goal by constructing a monad suitable for handling
the types of behaviours we were interested in and defining them in the right
setting. A natural and direct consequence of this treatment was Theorem
<ref> and Theorem <ref>,
i.e. a (co)algebraic characterization of regular and $\omega$-regular behaviour
for systems whose type is a $\mathsf{Set}$-based monad satisfying some
additional properties. Our theory of finite and infinite behaviour for abstract automata has been
successfully instantiated on: non-deterministic automata, tree
automata and probabilistic automata.

§.§.§ Future work

Given our natural characterization of coalgebraic ($\omega$-)regular languages we
ask if it is possible to characterize it in terms of
a preimage of a subset of a finite algebraic structure. Especially, considering
the fact that by Theorem <ref> the pair of hom-sets
$(\mathbb{T}(n,n),\mathbb{T}(n,0))$ equipped with suitable operations resembles
a Wilke algebra used in the algebraic characterization of these languages (see
e.g. [40] for details).

§.§.§ Related work

The first coalgebraic take on $\omega$-languages was presented in
[16], where authors put deterministic Muller
automata with Muller acceptance condition into a coalgebraic framework.  Our work is
related to a more recent paper [49], where Urabe
et al. give a coalgebraic framework for modelling behaviour with Büchi
acceptance condition for $(T,F)$-systems. The main ingredient of their work is a
solution to a system of equations which uses least and greatest fixpoints. This
is done akin to Park's [39] classical
characterization of $\omega$-languages via a system of equations. In our paper
we also use least and greatest fixpoints, however, the operators we consider are
the two natural types of  operators $(-)^\ast=\mu x. \mathsf{id} \vee x\cdot
(-)$ and $(-)^\omega=\nu x. x\cdot (-)$ which generalize the language operators
$(-)^\ast$ and $(-)^\omega$ known from the classical theory of regular and
$\omega$-regular languages. The definitions of behaviours
of an automaton are presented in terms of simple expressions involving Kleisli
composition and the above operators.
This allows us to state and prove generic Kleene theorems
for ($\omega$-)regular input which was not achieved in
[49] and (in our opinion) would be difficult to
obtain in that setting. To summarize, the major differences between our work and
[49] are the following:

* we use the setting of systems with internal moves (i.e. coalgebras over a
monad) to discuss infinite behaviour with BAC, which is given in terms of a simple
expression using $(-)^\ast$ and $(-)^\omega$ in the Kleisli category,

* we provide the definition of (in)finite behaviours of a system
and build a bridge between regular and $\omega$-regular behaviours
by characterizing them on a categorical level in terms of the Kleene theorems.

Abstract finite automata have already been considered in the computer science
literature in the context of Lawvere iteration theories with analogues of Kleene
theorems stated and proven (see e.g.
[18, 20, 21, 19, 8]). Some of these results
seem to be presented  using a slightly
different language than ours (see Theorem <ref>
and e.g. <cit.>). We decided to state
Theorem <ref> the way we did, in order to make a direct
generalization of the classical Kleene theorem for regular input and to give a
coalgebraic interpretation which is missing in
[18, 20, 21, 19, 8].  We should also
mention that the infinite behaviour with BAC was defined in loc. cit.
only for a very specific type of theories (i.e. the matricial theories over an
algebra with an infinite iteration operator), which do not encompass e.g.
non-deterministic Büchi tree automata and their infinite tree languages or
probabilistic automata and their infinite behaviour.

[1]
J. Adámek, M. Haddadi, and S. Milius.
Corecursive algebras, corecursive monads and bloom monads.
Logical Methods in Computer Science, 10(3), 2014.

[2]
C. Baier, B. Engelen, and M. E. Majster-Cederbaum.
Deciding bisimilarity and similarity for probabilistic processes.
J. Comput. Syst. Sci., 60(1):187–231, 2000.

[3]
C. Baier and M. Grosser.
Recognizing omega-regular languages with probabilistic automata.
In Proceedings of the 20th Annual IEEE Symposium on Logic in
Computer Science, LICS '05, pages 137–146, Washington, DC, USA, 2005. IEEE
Computer Society.

[4]
C. Baier, M. Grösser, and N. Bertrand.
Probabilistic omega-automata.
J. ACM, 59(1):1:1–1:52, Mar. 2012.

[5]
C. Baier and H. Hermanns.
Weak bisimulation for fully probabilistic processes.
In CAV, pages 119–130, 1997.

[6]
M. Barr and C. Wells.
Toposes, Triples and Theories.

[7]
J. Beck.
Distributive laws.
In B. Eckmann, editor, Seminar on Triples and Categorical
Homology Theory, pages 119–140, Berlin, Heidelberg, 1969. Springer Berlin

[8]
S. Bloom and Z. Ésik.
Iteration Theories. The Equational Logic of Iterative
Monographs in Theoretical Computer Science. Springer, 1993.

[9]
F. Bonchi, S. Milius, A. Silva, and F. Zanasi.
Killing epsilons with a dagger: A coalgebraic study of systems with
algebraic label structure.
Theoretical Computer Science, 604:102–126, 2015.

[10]
T. Brengos.
On coalgebras with internal moves.
In M. M. Bonsangue, editor, Proc. CMCS, Lecture Notes in
Computer Science, pages 75–97. Springer, 2014.

[11]
T. Brengos.
Weak bisimulation for coalgebras over order enriched monads.
Logical Methods in Computer Science, 11(2):1–44, 2015.

[12]
T. Brengos.
A Coalgebraic Take on Regular and omega-Regular Behaviour for
Systems with Internal Moves.
In S. Schewe and L. Zhang, editors, 29th International
Conference on Concurrency Theory (CONCUR 2018), volume 118 of Leibniz
International Proceedings in Informatics (LIPIcs), pages 25:1–25:18,
Dagstuhl, Germany, 2018. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.

[13]
T. Brengos, M. Miculan, and M. Peressotti.
Behavioural equivalences for coalgebras with unobservable moves.
Journal of Logical and Algebraic Methods in Programming,
84(6):826–852, 2015.

[14]
T. Brengos and M. Peressotti.
A Uniform Framework for Timed Automata.
In J. Desharnais and R. Jagadeesan, editors, 27th International
Conference on Concurrency Theory (CONCUR 2016), volume 59 of Leibniz
International Proceedings in Informatics (LIPIcs), pages 26:1–26:15,
Dagstuhl, Germany, 2016. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.

[15]
J. R. Büchi.
On a Decision Method in Restricted Second Order Arithmetic,
pages 425–435.
Springer New York, New York, NY, 1990.

[16]
V. Ciancia and Y. Venema.
Stream automata are coalgebras.
In Proc. CMCS, volume 7399 of Lecture Notes in Computer
Science, pages 90–108, 2012.

[17]
C. Cîrstea.
Generic infinite traces and path-based coalgebraic temporal logics.
Electr. Notes Theor. Comput. Sci., 264(2):83–103, 2010.

[18]
Z. Ésik.
Completeness of Park induction.
Theor. Comput. Sci., 177(1):217–283, 1997.

[19]
Z. Ésik and T. Hajgató.
Iteration grove theories with applications.
In Proc. Algebraic Informatics, volume 5725 of Lecture
Notes in Computer Science, pages 227–249. Springer, 2009.

[20]
Z. Ésik and W. Kuich.
A Unifying Kleene Theorem for Weighted Finite Automata, pages
Springer Berlin Heidelberg, Berlin, Heidelberg, 2011.

[21]
Z. Ésik and W. Kuich.
Modern Automata Theory, page 222.

[22]
B. Fong and D. I. Spivak.
Seven Sketches in Compositionality: An Invitation to Applied
Category Theory.
arxiv:1803.05316, 2018.

[23]
S. Goncharov and D. Pattinson.
Coalgebraic weak bisimulation from recursive equations over monads.
In J. Esparza, P. Fraigniaud, T. Husfeldt, and E. Koutsoupias,
editors, Proc. ICALP, volume 8573 of Lecture Notes in Computer
Science, pages 196–207. Springer, 2014.

[24]
E. Grädel, W. Thomas, and T. Wilke, editors.
Automata Logics, and Infinite Games: A Guide to Current
Research, page 392.
Springer-Verlag New York, Inc., New York, NY, USA, 2002.

[25]
H. P. Gumm.
Elements of the general theory of coalgebras.
LUATCS 99, Rand Afrikaans University, 1999.

[26]
I. Hasuo.
Generic forward and backward simulations.
In Prof. CONCUR, volume 4137 of Lecture Notes in Computer
Science, pages 406–420, 2006.

[27]
I. Hasuo, B. Jacobs, and A. Sokolova.
Generic trace semantics via coinduction.
Logical Methods in Computer Science, 3(4), 2007.

[28]
J. E. Hopcroft, R. Motwani, Rotwani, and J. D. Ullman.
Introduction to Automata Theory, Languages and Computability.
Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2nd
edition, 2000.

[29]
M. Hyland and J. Power.
The category theoretic understanding of universal algebra: Lawvere
theories and monads.
Electronic Notes in Theoretical Computer Science, 172:437–458,

[30]
B. Jacobs.
Trace semantics for coalgebras.
Electr. Notes Theor. Comput. Sci., 106:167–184, 2004.

[31]
B. Jacobs, A. Silva, and A. Sokolova.
Trace semantics via determinization.
In Proc. CMCS, volume 7399 of Lecture Notes in Computer
Science, pages 109–129, 2012.

[32]
B. Khoussainov and A. Nerode.
Automata Theory and Its Applications.
Birkhauser Boston, Inc., USA, 2001.

[33]
S. C. Kleene.
Representation of events in nerve nets and finite automata.
In C. Shannon and J. McCarthy, editors, Automata Studies, pages
3–41. Princeton University Press, Princeton, NJ, 1956.

[34]
A. Kock.
Strong functors and monoidal monads.
Archiv der Mathematik, 23(1):113–120, 1972.

[35]
F. W. Lawvere.
Functorial semantics of algebraic theories.
Proc. Nat. Acad. Sci. U.S.A., 50:869–872, 1963.

[36]
S. Mac Lane.
Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics.
Springer-Verlang New York, 1978.

[37]
R. Milner.
Communication and Concurrency.
Prentice-Hall, 1989.

[38]
P. S. Mulry.
Lifting theorems for Kleisli categories.
In S. D. Brookes, M. G. Main, A. Melton, M. W. Mislove, and D. A.
Schmidt, editors, Mathematical Foundations of Programming Semantics,
9th International Conference, New Orleans, LA, USA, April
7-10, 1993, Proceedings, volume 802 of Lecture Notes in Computer
Science, pages 304–319. Springer, 1993.

[39]
D. Park.
Concurrency and automata on infinite sequences.
In P. Deussen, editor, Theoretical Computer Science, pages
167–183, Berlin, Heidelberg, 1981. Springer Berlin Heidelberg.

[40]
J.-E. Pin and D. Perrin.
Infinite Words: Automata, Semigroups, Logic and Games, page
Elsevier, 2004.

[41]
J. J. M. M. Rutten.
Universal coalgebra: a theory of systems.
Theoretical Computer Science, 249(1):3–80, 2000.

[42]
D. Sangiorgi.
Introduction to Bisimulation and Coinduction.
Cambridge University Press, 2011.

[43]
P. Selinger.
A survey of graphical languages for monoidal categories.
volume 813, pages 289–355, 2011.

[44]
A. Silva and B. Westerbaan.
A coalgebraic view of $\epsilon$-transitions.
In R. Heckel and S. Milius, editors, Proc. CALCO, volume 8089
of Lecture Notes in Computer Science, pages 267–281. Springer, 2013.

[45]
A. Simpson and G. Plotkin.
Complete axioms for categorical fixed-point operators.
In Proceedings of the 15th Annual IEEE Symposium on Logic in
Computer Science, LICS '00, pages 30–, Washington, DC, USA, 2000. IEEE
Computer Society.

[46]
A. Sokolova.
Probabilistic systems coalgebraically: A survey.
Theoretical Computer Science, 412(38):5095–5110, 2011.

[47]
A. Sokolova, E. P. de Vink, and H. Woracek.
Coalgebraic weak bisimulation for action-type systems.
Scientific Annals of Computer Science, 19:93–144, 2009.

[48]
N. Urabe and I. Hasuo.
Coalgebraic infinite traces and Kleisli simulations.
CoRR, abs/1505.06819, 2015.

[49]
N. Urabe, S. Shimizu, and I. Hasuo.
Coalgebraic Trace Semantics for Buechi and Parity Automata.
In J. Desharnais and R. Jagadeesan, editors, 27th International
Conference on Concurrency Theory (CONCUR 2016), volume 59 of Leibniz
International Proceedings in Informatics (LIPIcs), pages 24:1–24:15,
Dagstuhl, Germany, 2016. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.


| 0.0707 | 17285 | 5.60e-02 | $--$ | 2.77e-01 | $--$ | 7.07e-02 | $--$ | 1.02e-01 | $--$ | 4.85e-02 | $--$
| 0.0566 | 26855 | 4.48e-02 | 1.00 | 2.23e-01 | 0.97 | 5.66e-02 | 1.00 | 8.15e-02 | 1.00 | 3.88e-02 | 1.00
| 0.0471 | 38525 | 3.73e-02 | 1.00 | 1.87e-01 | 0.97 | 4.72e-02 | 1.00 | 6.80e-02 | 1.00 | 3.23e-02 | 1.00
0 | 0.0404 | 52295 | 3.20e-02 | 1.00 | 1.61e-01 | 0.96 | 4.04e-02 | 1.00 | 5.83e-02 | 1.00 | 2.77e-02 | 1.00
| 0.0354 | 68165 | 2.80e-02 | 1.00 | 1.42e-01 | 0.96 | 3.54e-02 | 1.00 | 5.10e-02 | 1.00 | 2.42e-02 | 1.00
| 0.0236 | 152645 | 1.87e-02 | 1.00 | 9.63e-02 | 0.95 | 2.36e-02 | 1.00 | 3.40e-02 | 1.00 | 1.61e-02 | 1.00
| 0.0166 | 305495 | 1.32e-02 | 1.00 | 6.94e-02 | 0.94 | 1.66e-02 | 1.00 | 2.40e-02 | 1.00 | 1.14e-02 | 1.00
| 0.0135 | 465575 | 1.07e-02 | 1.00 | 5.69e-02 | 0.93 | 1.35e-02 | 1.00 | 1.94e-02 | 1.00 | 9.22e-03 | 1.00
| 0.0707 | 58565 | 2.34e-04 | $--$ | 2.67e-02 | $--$ | 1.35e-04 | $--$ | 1.45e-03 | $--$ | 7.06e-04 | $--$
| 0.0566 | 91205 | 1.56e-04 | 1.82 | 2.30e-02 | 0.68 | 9.20e-05 | 1.71 | 9.30e-04 | 2.00 | 4.62e-04 | 1.90
1 | 0.0471 | 131045 | 1.12e-04 | 1.81 | 2.03e-02 | 0.67 | 6.75e-05 | 1.69 | 6.46e-04 | 2.00 | 3.27e-04 | 1.89
| 0.0404 | 178085 | 8.47e-05 | 1.81 | 1.83e-02 | 0.67 | 5.21e-05 | 1.69 | 4.75e-04 | 2.00 | 2.44e-04 | 1.89
| 0.0354 | 232325 | 6.66e-05 | 1.80 | 1.68e-02 | 0.67 | 4.16e-05 | 1.68 | 3.63e-04 | 2.00 | 1.90e-04 | 1.88
| 0.0236 | 521285 | 3.23e-05 | 1.79 | 1.28e-02 | 0.67 | 2.11e-05 | 1.68 | 1.62e-04 | 2.00 | 8.93e-05 | 1.86
| 0.0707 | 123845 | 3.00e-05 | $--$ | 1.52e-02 | $--$ | 3.29e-05 | $--$ | 1.64e-05 | $--$ | 8.29e-05 | $--$
| 0.0566 | 193055 | 2.07e-05 | 1.67 | 1.31e-02 | 0.67 | 2.27e-05 | 1.67 | 8.39e-06 | 3.01 | 5.70e-05 | 1.68
2 | 0.0471 | 277565 | 1.52e-05 | 1.67 | 1.16e-02 | 0.67 | 1.67e-05 | 1.67 | 4.85e-06 | 3.01 | 4.20e-05 | 1.67
| 0.0404 | 377375 | 1.18e-05 | 1.67 | 1.05e-02 | 0.67 | 1.29e-05 | 1.67 | 3.05e-06 | 3.00 | 3.25e-05 | 1.67
| 0.0354 | 492485 | 9.44e-06 | 1.67 | 9.60e-03 | 0.67 | 1.04e-05 | 1.67 | 2.04e-06 | 3.00 | 2.60e-05 | 1.67
Table 2: History of convergence for Example 2.

Example 3. Finally, we aim to illustrate the accuracy of our method by
considering a case in which the exact solution is unknown in the a time-
dependent approach. More precisely, we add $\partial_{t}\boldsymbol{u}$ and
$\partial_{t}\boldsymbol{\varphi}$ to the left-hand side of first and last
equations of (2.1), respectively, which, together with the boundary conditions
(2.4), we consider initial conditions

$\boldsymbol{u}(\cdot,0)\,=\,\boldsymbol{u}_{0}\,\hskip 5.69046pt\mbox{in
}\Omega\qquad\mbox{and}\qquad\boldsymbol{\varphi}(\cdot,0)\,=\,\boldsymbol{\varphi}_{0}\,\hskip
5.69046pt\mbox{in }\Omega\,.$

We remark here that, in similar way of [33], the analysis presented along of
this paper can be extended to this time-dependent problem by employing
backward Euler time stepping in order to obtain a fully-discrete method. On
the other hand, for this example we consider once again the unit square
$\Omega=(0,1)^{2}$, and set
${\Gamma_{\mathrm{D}}}=\left\\{(0,s),(1,s)\in\text{\rm R}^{2}\,:\,0\leq s\leq
1\right\\}$, ${\Gamma_{\mathrm{N}}}=\Gamma\setminus{\Gamma_{\mathrm{D}}}$,
$\gamma=10^{-3}$, $\nu({\boldsymbol{x}})=10^{-2}$,
$\boldsymbol{\alpha}=(1,10)^{\mathrm{t}}$,
$\mathbb{K}=\left(\begin{smallmatrix}1&0\\\\[2.15277pt]
0&10^{-1}\end{smallmatrix}\right)$. The boundary condition is defined as

$\boldsymbol{\varphi}_{{\mathrm{D}}}({\boldsymbol{x}},t)\ =\
\left\\{\begin{array}[]{cl}(1,1)^{\mathrm{t}}&\text{if }x_{1}=0\\\\[4.30554pt]
(-1,-1)^{\mathrm{t}}&\text{if }x_{1}=1\end{array}\right.$

for all ${\boldsymbol{x}}:=(x_{1},x_{2})^{\mathrm{t}}\in\Omega$, whereas the
initial conditions are given by

$\boldsymbol{u}_{0}({\boldsymbol{x}})\ =\ \left(\begin{array}[]{r}\sin^{2}(\pi
x_{1})\sin(2\pi x_{2})\\\\[4.30554pt] -\sin(2\pi x_{1})\sin^{2}(\pi
x_{2})\end{array}\right)\qquad\text{and}\qquad\boldsymbol{\varphi}_{0}({\boldsymbol{x}})\
=\ \left(\begin{array}[]{r}\exp(x_{1}+x_{2})\\\\[4.30554pt]
\exp(x_{1}-x_{2})\end{array}\right)\,.$

In addition, for the time stepping technique we use $\triangle
t=\frac{1}{50}$.

In Table 3, we summarize the convergence history, where we can note that the
rate of convergence $O(h^{k+1})$ predicted by Theorem 5.5 is attained by all
the unknowns for $k=0$ and time step $t_{25}=0.5$. We mention that the errors
and the convergence rates are computed by considering the discrete solution
obtained with a finer mesh ($N=28895$) as the exact solution. Additionally, in
Figures 1 and 2, we display the approximation of the velocity components,
temperature and concentration. All the figures presented there were obtained
with $N=28895$ degrees of freedom (used as exact solution) in the time step
$t_{\ell}:=\ell\cdot\triangle t$, with $\ell\in\\{1,5,10,15,20\\}$.

$k$ | $h$ | $N$ | $\mathtt{e}(\boldsymbol{t})$ | $\mathtt{r}(\boldsymbol{t})$ | $\mathtt{e}(\boldsymbol{\sigma})$ | $\mathtt{r}(\boldsymbol{\sigma})$ | $\mathtt{e}(\boldsymbol{u})$ | $\mathtt{r}(\boldsymbol{u})$ | $\mathtt{e}(\boldsymbol{\varphi})$ | $\mathtt{r}(\boldsymbol{\varphi})$ | $\mathtt{e}(p)$ | $\mathtt{r}(p)$
---|---|---|---|---|---|---|---|---|---|---|---|---
| 0.0707 | 5845 | 4.47e+01 | $--$ | 1.07e+01 | $--$ | 5.79e-01 | $--$ | 5.15e-01 | $--$ | 8.63e-01 | $--$
| 0.0566 | 9055 | 3.57e+01 | 1.01 | 8.35e+00 | 1.10 | 4.54e-01 | 1.08 | 4.02e-01 | 1.12 | 6.86e-01 | 1.03
0 | 0.0471 | 12965 | 2.95e+01 | 1.05 | 6.80e+00 | 1.13 | 3.61e-01 | 1.26 | 3.21e-01 | 1.24 | 5.66e-01 | 1.05
| 0.0404 | 17575 | 2.53e+01 | 0.99 | 5.72e+00 | 1.12 | 3.08e-01 | 1.03 | 2.70e-01 | 1.11 | 4.85e-01 | 1.01
| 0.0354 | 22885 | 2.21e+01 | 1.03 | 4.93e+00 | 1.11 | 2.68e-01 | 1.02 | 2.34e-01 | 1.08 | 4.19e-01 | 1.09
Table 3: History of convergence for Example 3 for $t=0.5$.

Figure 1: Example 3, velocity components $u_{h,1}$ (left) and $u_{h,2}$
(right), obtained with a fully-discrete time-dependent mixed method with no
manufactured analytical solution using $k=0$ and $N=28895$ degrees of freedom.
We plot for $t\in\\{t_{1},t_{5},t_{10},t_{15},t_{20}\\}$, en each row.

Figure 2: Example 3, temperature $\varphi_{h,1}$ (left) and concentration
$\varphi_{h,2}$ (right), obtained with a fully-discrete time-dependent mixed
method with no manufactured analytical solution using $k=0$ and $N=28895$
degrees of freedom. We plot for $t\in\\{t_{1},t_{5},t_{10},t_{15},t_{20}\\}$,
en each row.

## References

  * [1] J. Abedi, S. Aliabadi, Simulation of incompressible flows with heat and mass transfer using parallel finite element method. Electronic J. Diff. Eq., Conference 10 (2003), 1–11.
  * [2] R.A. Adams and J.J.F. Fournier, Sobolev Spaces. Second edition. Pure and Applied Mathematics (Amsterdan), 140. Elsevier/Academic Press, Amsterdam, 2003.
  * [3] G. Alekseev, D. Tereshko and V. Pukhnachev. Boundary control problems for Oberbeck-Boussinesq model of heat and mass transfer. Advanced Topics in Mass Transfer (2011), 485–512.
  * [4] J.A. Almonacid, G.N. Gatica and R. Oyarzúa, A new mixed finite element method for the n-dimensional Boussinesq problem with temperature-dependent viscosity. Calcolo 55 (2018), no. 3, Art. 36, 42pp.
  * [5] M. Alvarez, G.N. Gatica, B. Gómez-Vargas and R. Ruiz-Baier, New mixed finite element methods for natural convection with phase-change in porous media. J. Sci. Comput. 80 (2019), no. 1, 141–174.
  * [6] M. Alvarez, G.N. Gatica and R. Ruiz-Baier, A mixed-primal element approximation of a sedimentation-consolidation system. M3AS: Math. Models Methods Appl. Sci., 26 (2016), no. 5, 867–900.
  * [7] M. Alvarez, G.N. Gatica and R. Ruiz-Baier, An augmented mixed-primal finite element method for a coupled flow-transport problem. ESAIM Math. Model. Numer. Anal. 49 (2015), no. 5, 1399–1427.
  * [8] M. Alvarez, G.N. Gatica, B. Gomez-Vargas, R. Ruiz-Baier, New Mixed Finite Element Nethods For Natural Convection with Phase-Change in Porous Media. Journal of Scientific Computing. vol. 80, 1, pp. 141-174, (2019).
  * [9] F. Brezzi and M. Fortin, Mixed and Hybrid Finite Element Methods. Springer Series in Computational Mathematics, 15. Springer-Verlag, New York, 1991.
  * [10] R. Bürger, P.E. Méndez and R. Ruiz-Baier, On H(div)-conforming methods for double-diffusion equations in porous media. SIAM J. Numer. Anal. 57 (2019), no. 3, 1318–1343.
  * [11] E. Cáceres and G.N. Gatica, A mixed virtual element method for the pseudostress-velocity formulation of the Stokes problem. IMA J. Numer. Anal. 37 (2017), no. 1, 296–331.
  * [12] J. Camaño, G.N. Gatica, R. Oyarzúa and G. Tierra, An augmented mixed finite element method for the Navier-Stokes equations with variable viscosity. SIAM J. Numer. Anal. 54 (2016), no. 2, 1069–1092.
  * [13] S. Caucao, G. N. Gatica and R. Oyarzúa, Analysis of an augmented fully-mixed formulation for the coupling of the Stokes and heat equations. ESAIM Math. Model. Numer. Anal. 52 (2018), no. 5, 1947–1980.
  * [14] Y.Y. Chen, B.W. Li and J.K. Zhang, Spectral collocation method for natural convection in a square porous cavity with local thermal equilibrium and non-equilibrium models. Int. J. Heat Mass Transfer 64 (2013), 35–49.
  * [15] P. Cheng, Heat transfer in geothermal systems. Adv. Heat Transfer 14 (1979), 1–105.
  * [16] P.G. Ciarlet, Linear and Nonlinear Functional Analysis with Applications. Society for Industrial and Applied Mathematics, Philadelphia, PA, 2013.
  * [17] A. Çibik and S. Kaya, Finite element analysis of a projection-based stabilization method for the Darcy-Brinkman equations in double-diffusive convection. Appl. Numer. Math. 64 (2013), 35–49.
  * [18] E. Colmenares, G.N. Gatica, S. Moraga and R. Ruiz-Baier, A fully-mixed finite element method for the steady state Oberbeck-Boussinesq system. SMAI J. Comput. Math. 6 (2020), 125–157.
  * [19] E. Colmenares, G.N. Gatica and R. Oyarzúa, Fixed point strategies for mixed variational formulations of the stationary Boussinesq problem. C. R. Math. Acad. Sci. Paris 354 (2016), no. 1, 57–62.
  * [20] E. Colmenares, G.N. Gatica and R. Oyarzúa, Analysis of an augmented mixed-primal formulation for the stationary Boussinesq problem. Numer. Methods Partial Differential Equations 32 (2016), no. 2, 445–478.
  * [21] E. Colmenares, G.N. Gatica and R. Oyarzúa, An augmented fully-mixed finite element method for the stationary Boussinesq problem. Calcolo 54 (2017), no. 1, 167–205.
  * [22] H. Dallmann and D. Arndt, Stabilized finite element methods for the Oberbeck-Boussinesq model. J. Sci. Comput. 69 (2016), no. 1, 244–273.
  * [23] T.A. Davis, Algorithm 832: UMFPACK V4.3–an unsymmetric-pattern multifrontal method. ACM Trans. Math. Software 30 (2004), no. 2, 196–199.
  * [24] B. Daya Reddy Introductory Functional Analysis: With Appliations to Boundary Value Problems and Finite Elements. Texts in Applied Mathematics, Springer (1998), no. 27.
  * [25] A. Ern and J.L. Guermond, Theory and Practice of Finite Elements, Applied Mathematical Sciences, Springer (2004), no. 159.
  * [26] L.E. Figueroa, G.N. Gatica and A. Márquez, Augmented mixed finite element methods for the stationary Stokes equations. SIAM J. Sci. Comput. 31 (2008/09), no. 2, 1082–1119.
  * [27] G.N. Gatica, A Simple Introduction to the Mixed Finite Element Method. Theory and Applications. Springer Briefs in Mathematics. Springer, Cham, 2014.
  * [28] G.N. Gatica, Introducción al Análisis Funcional. Teoría y Aplicaciones. Editorial Reverte, Barcelona Bogotá Buenos Aires Caracas México, 2014.
  * [29] B. Gebhart and L. Pera, The nature of vertical natural convection flows resulting from the combined buoyancy effects of thermal and mass diffusion. Int. J. Heat Mass Transfer 14 (1971), no. 12, 2025–2050.
  * [30] B. Gebhart and L. Pera, Natural convection flows adjacent to horizontal surfaces resulting from the combined buoyancy effects of thermal and mass diffusion. Int. J. Heat Mass Transfer 15 (1972), no. 2, 269–278.
  * [31] C. Geuzaine and J.-F. Remacle, Gmsh: a three-dimensional finite element mesh generator with built-in pre- and post-processing facilities. Int. J. Numer. Methods Engrg. 79 (2009), no. 11, 1309–1331.
  * [32] V. Girault and P-A. Raviart, Finite Element Methods for Navier-Stokes Equations. Theory and Algorithms. Springer Series in Computational Mathematics, 5. Springer-Verlag, Berlin, 1986.
  * [33] J. Guzmán, F.A. Sequeira and C.W. Shu, H(div) conforming and DG methods for incompressible Euler’s equations. IMA J. Numer. Anal. 37 (2017), no. 4, 1733–1771.
  * [34] M. Hammami, M. Mseddi and Mounir Baccar, Numerical Study of Coupled Heat and Mass Transfer in a Trapezoidal Cavity. Eng. Appl. Comput. Fluid Mech. 1 (2007), no. 3, 216–226.
  * [35] M. Karimi-Fard, M.C. Charrier-Mojtabi and K. Vafai, Non-Darcian effects on double-diffusive convection within a porous medium. Numer. Heat Transfer, Part A: Appl. 31 (1997), no. 8, 837–852.
  * [36] W. McLean, Strongly elliptic systems and boundary integral equations. Cambridge University Press, Cambridge, 2000.
  * [37] A. Mojtabi and M.C. Charrier-Mojtabi, Double-diffusive convection in porous media. Handbook of Porous Media, Part III. Taylor and Francis, 2005.
  * [38] N. Moraga, C. Zambra, P. Torres and R Lemus-Mondaca, Fluid dinamics, heat and mass transfer modelling by finite volume method for agrofood processes. DYNA 78 (2011), 140–149.
  * [39] D.A. Nield and A. Bejan, Convection in porous media. Second edition. Springer Science and & Business Media. Springer-Verlag, New York, 1999.
  * [40] R. Oyarzúa, T. Qin and D. Schötzau, An exactly divergence-free finite element method for a generalized Boussinesq problem. IMA J. Numer. Anal. 34 (2014), no. 3, 1104–1135.
  * [41] A. Quarteroni and A. Valli. Numerical Approximation of Partial Differential Equations. Springer Series in Computational Mathematics, 23. Springer-Verlag, Berlin, 1994.
  * [42] P.-A. Raviart and J.-M. Thomas, Introduction à l’Analyse Numérique des Équations aux Dérivées Partielles. (French) [Introduction to the numerical analysis of partial differential equations] Collection Mathématiques Appliquées pour la Maîtrise. Masson, Paris, 1983.
  * [43] J.E. Roberts and J.-M. Thomas, Mixed and Hybrid Methods. Handbook of numerical analysis, vol. II, 523–639, Handb. Numer. Anal., II, North-Holland, Amsterdam, 1991.
  * [44] S. C. Saha and A. Hossain, Natural convection flow with combined buoyancy effects due to thermal and mass diffusion in a thermally stratified media. Nonlinear Analysis: Modelling and Control 9 (2004), 89–102.
  * [45] L.R. Scott and S. Zhang, Finite element interpolation of nonsmooth functions satisfying boundary conditions. Math. Comp. 54 (1990), no. 190, 483–493.