---
abstract: 'We introduce a novel technique to analyse unambiguous Büchi automata quantitatively, and apply this to the model checking problem. It is based on linear-algebra arguments that originate from the analysis of matrix semigroups with constant spectral radius. This method can replace a combinatorial procedure that dominates the computational complexity of the existing procedure by Baier et al. We analyse the complexity in detail, showing that, in terms of the set $Q$ of states of the automaton, the new algorithm runs in time $O(|Q|^4)$, improving on an efficient implementation of the combinatorial algorithm by a factor of $|Q|$.'
author:
- Stefan Kiefer
- Cas Widdershoven
bibliography:
- 'ms.bib'
title: Efficient Analysis of Unambiguous Automata Using Matrix Semigroup Techniques
---

Introduction
============

Preliminaries {#sec:prelim}
=============

We assume the reader to be familiar with basic notions of finite automata over infinite words and Markov chains, see, e.g., @GraedelThomasWilke02 [@Kulkarni]. In the following we provide a brief summary of our notation and a few facts related to linear algebra.

##### Finite automata. {#finite-automata. .unnumbered}

A *Büchi automaton* is a tuple $\cA = (Q,\Sigma,\delta,Q_0,F)$ where $Q$ is the finite set of states, $Q_0 \subseteq Q$ is the set of initial states, $\Sigma$ is the finite alphabet, $\delta: Q \times \Sigma \to 2^Q$ is the transition function, and $F \subseteq Q$ is the set of accepting states. We extend the transition function to $\delta: Q \times \Sigma^* \to 2^Q$ and to $\delta: 2^Q \times \Sigma^* \to 2^Q$ in the standard way. For $q \in Q$ we write $\cA_q$ for the automaton obtained from $\cA$ by making $q$ the only initial state.

Given states $q,r\in Q$ and a finite word $w = a_0 a_1 \cdots a_{n-1} \in \Sigma^*$, a *run* for $w$ from $q$ to $r$ is a sequence $q_0 q_1 \cdots q_n \in Q^{n+1}$ with $q_0=q$, $q_n=r$ and $q_{i+1} \in \delta(q_i,a_i)$ for $i \in \{0, \ldots, n-1\}$. A *run* in $\cA$ for an infinite word $w = a_0 a_1 a_2 \cdots \in \Sigma^{\omega}$ is an infinite sequence $\rho = q_0 q_1 \cdots \in Q^{\omega}$ such that $q_0 \in Q_0$ and $q_{i+1} \in \delta(q_i,a_i)$ for all $i \in \Nat$. Run $\rho$ is called *accepting* if $\inf(\rho) \cap F \ne \emptyset$ where $\inf(\rho) \subseteq Q$ is the set of states that occur infinitely often in $\rho$. The *language* $\cL(\cA)$ of accepted words consists of all infinite words $w\in \Sigma^{\omega}$ that have at least one accepting run. $\cA$ is called *unambiguous* if each word $w\in \Sigma^{\omega}$ has at most one accepting run. We use the acronym UBA for unambiguous Büchi automaton.

We define $|\delta| := |\{(q,r) \mid \exists\, a \in \Sigma : r \in \delta(q,a)\}|$, i.e., $|\delta| \le |Q|^2$ is the number of transitions in $\cA$ when allowing for multiple labels per transition. In Appendix \[app-A\] we give an example that shows that the number of transitions can be quadratic in $|Q|$, even for UBAs with a strongly connected state space. We assume $|Q| \le |\delta|$, as states without outgoing transitions can be removed. In this paper, $\Sigma$ may be a large set (of states in a Markov chain), so it is imperative to allow for multiple labels per transition. We use a lookup table to check in constant time whether $r \in \delta(q,a)$ holds for given $r, q, a$. A *diamond* is given by two states $q, r \in Q$ and a finite word $w$ such that there exist at least two distinct runs for $w$ from $q$ to $r$. One can remove diamonds (see Appendix \[app:prelims\]):

<span>ourlemma</span><span>lemdiamondfree</span>\[lem:diamondfree\] Given a UBA, one can compute in time $O(|\delta|^2|\Sigma|)$ a UBA of at most the same size, with the same language and without diamonds.

For the rest of the paper, we assume that UBAs do not have diamonds.

##### Vectors and matrices. {#vectors-and-matrices. .unnumbered}

We consider vectors and square matrices indexed by a finite set $S$. We write (column) vectors $\vec{v} \in \Real^S$ with arrows on top, and $\vec{v}^\top$ for the transpose (a row vector) of $\vec{v}$. The zero vector and the all-ones vector are denoted by $\vec{0}$ and $\vec{1}$, respectively. For a set $T \subseteq S$ we write ${\pmb{\left[\vphantom{T}\right.} T \pmb{\left.\vphantom{T}\right]}} \in \{0,1\}^S$ for the characteristic vector of $T$, i.e., ${\pmb{\left[\vphantom{T}\right.} T \pmb{\left.\vphantom{T}\right]}}_s = 1$ if $s \in T$ and ${\pmb{\left[\vphantom{T}\right.} T \pmb{\left.\vphantom{T}\right]}}_s = 0$ otherwise. A matrix $M \in [0,1]^{S \times S}$ is called *stochastic* if $M \vec{1} = \vec{1}$, i.e., if every row of $M$ sums to one. For a set $U \subseteq S$ we write $\vec{v}_U \in \Real^U$ for the restriction of $\vec{v}$ to $U$. Similarly, for $T, U \subseteq S$ we write $M_{T,U}$ for the submatrix of $M$ obtained by deleting the rows not indexed by $T$ and the columns not indexed by $U$. The (directed) *graph* of a nonnegative matrix $M \in \Real^{S \times S}$ has vertices $s \in S$ and edges $(s,t)$ if $M_{s,t} > 0$. We may implicitly associate $M$ with its graph and speak about graph-theoretic concepts such as reachability and strongly connected components (SCCs) in $M$.

##### Markov chains. {#markov-chains. .unnumbered}

A (finite-state discrete-time) *Markov chain* is a pair $\cM = (S,M)$ where $S$ is the finite set of states, and $M \in [0,1]^{S \times S}$ is a stochastic matrix that specifies transition probabilities. An *initial distribution* is a function $\iota : S \to [0,1]$ satisfying $\sum_{s \in S} \iota(s) = 1$. Such a distribution induces a probability measure $\Pr^{\cM}_\iota$ on the measurable subsets of $S^\omega$ in the standard way, see for instance @baie2008 [chapter 10.1, page 758]. If $\iota$ is concentrated on a single state $s$, we may write $\Pr^{\cM}_s$ for $\Pr^{\cM}_\iota$. We write $E$ for the set of edges in the graph of $M$. Note that $|S| \le |E| \le |S|^2$, as $M$ is stochastic.

##### Solving linear systems. {#solving-linear-systems. .unnumbered}

Let $\kappa \in [2,3]$ be such that one can multiply two $n \times n$-matrices in time $O(n^\kappa)$ (in other literature, $\kappa$ is often denoted by $\omega$). We assume that arithmetic operations cost constant time. One can choose $\kappa = 2.4$, see @gall2014 for a recent result. One can check whether an $n \times n$ matrix is invertible in time $O(n^\kappa)$ @bunc1974. Finally, one can solve a linear system with $n$ equations using the Moore-Penrose pseudo-inverse @jame1978 in time $O(n^\kappa)$ @petk2009.

##### Spectral theory. {#spectral-theory. .unnumbered}

The *spectral radius* of a matrix $M \in \Real^{S \times S}$, denoted $\rho(M)$, is the largest absolute value of the eigenvalues of $M$. By the Perron-Frobenius theorem @book:bermanP94 [Theorems 2.1.1, 2.1.4], if $M$ is nonnegative then the spectral radius $\rho(M)$ is an eigenvalue of $M$ and there is a nonnegative eigenvector $\vec{x}$ with $M\vec{x}=\rho(M)\vec{x}$. Such a vector $\vec{x}$ is called *dominant*. Further, if $M$ is nonnegative and strongly connected then $\vec{x}$ is strictly positive in all components and the eigenspace associated with $\rho(M)$ is one-dimensional.

Algorithms {#sec:uba}
==========

Given a Markov chain $\cM$, an initial distribution $\iota$, and a Büchi automaton $\cA$ whose alphabet is the state space of $\cM$, the *probabilistic model-checking problem* is to compute $\Pr^{\cM}_\iota(\cL(\cA))$. This problem is PSPACE-complete @CY95 [@BusRubVar04], but solvable in polynomial time if $\cA$ is deterministic. For UBAs a polynomial-time algorithm was described in @16BKKKMW-CAV [@baieunp1]. In this paper we obtain a faster algorithm (recall that $E$ is the set of transitions in the Markov chain):

<span>theorem</span><span>thmPMCMCUBA</span> \[thm:PMC-MC-UBA\] Given a Markov chain $\cM = (S,M)$, an initial distribution $\iota$, and a UBA $\cA = (Q,S,\delta,Q_0,F)$, one can compute $\Pr^{\cM}_\iota(\cL(\cA))$ in time $O(|Q|^\kappa |S|^\kappa + |Q|^3|E|+|\delta|^2|E|)$.

Before we prove this theorem in Section \[sub:pseudo-cuts\], we describe the algorithm from @16BKKKMW-CAV [@baieunp1] and analyse the runtime of an efficient implementation.

The Basic Linear System {#sub:linear-system}
-----------------------

Let $\cM = (S,M)$ be a Markov chain, $\iota$ an initial distribution. Let $B \in \Real^{(Q\times S)\times(Q\times S)}$ be the following matrix: $$\label{eq:Bmat}
B_{\langle q,s\rangle,\langle q',s'\rangle} = \left\{\begin{array}{ll}
M_{s,s'} & \textrm{if $q' \in \delta(q,s)$} \\
0 & \textrm{otherwise}
\end{array}\right.$$ Define $\vec{z} \in \Real^{Q\times S}$ by $\vec{z}_{\langle q,s \rangle} = \Pr^{\cM}_s(\cL(\cA_q))$. Then $\Pr^{\cM}_\iota(\cL(\cA)) = \sum_{q\in Q_0}\sum_{s \in S} \iota(s) \vec{z}_{\langle q,s \rangle}$. Lemma 4 in @baieunp1 implies that $\vec{z} = B\vec{z}$.

Consider the UBA $\cA$ from Figure \[fig:automaton\] and the two-state Markov chain $\cM$ shown on the left of Figure \[fig:product\]. The weighted graph on the right of Figure \[fig:product\] represents the matrix $B$, obtained from $\cA$ and $\cM$ according to Equation . It is natural to think of $B$ as a product of $\cA$ and $\cM$. Notice that $B$ is not stochastic: the sum of the entries in each row (equivalently, the total outgoing transition weight of a graph node) is not always one. \[ex:product\]

\[-&gt;,&gt;=stealth',shorten &gt;=1pt,auto,node distance=2.5cm, semithick\] =\[draw=black,text=black\]

\(A) <span>$q_0$</span>; (B) \[right of=A\] <span>$q_1$</span>; (C) \[below of=A\] <span>$q_2$</span>; (D) \[below of=B\] <span>$q_3$</span>;

(-1.3,0) – (A); (A) edge \[bend left\] node <span>$a$</span> (B); (B) edge \[loop right\] node <span>$b$</span> (B); (B) edge node <span>$b$</span> (D); (B) edge \[bend left\] node <span>$a$</span> (A); (C) edge \[loop left\] node <span>$b$</span> (C); (C) edge node <span>$b$</span> (A); (C) edge \[bend left\] node <span>$a$</span> (D); (D) edge \[bend left\] node <span>$a$</span> (C);

\(X) \[below of=C\] <span>$a$</span>; (Y) \[right of=X\] <span>$b$</span>;

\(X) edge \[bend left\] node <span>$\frac{1}{2}$</span> (Y); (Y) edge \[bend left\] node <span>$\frac{1}{2}$</span> (X); (X) edge \[loop above\] node <span>$\frac{1}{2}$</span> (X); (Y) edge \[loop above\] node <span>$\frac{1}{2}$</span> (Y);

\[-&gt;,&gt;=stealth',shorten &gt;=1pt,auto,node distance=2.1cm, semithick, inner sep=1\] =\[draw=black,text=black\]

\(A) <span>$\langle q_3,b \rangle$</span>; (B) \[right of=A\] <span>$\langle q_1,b \rangle$</span>; (C) \[right of=B\] <span>$\langle q_0,a \rangle$</span>; (D) \[above of=C\] <span>$\langle q_1,a \rangle$</span>; (E) \[below of=B\] <span>$\langle q_3,a \rangle$</span>; (F) \[right of=E\] <span>$\langle q_2,b \rangle$</span>; (G) \[right of=F\] <span>$\langle q_0,b \rangle$</span>; (H) \[below of=E\] <span>$\langle q_2,a \rangle$</span>;

\(B) edge node<span>$\frac{1}{2}$</span> (A); (B) edge \[loop above\] node<span>$\frac{1}{2}$</span> (B); (B) edge node<span>$\frac{1}{2}$</span> (D); (B) edge node<span>$\frac{1}{2}$</span> (E);

\(C) edge node<span>$\frac{1}{2}$</span> (B); (C) edge \[bend left=15\] node\[inner sep=1pt\]<span>$\frac{1}{2}$</span> (D);

\(D) edge \[bend left=15,'\] node\[inner sep=1pt\]<span>$\frac{1}{2}$</span> (C); (D) edge node<span>$\frac{1}{2}$</span> (G);

\(E) edge node<span>$\frac{1}{2}$</span> (F); (E) edge \[bend left=15\] node\[inner sep=1pt\]<span>$\frac{1}{2}$</span> (H);

\(F) edge node<span>$\frac{1}{2}$</span> (C); (F) edge \[loop below\] node<span>$\frac{1}{2}$</span> (F); (F) edge node<span>$\frac{1}{2}$</span> (G); (F) edge node<span>$\frac{1}{2}$</span> (H);

\(H) edge node<span>$\frac{1}{2}$</span> (A); (H) edge \[bend left=15,'\] node\[inner sep=1pt\]<span>$\frac{1}{2}$</span> (E);

<span>background</span> (D.north -| H.west) rectangle (H.south -| D.east); (A.north -| A.west) rectangle (A.south -| A.east) (G.north -| G.west) rectangle (G.south -| G.east);

Although $\vec{z}$ is a solution the system of equations $\vec{\zeta} = B\vec{\zeta}$, this system does not uniquely identify $\vec{z}$. Indeed, any scalar multiple of $\vec{z}$ is a solution for these equations. To uniquely identify $\vec{z}$ by a system of linear equations, we need to analyse the SCCs of $B$.

All SCCs $D$ satisfy $\rho(D) \leq 1$, see @baieunp1 [Proposition 7]. An SCC $D$ of $B$ is called *recurrent* if $\rho(B_{D,D})=1$. It is called *accepting* if there is $\langle q,s \rangle \in D$ with $q \in F$.

The matrix $B$ from Figure \[fig:product\] has three SCCs, namely the two singleton sets $\{\langle q_0,b \rangle\}$ and $\{\langle q_3,b \rangle\}$, and $D = \{\langle q_0,a \rangle,\langle q_1,a \rangle,\langle q_1,b \rangle,\langle q_2,a \rangle,\langle q_2,b \rangle,\langle q_3,a \rangle\}$. Only $D$ is recurrent; indeed, $\vec{y} = (\vec{y}_{\langle q_0,a \rangle},\vec{y}_{\langle q_1,a \rangle},\vec{y}_{\langle q_1,b \rangle},\vec{y}_{\langle q_2,a \rangle},\vec{y}_{\langle q_2,b \rangle},\vec{y}_{\langle q_3,a\rangle})^\top = (2,1,3,1,3,2)^\top$ is a dominant eigenvector with $B_{D,D}\vec{y}=\vec{y}$. Since $q_0$ is accepting, $D$ is accepting recurrent.

Denote the set of accepting recurrent SCCs by $\cD_+$ and the set of non-accepting recurrent SCCs by $\cD_0$. By @baieunp1 [Lemma 8], for $D \in \cD_+$ we have $\vec{z}_d > 0$ for all $d \in D$, and for $D \in \cD_0$ we have $\vec{z}_D = \vec{0}$. Hence, for $D \in \cD_+$, there exists a *$D$-normaliser*, i.e., a vector $\vec{\mu} \in \mathbb{R}^D$ such that $\vec{\mu}^\top \vec{z}_D = 1$. This gives us a system of linear equations that identifies $\vec{z}$ uniquely @baieunp1:

\[Lemma 12 in @baieunp1\]\[lem:linear-system\] Let $\cD_+$ be the set of accepting recurrent SCCs, and $\cD_0$ the set of non-accepting recurrent SCCs. For each $D \in \cD_+$ let $\vec{\mu}(D)$ be a $D$-normaliser. Then $\vec{z}$ is the unique solution of the following linear system: $$\begin{aligned}
&&\vec{\zeta} & = B \vec{\zeta} \\
\text{for all } D \in \cD_+ :&& \quad \vec{\mu}(D)^\top \vec{\zeta}_D & = 1 \\
\text{for all } D \in \cD_0 :&& \quad \vec{\zeta}_D & = \vec{0}
\end{aligned}
\label{eq:linear-system}$$

Uniqueness follows from the fact that the system $\vec{\zeta} = B \vec{\zeta}$ describes the eigenspace of the dominant eigenvalue (here, $1$) of a nonnegative strongly connected matrix (here, $B$), and such eigenspaces are one-dimensional. This leads to the following result:

\[prop:mccomp\] Suppose $N$ is the runtime of an algorithm to calculate a normaliser for each accepting recurrent SCC. Then one can compute $\Pr^{\cM}_\iota(\cL(\cA))$ in time $O(|Q|^\kappa|S|^\kappa)+N$.

Lemma \[lem:linear-system\] implies correctness of the following procedure to calculate $\Pr^{\cM}_\iota(\cL(\cA))$:

1.  Set up the matrix $B$ from Equation .

2.  Compute the SCCs of $B$.

3.  For each SCC $C$, check whether $C$ is recurrent.

4.  For each accepting recurrent SCC $D$, compute its $D$-normaliser $\vec{\mu}(D)$.

5.  Compute $\vec{z}$ by solving the linear system  in Lemma \[lem:linear-system\].

6.  Compute $\Pr^{\cM}_\iota(\cL(\cA)) = \sum_{s \in S}\sum_{q \in Q_0}\iota(s)\vec{z}_{q,s}$.

One can set up $B$ in time $O(|Q|^2|S|^2)$. Using Tarjan's algorithm one can compute the SCCs of $B$ in time linear in the vertices and edges of $B$, hence in $O(|Q|^2|S|^2)$ @tarj1972. One can find those SCCs $D$ which are recurrent in time $O(|Q|^\kappa|S|^\kappa)$ by checking if $I - B_{D,D}$ is invertible. The linear system  has $O(|Q||S|)$ equations, and thus can be solved in time $O(|Q|^\kappa|S|^\kappa)$. Hence the total runtime is $O(|Q|^\kappa|S|^\kappa)+N$.

In Section \[sub:cuts\] we describe the combinatorial, *cut* based, approach from @16BKKKMW-CAV [@baieunp1] to calculating $D$-normalisers and analyse its complexity. In Section \[sub:pseudo-cuts\] we describe a novel linear-algebra based approach, which is faster in terms of the automaton.

Calculating D-Normalisers Using Cuts {#sub:cuts}
------------------------------------

For the remainder of the paper, let $D$ be an accepting recurrent SCC. A *fibre over $s \in S$* is a subset of $D$ of the form $\alpha\times\{s\}$ for some $\alpha \subseteq Q$. Given a fibre $f = \alpha\times\{s\}$ and a state $s' \in S$, if $M_{s,s'} > 0$ we define the fibre $f {\mathop{\triangleright}}s'$ as follows: $$f {\mathop{\triangleright}}s' := \{\langle q,s' \rangle \; | \; q \in \delta(\alpha,s)\}\cap D.$$ If $M_{s,s'} = 0$, then $f {\mathop{\triangleright}}s'$ is undefined, and for $w \in S^*$ we define $f {\mathop{\triangleright}}w = f$ if $w = \varepsilon$ and $f {\mathop{\triangleright}}ws' = (f {\mathop{\triangleright}}w){\mathop{\triangleright}}s'$. If $f = \{d\}$ for some $d \in D$ we may write $d {\mathop{\triangleright}}s'$ for $f {\mathop{\triangleright}}s'$.

We call a fibre $c$ a *cut* if $c = d {\mathop{\triangleright}}v$ for some $v \in S^*$ and $d \in D$, and $c {\mathop{\triangleright}}w \neq \emptyset$ for all $w \in S^*$ whenever $c {\mathop{\triangleright}}w$ is defined. Note that if $c$ is a cut then so is $c {\mathop{\triangleright}}w$ whenever it is defined. Given a cut $c \subseteq D$ we call its characteristic vector ${\pmb{\left[\vphantom{c}\right.} c \pmb{\left.\vphantom{c}\right]}} \in \{0,1\}^D$ a *cut vector*. In the example in Figure \[fig:product\], it is easy to see that $\{\langle q_1,b\rangle\} = \langle q_0,a\rangle {\mathop{\triangleright}}b$ is a cut.

\[Lemma 10 in @baieunp1\]\[lem:cutnormalises\] There exists a cut. Any cut vector $\vec{\mu}$ is a normaliser, i.e., $\vec{\mu}^\top \vec{z}_D = 1$.

Loosely speaking, $\vec{\mu}^\top \vec{z}_D \le 1$ follows from unambiguousness, and $\vec{\mu}^\top \vec{z}_D \not< 1$ follows from an ergodicity argument (intuitively, all states in the cut are almost surely visited infinitely often). The following lemma is the basis for the cut computation algorithm in @16BKKKMW-CAV [@baieunp1]:

\[Lemma 17 in @baieunp1\] \[lem:get-larger\] Let $D \subseteq Q \times S$ be a recurrent SCC. Let $d \in D$. Suppose $w \in S^*$ is such that $d {\mathop{\triangleright}}w \ni d$ is not a cut. Then there are $v \in S^*$ and $e \ne d$ with $d {\mathop{\triangleright}}v \supseteq \{d,e\}$ and $e {\mathop{\triangleright}}w \ne \emptyset$. For any such $e$, $d {\mathop{\triangleright}}w \cap e {\mathop{\triangleright}}w = \emptyset$. Hence $d {\mathop{\triangleright}}v w \supseteq \{d,e\} {\mathop{\triangleright}}w \supsetneq d {\mathop{\triangleright}}w$.

This suggests a way of generating an increasing sequence of fibres, culminating in a cut. We prove the following proposition:

<span>ourproposition</span><span>propfindcut</span>\[prop:findcut\] Let $D \subseteq Q \times S$ be a recurrent SCC. Denote by $T$ the set of edges in $B_{D,D}$. One can compute a cut in time $O(|Q|^2 |\delta| |D| + |\delta| |T|)$.

Define, for some $d = \langle q,s\rangle \in D$, its *co-reachability* set $\Co(d) \subseteq D$: it consists of those $e \in D$ such that there exists a word $w$ with $\{d,e\} \subseteq d {\mathop{\triangleright}}w$. Note that $\Co(d)$ is a fibre over $s$. In the example of Figure \[fig:product\] we have that $\Co(\langle q_0, a\rangle) = \{\langle q_0, a\rangle,\langle q_2, a\rangle\}$, with $\{\langle q_0, a\rangle, \langle q_2, a\rangle\} \in \langle q_0, a\rangle {\mathop{\triangleright}}ba$. The following lemma (proof in Appendix \[app:cuts\]) gives a bound on the time to compute $\Co(d)$:

<span>ourlemma</span><span>lemcalccod</span>\[lem:calccod\] One can compute $\Co(d)$ in time $O(|Q| |D| + |\delta| |T|)$. Moreover, one can compute in time $O(|Q|^2 |D| + |\delta| |T|)$ a list $(\CoPath(d)(e))_{e \in \Co(d)}$ such that $\CoPath(d)(e) \in S^*$ and $\{d,e\} \subseteq d {\mathop{\triangleright}}\CoPath(d)(e)$ and $|\CoPath(d)(e)| \le |Q| |D|$.

The lemma is used in the proof of Proposition \[prop:findcut\]:

\[Proof sketch of Proposition \[prop:findcut\]\] Starting from a singleton fibre $\{d\}$, where $d = \langle q,s\rangle \in D$ is chosen arbitrarily, we keep looking for words $v \in S^*$ that have the properties described in Lemma \[lem:get-larger\] to generate larger fibres $d{\mathop{\triangleright}}w$:

1.  $w := \varepsilon$ (the empty word)

2.  while $\exists\, v \in S^*$ and $\exists\, e \ne d$ such that $d {\mathop{\triangleright}}v \supseteq \{d, e\}$ and $e {\mathop{\triangleright}}w \neq \emptyset:$\

    $w := v w$

3.  return $d {\mathop{\triangleright}}w$.

By @16BKKKMW-CAV [Lemma 18] the algorithm returns a cut. In every loop iteration the fibre $d {\mathop{\triangleright}}w$ increases, so the loop terminates after at most $|Q|$ iterations. For efficiency we calculate $\Co(d)$ and $\CoPath(d)$ using Lemma \[lem:calccod\], and we use dynamic programming to maintain the set, $\Survives$, of those $e \in D$ for which $e {\mathop{\triangleright}}w \ne \emptyset$ holds. Whenever a prefix $v$ is added to $w$, we update $\Survives$ by processing $v$ backwards. This leads to the following algorithm:

1.  Calculate $\Co(d)$ and $\CoPath(d)$ using Lemma \[lem:calccod\]

2.  $w := \varepsilon;$ $\Survives := (Q \times \{s\}) \cap D$

3.  while $\exists\, e \in \Co(d) \setminus \{d\}$ such that $e \in \Survives$:\

    $v_0= s$; $v_1\ldots v_n := \CoPath(d)(e)$\

    for $i = n, n-1, \ldots, 1$:\

    $\Survives := \{\langle p,v_{i-1}\rangle \in D \mid (\delta(p, v_{i-1}) \times \{v_i\}) \cap \Survives \neq \emptyset\}$\

    $w := v_1\ldots v_nw$

4.  return $d {\mathop{\triangleright}}w$

The runtime analysis is in Appendix \[app:cuts\].

\[ex:cut\] Letting $d = \langle q_0,a \rangle$ and $e = \langle q_2,a \rangle$ we have $\Co(d) = \{d, e\}$ with $\CoPath(d)(d) = \varepsilon$ and $\CoPath(d)(e) = b a a$. Initially we have $\Survives = Q \times \{a\}$. In the first iteration the algorithm can only pick $e$. The inner loop updates $\Survives$ first to $\{q_0, q_1, q_2, q_3\} \times \{a\}$ (i.e., to itself), then to $\{q_1, q_2\} \times \{b\}$, and finally to $\{q_0,q_3\} \times \{a\}$. Now $(\Co(d) \setminus d) \cap \Survives$ is empty and the loop terminates. The algorithm returns the cut $d {\mathop{\triangleright}}baa = \{d,e\}$.

Applying Proposition \[prop:findcut\] to the general procedure (Proposition \[prop:mccomp\]) leads to the following result on the combinatorial approach:

<span>ourtheorem</span><span>thmPMCMCUBAcut</span> \[thm:PMC-MC-UBA-cut\] Given a Markov chain $\cM = (S,M)$, an initial distribution $\iota$, and a UBA $\cA = (Q,S,\delta,Q_0,F)$, one can compute $\Pr^{\cM}_\iota(\cL(\cA))$ in time $O(|Q|^\kappa |S|^\kappa + |Q|^3 |\delta| |S|+|\delta|^2 |E|)$.

Discussion {#sec-discussion}
==========

We have analysed two algorithms for computing normalisers: the cut-based one by Baier et al. @16BKKKMW-CAV [@baieunp1], and a new one, which draws from techniques by Protasov and Voynov @Protasov17 for the analysis of matrix semigroups. The first approach is purely combinatorial, and in terms of the automaton, an efficient implementation runs in time $O(|Q|^3 |\delta| + |\delta|^2) = O(|Q|^3 |\delta|)$ (Proposition \[prop:findcut\]).

The second approach combines a linear-algebra component to compute $R(s)$ with a combinatorial algorithm to compute the co-reachability set $\Co(d)$. In terms of the automaton, the linear-algebra component runs in time $O(|Q|^3)$ (Lemma \[lem:calcR\]), while the combinatorial part runs in time $O(|\delta|^2)$, leading to an overall runtime of $O(|Q|^3 + |\delta|^2)$. Note that for all $r \in [1,2]$, if $|\delta| = \Theta(|Q|^r)$ then the second approach is faster by at least a factor of $|Q|$. Although it is not the main focus of this paper, we have analysed also the model-checking problem, where a non-trivial Markov chain is part of the input. The purely combinatorial algorithm runs in time $O(|Q|^\kappa |S|^\kappa + |Q|^3 |\delta| |S|+|\delta|^2 |E|)$, and the linear-algebra based algorithm in time $O(|Q|^\kappa |S|^\kappa + |Q|^3 |E|+|\delta|^2 |E|)$. There are cases in which the latter is asymptotically worse, but not if $\kappa = 3$ (i.e., solving linear systems in a normal way such as Gaussian elimination) or if $|E|$ is $O(|S|)$. It is perhaps unsurprising that a factor of $|\delta|^2$ from the computation of $\Co(d)$ occurs in the runtime, as it also occurs when one merely verifies the unambiguousness of the automaton, by searching the product of the automaton with itself. Can the factor $|\delta|^2$ (which may be quartic in $|Q|$) be avoided?

The Number of Transitions Can Be Quadratic. {#app-A}
===========================================

\[-<span>&gt;\[scale=5\]</span>,color=black,scale=0.7,semithick,,&gt;=stealth'\] (1) at (0,0) ; (2) at (3,2) ; (3) at (3,-2) ; (4) at (6,3) ; (5) at (6,1) ; (6) at (6,-1) ; (7) at (6,-3) ; (8) at (10,3) ; (9) at (10,1) ; (10) at (10,-1) ; (11) at (10,-3) ; (12) at (13,2) ; (13) at (13,-2) ; (14) at (16,0) ;

(1)–(2) node\[midway,fill=white\] <span>$a$</span>; (1)–(3) node\[midway,fill=white\] <span>$b$</span>; (2)–(4) node\[midway,fill=white\] <span>$a$</span>; (2)–(5) node\[midway,fill=white\] <span>$b$</span>; (3)–(6) node\[midway,fill=white\] <span>$a$</span>; (3)–(7) node\[midway,fill=white\] <span>$b$</span>; (4)–(8) node\[midway,fill=white\] <span>$a,b$</span>; (4)–(9) node\[midway,fill=white\] <span>$a,b$</span>; (4)–(10) node\[midway,fill=white\] <span>$a,b$</span>; (4)–(11) node\[midway,fill=white\] <span>$a,b$</span>; (5)–(8) node\[midway,fill=white\] <span>$a,b$</span>; (5)–(9) node\[midway,fill=white\] <span>$a,b$</span>; (5)–(10) node\[midway,fill=white\] <span>$a,b$</span>; (5)–(11) node\[midway,fill=white\] <span>$a,b$</span>; (6)–(8) node\[midway,fill=white\] <span>$a,b$</span>; (6)–(9) node\[midway,fill=white\] <span>$a,b$</span>; (6)–(10) node\[midway,fill=white\] <span>$a,b$</span>; (6)–(11) node\[midway,fill=white\] <span>$a,b$</span>; (7)–(8) node\[midway,fill=white\] <span>$a,b$</span>; (7)–(9) node\[midway,fill=white\] <span>$a,b$</span>; (7)–(10) node\[midway,fill=white\] <span>$a,b$</span>; (7)–(11) node\[midway,fill=white\] <span>$a,b$</span>; (8)–(12) node\[midway,fill=white\] <span>$a,b$</span>; (9)–(12) node\[midway,fill=white\] <span>$a,b$</span>; (10)–(13) node\[midway,fill=white\] <span>$a,b$</span>; (11)–(13) node\[midway,fill=white\] <span>$a,b$</span>; (12)–(14) node\[midway,fill=white\] <span>$a,b$</span>; (13)–(14) node\[midway,fill=white\] <span>$a,b$</span>;

\(14) edge\[loop above\] node\[above\] <span>$a$</span> (4);

\(14) edge\[out=270,in=270,bend angle=180,looseness=0.8\] node\[midway,fill=white\] <span>$b$</span> (1);

The example in Figure \[fig:manyarrows\] shows a strongly connected UBA where the number of transitions is quadratic in $|Q|$ for a fixed alphabet $\Sigma = \{a,b\}$. Indeed, for any $n \geq 2$ we can create a similar strongly connected UBA with $|Q| = O(2^{n})$ states and at least $(2^n)^2$ transitions.

Such a UBA can be created as follows: take two (directed) complete binary trees $T_1$ and $T_2$ where each node except for the leaves has $2$ outgoing edges labelled by $a,b$, respectively. In $T_2$, flip the directions of all edges and label them all with both $a$ and $b$. From the former root of $T_2$, add an $a$-labelled self-loop and a $b$-labelled transition to the root of $T_1$. From each leaf of $T_1$ add transitions to each former leaf of $T_2$, all labelled by both $a$ and $b$. The resulting graph is a strongly connected UBA with a number of arrows that is quadratic in the number of states, similar to the one in Figure \[fig:manyarrows\].

Missing Proofs
==============

Proof From Section \[sec:prelim\] {#app:prelims}
---------------------------------

We prove Lemma \[lem:diamondfree\] from the main body:

Let $\cA = (Q,\Sigma,\delta,Q_0,F)$ be the given UBA. First, we remove every state $q \in Q$ that is not reachable from $Q_0$, together with all its incoming and outgoing edges (i.e., transitions with their labels). Breadth-first search starting from every $q_0 \in Q_0$ costs at most $O(|Q|^2 + |Q||\delta||\Sigma|)$ time overall, as $|\delta||\Sigma|$ is at least the number of edges in $\cA$. Now we need to remove all the diamonds in the remaining automaton.

If there exists a diamond from $q$ to $s$, then, since $q$ is reachable, we see that $\cL(\cA_s) = \emptyset$ holds by unambiguousness, so we can remove $s$ (and all its incoming and outgoing edges) from the automaton without changing the language. Consider the product automaton $\cA \times \cA$ with states $(Q \times Q) \cup \{r\}$ and alphabet $\Sigma \cup \{\$\}$ for a fresh letter $\$$. There exists a transition between $(q,q')$ and $(s,s')$ labelled by $a \in \Sigma$ if and only if there exist an $a$-transition between $q$ and $s$ and an $a$-transition between $q'$ and $s'$. There also exists an $\$$-transition between $r$ and $(q,q)$ for every $q \in Q_0$. The number of transitions in $\cA \times \cA$ is at most $|\delta|^2|\Sigma| + |Q|$, as any transition is either an $\$$-transition from $r$ to $q \in Q_0$, or it is represented by some $a \in \Sigma$ and pairs $(q,q')$ and $(s,s')$ such that there exist $a$-transitions from $q$ to $s$ and from $q'$ to $s'$.

Finally we perform a breadth-first search on $\cA \times \cA$, starting in $r$, and remove $q$ from $\cA$ every time we encounter an edge between $(s, s')$ and $(q,q)$ with $s \neq s'$. Since we had removed all unreachable states in $\cA$, this means that for any diamond from $q$ to $t$, the state $(q,q)$ is reachable from $r$, and traversing the diamond means that at some point we will encounter an edge from $(s,s')$ with $s \neq s'$ to $(t',t')$ for some state $t'$. Removing $t'$ eliminates the diamond without altering the language of $\cA$. Breadth-first search on $\cA \times \cA$ costs time $O(|\delta|^2|\Sigma|)$, concluding the proof.

Proofs From Section \[sub:cuts\] {#app:cuts}
--------------------------------

We prove Lemma \[lem:calccod\] from the main body:

Let $P = (V,A)$ denote the graph with vertices in $V = \{(p,p',s) \in Q \times Q \times S \mid (p,s), (p',s) \in D\}$ and an edge from $(p,p',s)$ to $(r,r',t)$ whenever there are edges from $\langle p,s \rangle$ to $\langle r,t \rangle$ and from $\langle p',s \rangle$ to $\langle r',t \rangle$ in $B_{D,D}$. We have $|V| \le |Q| |D|$ and $|A| \le |\delta| |T|$. Define $\pi_S : V^* \rightarrow S^*$ as the function mapping $v_0 v_1\ldots v_n$ to $s_0 s_1\ldots s_n$, where $v_i = (p_i,p'_i,s_i)$. Let $v_0 v_1 \ldots v_n$ be a path from $(q,q,s)$ to $(q,q',s)$ in $P$, $v_0 = (q,q,s)$ and $v_n = (q,q',s)$. Then $w = \pi_S(v_1\ldots v_n)$ is a sequence of states in $S$ such that $\{\langle q,s\rangle, \langle q',s\rangle\} \subseteq \langle q,s\rangle {\mathop{\triangleright}}w$. We can (breadth-first) search $P$ to calculate $\Co(d)$ in $O(|V|+|A|)=O(|Q| |D| + |\delta| |T|)$. Using the breadth-first search tree, we can save the shortest paths from $(q,q,s)$ to $(q,q',s)$ for each $e = \langle q', s\rangle \in \Co(d)$. Since $\Co(d)$ is a fibre, we have $|\Co(d)| \le |Q|$. Hence we can compute in time $O(|Q| |D| + |\delta| |T| + |Q| |V|) \le O(|Q|^2 |D| + |\delta| |T|)$ the list $\CoPath(d)$ with $|\CoPath(d)(e)| \leq |Q| |D|$.

We prove Proposition \[prop:findcut\] from the main body:

We continue from the proof sketch in the main body. Step 1 of the algorithm computes $\Co(d)$ and $\CoPath(d)$ in time $O(|Q|^2 |D| + |\delta| |T|)$ using Lemma \[lem:calccod\]. We have $|\CoPath(d)(e)| \le |Q| |D|$, so the (final) word $w$ has length at most $|Q|^2 |D|$. For each state $v_{i-1}$ in $w$ one can update the set $\Survives$ in the inner loop in time $O(|\delta|)$ by going through the automaton transitions labelled by $v_{i-1}$. Hence step 3 of the algorithm takes time $O(|Q|^2 |\delta| |D|)$. Step 4 is to calculate $d {\mathop{\triangleright}}w$ by essentially the same computation as in the inner loop, but forwards instead of backwards and with fixed $w$, hence also in time $O(|Q|^2 |\delta| |D|)$. The total runtime is $O(|Q|^2 |\delta| |D| + |\delta| |T|)$.

We prove Theorem \[thm:PMC-MC-UBA-cut\] from the main body:

There are at most $|\delta| |E|$ edges in $B$. Thus, summing the quantities $|D|$ and $|T|$ from Proposition \[prop:findcut\] over all SCCs $D$ gives at most $|Q| |S|$ and $|\delta| |E|$, respectively. Hence, by Proposition \[prop:findcut\], one can compute normalisers for all recurrent SCCs in time $O(|Q|^3 |\delta| |S| + |\delta|^2 |E|)$. Using Proposition \[prop:mccomp\] we get a total runtime of $O(|Q|^\kappa |S|^\kappa + |Q|^3 |\delta| |S|+|\delta|^2 |E|)$.

Proofs From Section \[sub:pseudo-cuts\] {#app:pseudocuts}
---------------------------------------

The following lemma is used in the proof of Lemma \[lem:calcR\]:

<span>ourlemma</span><span>lemorderedlindep</span>\[lem:orderedlindep\] Let $t \in S$ and $x \in S^*$. Let $U \subseteq S^*$ be a set of words with $u \ll_S x$ for all $u \in U$ and $\Delta'(t)\Delta(x)\vec{y} = \sum_{u \in U} \gamma_u \Delta'(t)\Delta(u)\vec{y}$ for some $\gamma_u \in \Real$, $u \in U$. Let $s \in S$ and $w \in S^*$. Then there exists a set $U'$ of words $u' \ll_S w t x$ such that $\Delta'(s)\Delta(w t x)\vec{y} = \sum_{u' \in U'} \gamma_{u'} \Delta'(s)\Delta(u')\vec{y}$ holds for some $\gamma_{u'} \in \Real$, $u' \in U'$.

We have: $$\begin{aligned}
\Delta'(s)\Delta(w t x)\vec{y}
& \ = \ \Delta'(s) \Delta(w) \Delta(t) \Delta(x)\vec{y}  \\
& \ = \ \Delta'(s) \Delta(w) \Delta(t) \Delta'(t) \Delta(x)\vec{y} \\
& \ = \ \Delta'(s) \Delta(w) \Delta(t)\Big(\sum_{u \in U} \gamma_u \Delta'(t)\Delta(u)\vec{y}\Big) \\
& \ = \ \sum_{u \in U}\gamma_u\Delta'(s)\Delta(w t u)\vec{y}\;.\end{aligned}$$ Hence choose $U' = \{w t u \mid u \in U\}$.

Now we can prove Lemma \[lem:calcR\] from the main body:

We use induction to prove that for each $s$ the span of $R(s)$ contains $V(s)$. Denote all nonempty words in $S^*$ by $v^{(1)},v^{(2)},\ldots$ such that $v^{(i)} \ll_S v^{(j)}$ if and only if $i < j$. For each $v^{(i)}$, let $s^{(i)} \in S$ and $w^{(i)} \in S^*$ be such that $v^{(i)} = s^{(i)} w^{(i)}$. For each $v^{(i)}$ such that $w^{(i)}$ is the empty word, $\Delta'(s^{(i)})\vec{y}$ is linearly dependent on $R(s^{(i)})$. Our induction hypothesis is that for each $v^{(i)}$ for $i \leq n$, we have that $\Delta'(s^{(i)})\Delta(w^{(i)})\vec{y}$ is dependent on $R(s^{(i)})$. For the inductive step, consider $v^{(n+1)}$ and distinguish two cases:

-   Either $\Delta'(s^{(n+1)})\Delta(w^{(n+1)})\vec{y}$ was visited by the algorithm:\
    Then either $\Delta'(s^{(n+1)})\Delta(w^{(n+1)})\vec{y}$ was shown to be dependent on $R(s^{(n+1)})$ at that time, or $\Delta'(s^{(n+1)})\Delta(w^{(n+1)})\vec{y}$ was independent of $R(s^{(n+1)})$ at that time, after which $\Delta'(s^{(n+1)})\Delta(w^{(n+1)})\vec{y}$ was added to $R(s^{(n+1)})$.

-   Or $\Delta'(s^{(n+1)})\Delta(w^{(n+1)})\vec{y}$ was not visited by the algorithm:\
    Then for some suffix $v^{(q)}$ of $v^{(n+1)}$ the vector $\Delta'(s^{(q)})\Delta(w^{(q)})\vec{y}$ was visited by the algorithm and was found to be dependent on $R(s^{(q)})$ at the time, which was dependent on vectors of the form $\Delta'(s^{(q)})\Delta(w^{(p)})\vec{y}$, with $w^{(p)} \ll_S w^{(q)}$. By Lemma \[lem:orderedlindep\] the vector $\Delta'(s^{(n+1)})\Delta(w^{(n+1)})\vec{y}$ is dependent on vectors of the form $\Delta'(s^{(n+1)})\Delta(w^{(m)})\vec{y}$ with $w^{(m)} \ll_S w^{(n+1)}$. Since $s^{(n+1)}w^{(m)} \ll_S v^{(n+1)}$, by the induction hypothesis all of these vectors are dependent on $R(s^{(n+1)})$. Therefore, $\Delta'(s^{(n+1)})\Delta(w^{(n+1)})\vec{y}$ is dependent on $R(s^{(n+1)})$.

Concerning runtime, for every vector $\vec{u} = \Delta'(t)\Delta(w)\vec{y}$ visited by the algorithm, $\vec{u}$ is orthogonalised against $R(t)$. This costs $O(|Q|^2)$ time, as $\vec{u}$ and every vector in $R(t)$ is a fibre over $t$. Moreover, one can calculate $\Delta'(s) \Delta(t) \vec{u}$ from $\vec{u}$ in time $O(|Q|^2)$, as $\Delta'(s) \Delta(t)$ is possibly nonzero only in a $|Q| \times |Q|$ submatrix. The algorithm adds $|E(t)|$ vectors to $\unvisited$ each time a vector gets added to $R(t)$, and the latter happens at most $|Q_{D,t}|$ times since the nonzero elements only occur in $\langle q, t\rangle$ with $\langle q, t\rangle \in D$. This gives us the bound of $O(|Q|^2 \sum_{t \in S} |Q_{D,t}||E(t)|)$.

We prove Proposition \[prop:findcodcut\] from the main body:

One can compute $\vec{y}$ in time $O(|D|^\kappa)$. By Lemma \[lem:calccod\], one can calculate $\Co(d)$ in time <span>$O(|Q||D|+|\delta||T_D|)$</span>. By Lemma \[lem:calcR\], one can compute $R(s)$ in time $O(|Q|^2 \sum_{t \in S}|Q_{D,t}| |E(t)|)$. The $O(|D|)$ equations from Lemma \[lem:nullspclpc\] can be solved in time $O(|D|^\kappa)$. The total runtime is $O(|D|^\kappa + |Q||D|+|\delta||T_D| + |Q|^2 \sum_{t \in S}|Q_{D,t}| |E(t)|)$.

We prove Theorem \[thm:PMC-MC-UBA\] from the main body:

Denote by $\mathcal{D}$ the set of accepting recurrent SCCs. Using Proposition \[prop:findcodcut\] we compute a normaliser for each of them. Since there are at most $|\delta||E|$ edges in $B$, we have $\sum_{D \in \mathcal{D}} |T_D| \le |\delta| |E|$. Hence, $\sum_{D \in \mathcal{D}} |D|^\kappa + |Q| |D| + |\delta| |T_D|$ is $O(|Q|^\kappa |S|^\kappa + \delta^2 |E|)$. For any $t \in S$ and different SCCs $D,D' \in \mathcal{D}$, the sets $Q_{D,t}$ and $Q_{D',t}$ are disjoint. Thus, $$\sum_{t \in S} \sum_{D \in \mathcal{D}} |Q_{D,t}| |E(t)| \ \le \ \sum_{t \in S} |Q| |E(t)| \ = \ |Q| |E|\,.$$ Hence by Proposition \[prop:findcodcut\], one can compute normalisers for all accepting recurrent SCCs in time $O(|Q|^\kappa |S|^\kappa + |Q|^3 |E|+|\delta|^2 |E|)$. Using Proposition \[prop:mccomp\] we get a total runtime of $O(|Q|^\kappa |S|^\kappa + |Q|^3 |E|+|\delta|^2 |E|)$.

{'source': 'arXiv_out/1906'}