Efficient Analysis of Unambiguous Automata Using Matrix Semigroup Techniques

TL;DR

This paper presents a new linear-algebra-based technique for analyzing unambiguous automata, significantly improving the efficiency of model checking by reducing computational complexity from combinatorial methods.

Contribution

It introduces a novel matrix semigroup approach to analyze unambiguous automata, replacing a complex combinatorial procedure with a more efficient linear-algebraic method.

Findings

New algorithm runs in O(|Q|^4) time

Improves efficiency over existing combinatorial methods by a factor of |Q|

Applicable to quantitative analysis of unambiguous Büchi automata

Abstract

We introduce a novel technique to analyse unambiguous B\"uchi 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|$.

Equations

$${\vec{z}}_{q_0}$$

$${\vec{z}}_{q_2}$$

$${\vec{z}}_{q_0}$$

$${\vec{z}}_{q_2}$$

$$B_{\langle q,s\rangle,\langle q^{\prime},s^{\prime}\rangle}=\left\{\begin{array}[]{ll}M_{s,s^{\prime}}&\textrm{if $q^{\prime}\in\delta(q,s)$}\\ 0&\textrm{otherwise}\end{array}\right.$$

$$\vec{\zeta }$$

$$\text{for all }D\in {\mathcal{D}}_{+}:$$

$$\text{for all }D\in {\mathcal{D}}_0:$$

$$f▹s^{\prime }:=\{⟨q,s^{\prime }⟩|q\in \delta (\alpha ,s)\}\cap D.$$

$$\Delta(t)_{\langle q,s\rangle,\langle q^{\prime},s^{\prime}\rangle}:=\left\{\begin{array}[]{ll}1&\quad\textrm{if $s^{\prime}=t$, $M_{s,t}>0$, and $q^{\prime}\in\delta(q,s)$}\\ 0&\quad\textrm{otherwise}\end{array}\right.$$

$$[d{]}^{\top }\Delta (w)\vec{z}=[d{]}^{\top }\Delta (w{w}^{\prime }w)\vec{z}\ge [d{]}^{\top }\Delta (w)\vec{z}+[d^{\prime }{]}^{\top }\Delta (w)\vec{z},$$

$${\vec{\mu }}^{\top }\Delta (w)\vec{z}=\sum _{d^{\prime }\in Co(d)}{\vec{\mu }}_{d^{\prime }}[d^{\prime }{]}^{\top }\Delta (w)\vec{z}={\vec{\mu }}_d[d{]}^{\top }\Delta (w)\vec{z}.$$

$$[c{]}^{\top }\vec{y}$$

$$=[c{]}^{\top }{\Delta }^{\prime }(s)\Delta (w)\vec{y}$$

$$=[c{]}^{\top }\sum _{\vec{r}\in R(s)}{\gamma }_{\vec{r}}\vec{r}$$

$$=[c{]}^{\top }\vec{y}\sum _{\vec{r}\in R(s)}{\gamma }_{\vec{r}}$$

$${\vec{\mu }}^{\top }\Delta (w)\vec{y}={\vec{\mu }}^{\top }{\Delta }^{\prime }(s)\Delta (w)\vec{y}=\sum _{\vec{r}\in R(s)}{\gamma }_{\vec{r}}{\vec{\mu }}^{\top }\vec{r}=\sum _{\vec{r}\in R(s)}{\gamma }_{\vec{r}}{\vec{\mu }}^{\top }\vec{y}={\vec{\mu }}^{\top }\vec{y},$$

$${\Delta }^{\prime }(s)\Delta (wtx)\vec{y}$$

$$={\Delta }^{\prime }(s)\Delta (w)\Delta (t){\Delta }^{\prime }(t)\Delta (x)\vec{y}$$

$$\displaystyle\ =\ \Delta^{\prime}(s)\Delta(w)\Delta(t)\Big{(}\sum_{u\in U}\gamma_{u}\Delta^{\prime}(t)\Delta(u)\vec{y}\Big{)}$$

$$=\sum _{u\in U}{\gamma }_u{\Delta }^{\prime }(s)\Delta (wtu)\vec{y}.$$

$$\sum _{t\in S}\sum _{D\in \mathcal{D}}|Q_{D,t}||E(t)|\le \sum _{t\in S}|Q||E(t)|=|Q||E|.$$

Full text

1 Introduction

Given a finite automaton $\mathcal{A}$, what is the proportion of words accepted by it? This question is natural but imprecise: there are infinitely many words and the proportion of accepted words may depend on the word length. One may consider the sequence $d_{0},d_{1},\ldots$ where $d_{i}$ is the proportion of length-$i$ words accepted by $\mathcal{A}$, i.e., $d_{i}=\frac{|L(\mathcal{A})\cap\Sigma^{i}|}{|\Sigma|^{i}}$. The sequence does not necessarily converge, but one may study, e.g., possible limits and accumulation points [5].

Alternatively, one can specify a probability distribution on words, e.g., with a Markov chain, and ask for the probability that a word is accepted by $\mathcal{A}$. For instance, if $\Sigma=\{a,b\}$, one may generate a random word, letter by letter, by outputting $a$, $b$ with probability $1/3$ each, and ending the word with probability $1/3$. For an NFA $\mathcal{A}$, determining whether the probability of generating an accepted word is $1$ is equivalent to universality (is $L(\mathcal{A})=\Sigma^{*}$?), a PSPACE-complete problem. However, if $\mathcal{A}$ is unambiguous, i.e., every accepted word has exactly one accepting path, then one can compute the probability of generating an accepted word in polynomial time by solving a linear system of equations. Unambiguousness allows us to express the probability of a union as the sum of probabilities:

Example 1.1**.**

Consider the unambiguous automaton $\mathcal{A}$ in Figure 1 (left). If we generate a random word over $\{a,b\}$ according to the process described above, we have the following linear system for the vector $\vec{z}$ where $\vec{z}_{q}$ is, for each $q\in\{q_{0},q_{1},q_{2},q_{3}\}$, the probability that the word is accepted when $q$ is taken as initial state:

[TABLE]

The constant term in the equation for $\vec{z}_{q_{0}}$ reflects the fact that $q_{0}$ is accepting. The (other) coefficients $\frac{1}{3}$ correspond to the production of either $a$ or $b$. The linear system has a unique solution.

One may view an NFA $\mathcal{A}$ as a Büchi automaton, so that its language $L(\mathcal{A})\subseteq\Sigma^{\omega}$ is the set of those infinite words that have an accepting run in $\mathcal{A}$, i.e., a run that visits accepting states infinitely often. There is a natural notion of an infinite random word over $\Sigma$: in each step sample a letter from $\Sigma$ uniformly at random, e.g., if $\Sigma=\{a,b\}$ then choose $a$ and $b$ with probability $1/2$ each. Perhaps more significantly, model checking Markov chains against Büchi automata, i.e., computing the probability that the random word generated by the Markov chain is accepted by the automaton, is a key problem in the verification of probabilistic systems. Unfortunately, like the aforementioned problem on finite words, it is also PSPACE-complete [8]. However, if the Büchi automaton is unambiguous, i.e., every accepted (infinite) word has exactly one accepting path, then one can compute the probability of generating an accepted word in polynomial time [2], both in the given Büchi automaton and in a given (discrete-time, finite-state) Markov chain. Since LTL specifications can be converted to unambiguous Büchi automata with a single-exponential blow-up, this leads to an LTL model-checking algorithm with single-exponential runtime, which is optimal. The polynomial-time algorithm from [2] for unambiguous Büchi automata is more involved than in the finite-word case.

Example 1.2**.**

In the following we view the automaton $\mathcal{A}$ from Figure 1 as an (unambiguous) Büchi automaton. If we generate a random word over $\{a,b\}$ according to the process described above, then the vector $\vec{z}$ where for each $q\in\{q_{0},q_{1},q_{2},q_{3}\}$, $\vec{z}_{q}$ is the probability that the word is accepted when $q$ is taken as initial state, is a solution to the following linear system:

[TABLE]

However, this linear system has multiple solutions: indeed, any scalar multiple $(1,2,2,1)^{\top}$ is a solution.

In order to make such a linear system uniquely solvable, one needs to add further equations, and finding these further equations is where the real challenge lies. Assuming that the state space $Q$ of $\mathcal{A}$ is strongly connected and the Markov chain generates letters uniformly at random as described above, a single additional equation $\vec{\mu}^{\top}\vec{z}=1$ suffices (this can be shown with Perron-Frobenius theory: the eigenspace for the dominant eigenvalue of a nonnegative irreducible matrix is one-dimensional). We call such a vector $\vec{\mu}\in\mathbb{R}^{Q}$ a normaliser. The aim of this paper is to use a novel, linear-algebra based technique to compute normalisers more efficiently.

The suggestion in [2] was to take as normaliser the characteristic vector $\boldsymbol{\left[\vphantom{c}\right.}c\boldsymbol{\left.\vphantom{c}\right]}\in\{0,1\}^{Q}$ of a so-called cut $c\subseteq Q$. To define this, let us write $\delta(q,w)$ for the set of states reachable from a state $q\in Q$ via the word $w\in\Sigma^{*}$. A cut is a set of states of the form $c=\delta(q,w)$ such that $\delta(q,wx)\neq\emptyset$ holds for all $x\in\Sigma^{*}$. If a cut does not exist or if $\mathcal{A}$ does not have accepting states, then we have $\vec{z}=\vec{0}$.

Example 1.3**.**

In the automaton $\mathcal{A}$ from Figure 1, we have a cut $c=\delta(q_{0},aba)=\{q_{0},q_{2}\}$. Hence its characteristic vector $\vec{\mu}=(1,0,1,0)^{\top}$ is a normaliser, allowing us to add the equation $\vec{\mu}^{\top}\vec{z}=\vec{z}_{q_{0}}+\vec{z}_{q_{2}}=1$. Now the system is uniquely solvable: $\vec{z}=\frac{1}{3}(1,2,2,1)^{\top}$. The equation $\vec{z}_{q_{0}}+\vec{z}_{q_{2}}=1$ is valid by an ergodicity argument: intuitively, given a finite word that leads to $q_{0}$ and $q_{2}$, a random infinite continuation will almost surely enable an accepting run. For instance, $\vec{z}_{q_{0}}=\frac{1}{3}$ is the probability that a random infinite word over $\{a,b\}$ has an odd number of $a$s before the first $b$. (This holds despite the fact that the word $abbb\ldots$ is not accepted from $q_{0}$.)

In Proposition 3.8 we show that an efficient implementation of the algorithm from [2] for computing a cut runs in time $O(|Q|^{5})$. Our goal is to find a normaliser $\vec{\mu}$ more efficiently.

The general idea is to move from a combinatorial problem, namely computing a set $c\subseteq Q$, to a continuous problem, namely computing a vector $\vec{\mu}\in\mathbb{R}^{Q}$. To illustrate this, note that since we can choose as $\vec{\mu}$ the characteristic vector of an arbitrary cut, we may also choose a convex combination of such vectors, leading to a normaliser $\vec{\mu}$ with entries other than [math] or $1$.

The technical key ideas of this paper draw on the observation that for unambiguous automata with cuts, the transition matrices generate a semigroup of matrices whose spectral radii are all $1$. (The spectral radius of a matrix is the largest absolute value of its eigenvalues.) This observation enables us to adopt techniques that have recently been devised by Protasov and Voynov [15] for the analysis of matrix semigroups with constant spectral radius. To the best of the authors’ knowledge, such semigroups have not previously been connected to unambiguous automata. This transfer is the main contribution of this paper.

To sketch the gist of this technique, for any $a\in\Sigma$ write $M(a)\in\{0,1\}^{Q\times Q}$ for the transition matrix of the unambiguous automaton $\mathcal{A}$, define the average matrix $\overline{M}=\frac{1}{|\Sigma|}\sum_{a\in\Sigma}M(a)$, and let $\vec{y}=\overline{M}\vec{y}\in\mathbb{R}^{Q}$ be an eigenvector with eigenvalue $1$ (the matrix $\overline{M}$ has such an eigenvector if $\mathcal{A}$ has a cut). Since the matrix semigroup, $\mathcal{S}\subseteq\{0,1\}^{Q\times Q}$, generated by the transition matrices $M(a)$ has constant spectral radius, it follows from [15] that one can efficiently compute an affine space $\mathcal{F}\subseteq\mathbb{R}^{Q}$ with $\vec{y}\in\mathcal{F}$ and $\vec{0}\not\in\mathcal{F}$ such that for any $\vec{v}\in\mathcal{F}$ and any $M\in\mathcal{S}$ we have $M\vec{v}\in\mathcal{F}$. Using the fact that $\delta(q,wx)$ is a cut (for all $x\in\Sigma^{*}$) whenever $\delta(q,w)$ is a cut, one can show that all characteristic vectors of cuts have the same scalar product with all $\vec{v}\in\mathcal{F}$, i.e., all characteristic vectors of cuts are in the vector space orthogonal to $\mathcal{F}$. Indeed, we choose as normaliser $\vec{\mu}$ a vector that is orthogonal to $\mathcal{F}$. This linear-algebra computation can be carried out in time $O(|Q|^{3})$. In the visualisation on the right of Figure 1, the characteristic vectors of cuts lie in the plane shaded in red, which is orthogonal to straight line $\mathcal{F}$ (blue).

Example 1.4**.**

In the automaton $\mathcal{A}$ from Figure 1, the vector $\vec{y}=(1,2,2,1)^{\top}$ satisfies $\overline{M}\vec{y}=\vec{y}$ where $\overline{M}=\frac{1}{2}(M(a)+M(b))$. The affine space $\mathcal{F}:=\{\vec{y}+s(1,-1,-1,1)^{\top}\mid s\in\mathbb{R}\}$ has the mentioned closure properties, i.e., $M(a)\mathcal{F}\subseteq\mathcal{F}$ and $M(b)\mathcal{F}\subseteq\mathcal{F}$. Note that the vector $\vec{\mu}$ from Example 1.3 is indeed orthogonal to $\mathcal{F}$, i.e., $\vec{\mu}^{\top}(1,-1,-1,1)^{\top}=0$.

However, to ensure that $\vec{\mu}$ is a valid normaliser, we need to restrict it further. To this end, we compute, for some state $q\in Q$, the set $\mathit{Co}(q)\subseteq Q$ of co-reachable states, i.e., states $r\in Q$ such that $\delta(q,w)\supseteq\{q,r\}$ holds for some $w\in\Sigma^{*}$. This requires a combinatorial algorithm, which is similar to a straightforward algorithm that would verify the unambiguousness of $\mathcal{A}$. Its runtime is quadratic in the number of transitions of $\mathcal{A}$, i.e., $O(|Q|^{4})$ in the worst case. Then we restrict $\vec{\mu}$ such that $\vec{\mu}_{q}=1$ and $\mu$ is non-zero only in entries that correspond to $\mathit{Co}(q)$. In the visualisation on the right of Figure 1, restricting some components of $\vec{\mu}$ to be [math] corresponds to the vectors in the shaded (red) plane that lie on the plane described by $q^{\prime}=0$ for all $q^{\prime}\in Q\setminus Co(q)$.

Example 1.5**.**

We have $\mathit{Co}(q_{0})=\{q_{0},q_{2}\}$. So we restrict $\vec{\mu}$ to be of the form $(1,0,x,0)^{\top}$. Together with the equation $\vec{\mu}^{\top}(1,-1,-1,1)^{\top}=0$ this implies $\vec{\mu}=(1,0,1,0)^{\top}$. The point is that, although this is the same vector computed via a cut in Example 1.3, the linear-algebra based computation of $\vec{\mu}$ is more efficient.

In the rest of the paper we analyse the general case of model checking a given Markov chain against a given unambiguous Büchi automaton. The efficiency gain we aim for with our technique can only be with respect to the automaton, not the Markov chain; nevertheless, we analyse in detail the runtime in terms of the numbers of states and transitions in both the automaton and the Markov chain. The main results are developed in Section 3. In Section 3.1 we describe the general approach from [2, 3]. In Section 3.2 we analyse the runtime of an efficient implementation of the algorithm from [2, 3] for computing a cut. Our main contribution lies in Section 3.3, where we develop a new approach for computing a normaliser, based on the mentioned spectral properties of the transition matrices in unambiguous automata. We close in Section 4 with a discussion. Some proofs are in the appendix.

2 Preliminaries

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

Finite automata.

A Büchi automaton is a tuple $\mathcal{A}=(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 $\mathcal{A}_{q}$ for the automaton obtained from $\mathcal{A}$ 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 $\mathcal{A}$ 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\mathbb{N}$. Run $\rho$ is called accepting if $\inf(\rho)\cap F\neq\emptyset$ where $\inf(\rho)\subseteq Q$ is the set of states that occur infinitely often in $\rho$. The language $\mathcal{L}(\mathcal{A})$ of accepted words consists of all infinite words $w\in\Sigma^{\omega}$ that have at least one accepting run. $\mathcal{A}$ 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|\leq|Q|^{2}$ is the number of transitions in $\mathcal{A}$ when allowing for multiple labels per transition. In Appendix 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|\leq|\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 B.1):{ourlemma}[]

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.

We consider vectors and square matrices indexed by a finite set $S$. We write (column) vectors $\vec{v}\in\mathbb{R}^{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 $\boldsymbol{\left[\vphantom{T}\right.}T\boldsymbol{\left.\vphantom{T}\right]}\in\{0,1\}^{S}$ for the characteristic vector of $T$, i.e., $\boldsymbol{\left[\vphantom{T}\right.}T\boldsymbol{\left.\vphantom{T}\right]}_{s}=1$ if $s\in T$ and $\boldsymbol{\left[\vphantom{T}\right.}T\boldsymbol{\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\mathbb{R}^{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\mathbb{R}^{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.

A (finite-state discrete-time) Markov chain is a pair $\mathcal{M}=(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 $\mathrm{Pr}^{\mathcal{M}}_{\iota}$ on the measurable subsets of $S^{\omega}$ in the standard way, see for instance [1, chapter 10.1, page 758]. If $\iota$ is concentrated on a single state $s$, we may write $\mathrm{Pr}^{\mathcal{M}}_{s}$ for $\mathrm{Pr}^{\mathcal{M}}_{\iota}$. We write $E$ for the set of edges in the graph of $M$. Note that $|S|\leq|E|\leq|S|^{2}$, as $M$ is stochastic.

Solving linear systems.

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 [13] for a recent result. One can check whether an $n\times n$ matrix is invertible in time $O(n^{\kappa})$ [6]. Finally, one can solve a linear system with $n$ equations using the Moore-Penrose pseudo-inverse [11] in time $O(n^{\kappa})$ [14].

Spectral theory.

The spectral radius of a matrix $M\in\mathbb{R}^{S\times S}$, denoted $\rho(M)$, is the largest absolute value of the eigenvalues of $M$. By the Perron-Frobenius theorem [4, 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.

3 Algorithms

Given a Markov chain $\mathcal{M}$, an initial distribution $\iota$, and a Büchi automaton $\mathcal{A}$ whose alphabet is the state space of $\mathcal{M}$, the probabilistic model-checking problem is to compute $\mathrm{Pr}^{\mathcal{M}}_{\iota}(\mathcal{L}(\mathcal{A}))$. This problem is PSPACE-complete [8, 7], but solvable in polynomial time if $\mathcal{A}$ is deterministic. For UBAs a polynomial-time algorithm was described in [2, 3]. In this paper we obtain a faster algorithm (recall that $E$ is the set of transitions in the Markov chain):

Theorem 3.1**.**

Given a Markov chain $\mathcal{M}=(S,M)$, an initial distribution $\iota$, and a UBA $\mathcal{A}=(Q,S,\delta,Q_{0},F)$, one can compute $\mathrm{Pr}^{\mathcal{M}}_{\iota}(\mathcal{L}(\mathcal{A}))$ in time $O(|Q|^{\kappa}|S|^{\kappa}+|Q|^{3}|E|+|\delta|^{2}|E|)$.

Before we prove this theorem in Section 3.3, we describe the algorithm from [2, 3] and analyse the runtime of an efficient implementation.

3.1 The Basic Linear System

Let $\mathcal{M}=(S,M)$ be a Markov chain, $\iota$ an initial distribution. Let $B\in\mathbb{R}^{(Q\times S)\times(Q\times S)}$ be the following matrix:

[TABLE]

Define $\vec{z}\in\mathbb{R}^{Q\times S}$ by $\vec{z}_{\langle q,s\rangle}=\mathrm{Pr}^{\mathcal{M}}_{s}(\mathcal{L}(\mathcal{A}_{q}))$. Then $\mathrm{Pr}^{\mathcal{M}}_{\iota}(\mathcal{L}(\mathcal{A}))=\sum_{q\in Q_{0}}\sum_{s\in S}\iota(s)\vec{z}_{\langle q,s\rangle}$. Lemma 4 in [3] implies that $\vec{z}=B\vec{z}$.

Example 3.2**.**

Consider the UBA $\mathcal{A}$ from Figure 1 and the two-state Markov chain $\mathcal{M}$ shown on the left of Figure 2. The weighted graph on the right of Figure 2 represents the matrix $B$, obtained from $\mathcal{A}$ and $\mathcal{M}$ according to Equation (1). It is natural to think of $B$ as a product of $\mathcal{A}$ and $\mathcal{M}$. 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.

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 [3, 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$.

Example 3.3**.**

The matrix $B$ from Figure 2 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 $\mathcal{D}_{+}$ and the set of non-accepting recurrent SCCs by $\mathcal{D}_{0}$. By [3, Lemma 8], for $D\in\mathcal{D}_{+}$ we have $\vec{z}_{d}>0$ for all $d\in D$, and for $D\in\mathcal{D}_{0}$ we have $\vec{z}_{D}=\vec{0}$. Hence, for $D\in\mathcal{D}_{+}$, 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 [3]:

Lemma 3.4** (Lemma 12 in [3]).**

Let $\mathcal{D}_{+}$ be the set of accepting recurrent SCCs, and $\mathcal{D}_{0}$ the set of non-accepting recurrent SCCs. For each $D\in\mathcal{D}_{+}$ let $\vec{\mu}(D)$ be a $D$-normaliser. Then $\vec{z}$ is the unique solution of the following linear system:

[TABLE]

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:

Proposition 3.5**.**

Suppose $N$ is the runtime of an algorithm to calculate a normaliser for each accepting recurrent SCC. Then one can compute $\mathrm{Pr}^{\mathcal{M}}_{\iota}(\mathcal{L}(\mathcal{A}))$ in time $O(|Q|^{\kappa}|S|^{\kappa})+N$.

Proof 3.6**.**

Lemma 3.4 implies correctness of the following procedure to calculate $\mathrm{Pr}^{\mathcal{M}}_{\iota}(\mathcal{L}(\mathcal{A}))$:

Set up the matrix $B$ from Equation (1). 2. 2.

Compute the SCCs of $B$. 3. 3.

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

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

Compute $\vec{z}$ by solving the linear system (2) in Lemma 3.4. 6. 6.

Compute $\mathrm{Pr}^{\mathcal{M}}_{\iota}(\mathcal{L}(\mathcal{A}))=\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})$ [16]. 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 (2) 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 3.2 we describe the combinatorial, cut based, approach from [2, 3] to calculating $D$-normalisers and analyse its complexity. In Section 3.3 we describe a novel linear-algebra based approach, which is faster in terms of the automaton.

3.2 Calculating $D$-Normalisers Using 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^{\prime}\in S$, if $M_{s,s^{\prime}}>0$ we define the fibre $f\mathop{\triangleright}s^{\prime}$ as follows:

[TABLE]

If $M_{s,s^{\prime}}=0$, then $f\mathop{\triangleright}s^{\prime}$ is undefined, and for $w\in S^{*}$ we define $f\mathop{\triangleright}w=f$ if $w=\varepsilon$ and $f\mathop{\triangleright}ws^{\prime}=(f\mathop{\triangleright}w)\mathop{\triangleright}s^{\prime}$. If $f=\{d\}$ for some $d\in D$ we may write $d\mathop{\triangleright}s^{\prime}$ for $f\mathop{\triangleright}s^{\prime}$.

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 $\boldsymbol{\left[\vphantom{c}\right.}c\boldsymbol{\left.\vphantom{c}\right]}\in\{0,1\}^{D}$ a cut vector. In the example in Figure 2, it is easy to see that $\{\langle q_{1},b\rangle\}=\langle q_{0},a\rangle\mathop{\triangleright}b$ is a cut.

Lemma 3.7** (Lemma 10 in [3]).**

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}\leq 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 [2, 3]:

Lemma 3.8** (Lemma 17 in [3]).**

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\neq d$ with $d\mathop{\triangleright}v\supseteq\{d,e\}$ and $e\mathop{\triangleright}w\neq\emptyset$. For any such $e$, $d\mathop{\triangleright}w\cap e\mathop{\triangleright}w=\emptyset$. Hence $d\mathop{\triangleright}vw\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: {ourproposition}[]

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 $\mathit{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 $\mathit{Co}(d)$ is a fibre over $s$. In the example of Figure 2 we have that $\mathit{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 B.2) gives a bound on the time to compute $\mathit{Co}(d)$: {ourlemma}[]

One can compute $\mathit{Co}(d)$ in time $O(|Q||D|+|\delta||T|)$. Moreover, one can compute in time $O(|Q|^{2}|D|+|\delta||T|)$ a list $(\mathit{CoPath}(d)(e))_{e\in\mathit{Co}(d)}$ such that $\mathit{CoPath}(d)(e)\in S^{*}$ and $\{d,e\}\subseteq d\mathop{\triangleright}\mathit{CoPath}(d)(e)$ and $|\mathit{CoPath}(d)(e)|\leq|Q||D|$.

The lemma is used in the proof of Proposition 3.8:

Proof 3.9** (Proof sketch of Proposition 3.8).**

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 3.8 to generate larger fibres $d\mathop{\triangleright}w$:

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

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

*     $w:=vw$* 3. 3.

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

By [2, 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 $\mathit{Co}(d)$ and $\mathit{CoPath}(d)$ using Lemma 3.8, and we use dynamic programming to maintain the set, $\mathit{Survives}$, of those $e\in D$ for which $e\mathop{\triangleright}w\neq\emptyset$ holds. Whenever a prefix $v$ is added to $w$, we update $\mathit{Survives}$ by processing $v$ backwards. This leads to the following algorithm:

Calculate $\mathit{Co}(d)$ and $\mathit{CoPath}(d)$ using Lemma 3.8 2. 2.

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

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

*     $v_{0}=s$; $v_{1}\ldots v_{n}:=\mathit{CoPath}(d)(e)$ *

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

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

*     $w:=v_{1}\ldots v_{n}w$* 4. 4.

return $d\mathop{\triangleright}w$

The runtime analysis is in Appendix B.2.

Example 3.10**.**

Letting $d=\langle q_{0},a\rangle$ and $e=\langle q_{2},a\rangle$ we have $\mathit{Co}(d)=\{d,e\}$ with $\mathit{CoPath}(d)(d)=\varepsilon$ and $\mathit{CoPath}(d)(e)=baa$. Initially we have $\mathit{Survives}=Q\times\{a\}$. In the first iteration the algorithm can only pick $e$. The inner loop updates $\mathit{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 $(\mathit{Co}(d)\setminus d)\cap\mathit{Survives}$ is empty and the loop terminates. The algorithm returns the cut $d\mathop{\triangleright}baa=\{d,e\}$.

Applying Proposition 3.8 to the general procedure (Proposition 3.5) leads to the following result on the combinatorial approach: {ourtheorem}[]

Given a Markov chain $\mathcal{M}=(S,M)$, an initial distribution $\iota$, and a UBA $\mathcal{A}=(Q,S,\delta,Q_{0},F)$, one can compute $\mathrm{Pr}^{\mathcal{M}}_{\iota}(\mathcal{L}(\mathcal{A}))$ in time $O(|Q|^{\kappa}|S|^{\kappa}+|Q|^{3}|\delta||S|+|\delta|^{2}|E|)$.

3.3 Calculating $D$-Normalisers Using Linear Algebra

Recall that $D$ is an accepting recurrent SCC. For $t\in S$ define the matrix $\Delta(t)\in\{0,1\}^{D\times D}$ as follows:

[TABLE]

Note that the graph of $\Delta(t)$ contains exactly the edges of the graph of $B_{D,D}$ that end in vertices in $Q\times\{t\}$. If $M_{s,t}>0$ holds for all pairs $(s,t)$, then the matrices $(\Delta(t))_{t\in S}$ generate a semigroup of matrices, all of which have spectral radius $1$. Such semigroups were recently studied by Protasov and Voynov [15]. Specifically, Theorem 5 in [15] shows that there exists an affine subspace $\mathcal{F}$ of $\mathbb{R}^{D}$ which excludes $\vec{0}$ and is invariant under multiplication by matrices from the semigroup. Moreover, they provide a way to compute this affine subspace efficiently. One can show that cut vectors are orthogonal to $\mathcal{F}$. The key idea of our contribution is to generalise cut vectors to pseudo-cuts, which are vectors $\vec{\mu}\in\mathbb{R}^{D}$ that are orthogonal to $\mathcal{F}$. We will show (in Lemma 3.13 below) how to derive a $D$-normaliser based on a pseudo-cut that is non-zero only in components that are in a co-reachability set $\mathit{Co}(d)$ (from Lemma 3.8).

If $M_{s,t}=0$ holds for some $s,t$ (which will often be the case in model checking), then $\Delta(s)\Delta(t)$ is the zero matrix, which has spectral radius [math], not $1$. Therefore, the results of [15] are not directly applicable and we have to move away from matrix semigroups. In the following we re-develop and generalise parts of the theory of [15] so that the paper is self-contained and products of $\Delta(s)\Delta(t)$ with $M_{s,t}=0$ are not considered.

Let $w=s_{1}s_{2}\ldots s_{n}\in S^{*}$. Define $\Delta(w)=\Delta(s_{1})\Delta(s_{2})\cdots\Delta(s_{n})$. We say $w$ is enabled if $M_{s_{i},s_{i+1}}>0$ holds for all $i\in\{1,\ldots,n-1\}$. If $f\subseteq D$ is a fibre over $s$ such that $sw$ is enabled, we have $\boldsymbol{\left[\vphantom{f\mathop{\triangleright}w}\right.}f\mathop{\triangleright}w\boldsymbol{\left.\vphantom{f\mathop{\triangleright}w}\right]}^{\top}=\boldsymbol{\left[\vphantom{f}\right.}f\boldsymbol{\left.\vphantom{f}\right]}^{\top}\Delta(w)$. We overload the term fibre over $s$ to describe any vector $\vec{\mu}\in\mathbb{R}^{D}$ such that $\vec{\mu}_{\langle q,s^{\prime}\rangle}=0$ whenever $s^{\prime}\neq s$. We define pseudo-cuts over $s$ to be fibres $\vec{\mu}$ over $s$ such that $\vec{\mu}^{\top}\Delta(w)\vec{z}=\vec{\mu}^{\top}\vec{z}$ holds for all $w\in S^{*}$ such that $sw$ is enabled. Let $c\subseteq Q\times\{s\}$ be a cut with $sw$ enabled. Then $c\mathop{\triangleright}w$ is a cut, and $\boldsymbol{\left[\vphantom{c}\right.}c\boldsymbol{\left.\vphantom{c}\right]}^{\top}\Delta(w)\vec{z}=1=\boldsymbol{\left[\vphantom{c}\right.}c\boldsymbol{\left.\vphantom{c}\right]}^{\top}\vec{z}$ holds by Lemma 3.7. It follows that cut vectors are pseudo-cuts.

Example 3.11**.**

Since $c=\{\langle q_{0},a\rangle,\langle q_{2},a\rangle\}$ from Example 3.10 is a cut, $\boldsymbol{\left[\vphantom{c}\right.}c\boldsymbol{\left.\vphantom{c}\right]}$ is a pseudo-cut over $a$. Pseudo-cuts do not need to be combinations of cut vectors: although the fibre $f=\{\langle q_{0},a\rangle,\langle q_{1},a\rangle\}$ is not a cut, $\boldsymbol{\left[\vphantom{f}\right.}f\boldsymbol{\left.\vphantom{f}\right]}$ is a pseudo-cut over $a$.

Fix some $d=\langle q,s\rangle\in D$. Recall that $\mathit{Co}(d)$ consists of those $e\in D$ such that there exists a word $w$ with $\{d,e\}\subseteq d\mathop{\triangleright}w$. We define $\mathit{Co}(d)$-pseudo-cuts to be pseudo-cuts $\vec{\mu}$ over $s$ such that $\vec{\mu}_{d}\neq 0$ and $\vec{\mu}_{e}=0$ holds for all $e\not\in\mathit{Co}(d)$.

Example 3.12**.**

Any cut vector is a $\mathit{Co}(d)$-pseudo-cut for some $d\in D$, by definition, and so are scalar multiples of cut vectors. The vector $\boldsymbol{\left[\vphantom{f}\right.}f\boldsymbol{\left.\vphantom{f}\right]}$ in Example 3.11, however, is not a $\mathit{Co}(d)$-pseudo-cut, since $\langle q_{1},a\rangle\not\in\mathit{Co}(\langle q_{0},a\rangle)$ and $\langle q_{0},a\rangle\not\in\mathit{Co}(\langle q_{1},a\rangle)$.

From a $\mathit{Co}(d)$-pseudo-cut we can easily derive a $D$-normaliser:

Lemma 3.13**.**

Let $\vec{\mu}\in\mathbb{R}^{D}$ be a $\mathit{Co}(d)$-pseudo-cut. Then $\frac{1}{\vec{\mu}_{d}}\vec{\mu}$ is a $D$-normaliser.

Proof 3.14**.**

Let $w$ be an enabled word in $M$ such that $d\mathop{\triangleright}w$ is a cut containing $d$. Such a word exists (see the proof sketch of Proposition 3.8). Since $(\boldsymbol{\left[\vphantom{d}\right.}d\boldsymbol{\left.\vphantom{d}\right]}^{\top}\Delta(w))^{\top}=\boldsymbol{\left[\vphantom{d\mathop{\triangleright}w}\right.}d\mathop{\triangleright}w\boldsymbol{\left.\vphantom{d\mathop{\triangleright}w}\right]}$ is a $D$-normaliser (by Lemma 3.7), it suffices to prove that $\frac{1}{\vec{\mu}_{d}}\vec{\mu}^{\top}\vec{z}=\boldsymbol{\left[\vphantom{d}\right.}d\boldsymbol{\left.\vphantom{d}\right]}^{\top}\Delta(w)\vec{z}$.

We can write $\vec{\mu}$ as $\sum_{d^{\prime}\in\mathit{Co}(d)}\vec{\mu}_{d^{\prime}}\boldsymbol{\left[\vphantom{d^{\prime}}\right.}d^{\prime}\boldsymbol{\left.\vphantom{d^{\prime}}\right]}$, so $\vec{\mu}^{\top}\Delta(w)=\sum_{d^{\prime}\in\mathit{Co}(d)}\vec{\mu}_{d^{\prime}}\boldsymbol{\left[\vphantom{d^{\prime}}\right.}d^{\prime}\boldsymbol{\left.\vphantom{d^{\prime}}\right]}^{\top}\Delta(w)$. For any $d^{\prime}\in\mathit{Co}(d)\setminus\{d\}$, let $w^{\prime}$ be such that $\{d,d^{\prime}\}\subseteq d\mathop{\triangleright}w^{\prime}$. Now we see that $d^{\prime}\in d\mathop{\triangleright}ww^{\prime}$, and since $d\mathop{\triangleright}w$ is a cut so are $d\mathop{\triangleright}ww^{\prime}$ and $d\mathop{\triangleright}ww^{\prime}w$. Thus,

[TABLE]

which implies $\boldsymbol{\left[\vphantom{d^{\prime}}\right.}d^{\prime}\boldsymbol{\left.\vphantom{d^{\prime}}\right]}^{\top}\Delta(w)\vec{z}=0$ for every $d^{\prime}\in\mathit{Co}(d)\setminus\{d\}$. This means that

[TABLE]

Since $\vec{\mu}$ is a pseudo-cut, this implies that $\frac{1}{\vec{\mu}_{d}}\vec{\mu}^{\top}\vec{z}=\frac{1}{\vec{\mu}_{d}}\vec{\mu}^{\top}\Delta(w)\vec{z}=\boldsymbol{\left[\vphantom{d}\right.}d\boldsymbol{\left.\vphantom{d}\right]}^{\top}\Delta(w)\vec{z}$.

By Lemma 3.13, to find a $D$-normaliser it suffices to find a $\mathit{Co}(d)$-pseudo-cut. Fix a dominant eigenvector $\vec{y}$ of $B_{D,D}$ so that $\vec{y}$ is strictly positive in all components. One can compute such $\vec{y}$ in time $O(|D|^{\kappa})$. By [2, Lemma 8] the vector $\vec{z}_{D}$ is also a dominant eigenvector of $B_{D,D}$, hence $\vec{y}$ and $\vec{z}_{D}$ (the latter of which is yet unknown) are scalar multiples. In order to compute a $\mathit{Co}(d)$-pseudo-cut, we compute a basis for the space spanned by $\Delta(w)\vec{y}$ for all enabled words $w$. We use a technique similar to the one employed by Tzeng in [17] for checking equivalence of probabilistic automata. To make this more efficient, we compute separate basis vectors for each $s\in S$. Define $\Delta^{\prime}(t)\in\{0,1\}^{D\times D}$ as $\Delta^{\prime}(t)_{\langle q_{1},s_{1}\rangle,\langle q_{2},s_{2}\rangle}=1$ if $q_{1}=q_{2}$ and $s_{1}=s_{2}=t$ and 0 otherwise. Note that $\Delta(s)\Delta^{\prime}(s)=\Delta(s)$ holds for all $s\in S$.

{ourlemma}

[]

Suppose $\vec{y}=B_{D,D}\vec{y}$ is given. Denote by $V(s)\subseteq\mathbb{R}^{D}$ the vector space spanned by the vectors $\Delta^{\prime}(s)\Delta(w)\vec{y}$ for $w\in S^{*}$ and $s\in S$. Let $Q_{D,t}=(Q\times\{t\})\cap D$ and let $E(t)=\{(s,t)\mid M_{s,t}>0\}$ be the set of edges in $M$ that end in $t$. One can compute a basis $R(s)$ of $V(s)$ for all $s\in S$ in time $O(|Q|^{2}\sum_{t\in S}|Q_{D,t}||E(t)|)$, where for each $\vec{r}\in R(s)$ we have $\vec{r}=\Delta^{\prime}(s)\Delta(w)\vec{y}$ for some enabled word $sw$.

Proof 3.15** (Proof sketch).**

Fix an arbitrary total order $<_{S}$ on $S$. We define a total order $\ll_{S}$ on $S^{*}$ as the “shortlex” order but with words read from right to left. That is, the empty word $\varepsilon$ is the smallest element, and for $v,w\in S^{*}$ and $s,t\in S$, we have $vs\ll_{S}wt$ if (1) $|vs|<|wt|$ or (2) $|vs|=|wt|$ and $s<_{S}t$ or (3) $|vs|=|wt|$ and $s=t$ and $v\ll_{S}w$.

We use a technique similar to the one by Tzeng in [17]. At every step in the algorithm, $\mathit{worklist}$ is a set of pairs $(sw,\Delta^{\prime}(s)\Delta(w)\vec{y})$. We write $\min_{\ll_{S}}(\mathit{worklist})$ to denote the pair in $\mathit{worklist}$ where $sw$ is minimal with respect to $\mathord{\ll_{S}}$.

for each $s\in S$, let $R(s):=\{\Delta^{\prime}(s)\vec{y}\}$ and $R(s)_{\bot}:=\{\Delta^{\prime}(s)\vec{y}\}$ 2. 2.

$\mathit{worklist}:=\{(st,\Delta^{\prime}(s)\Delta(t)\vec{y})\mid M_{s,t}>0\}$** 3. 3.

*while $\mathit{worklist}\neq\emptyset$: *

*     $(tw,\vec{u}):=\min_{\ll_{S}}(\mathit{worklist})$; $\mathit{worklist}:=\mathit{worklist}\setminus\{(tw,\vec{u})\}$ *

*     Using the Gram-Schmidt process111For good numerical stability, one should use the so-called Modified Gram-Schmidt process [10, Chapter 19]., let $\vec{u}_{\bot}$ be the orthogonalisation of $\vec{u}$ against $R_{\bot}(t)$ *

*     if $\vec{u}_{\bot}\neq\vec{0}$, i.e., if $\vec{u}$ is linearly independent of $R_{\bot}(t)$: *

*          $R(t):=R(t)\cup\{\vec{u}\}$ and $R_{\bot}(t):=R_{\bot}(t)\cup\{\vec{u}_{\bot}\}$ *

*          $\mathit{worklist}:=\mathit{worklist}\cup\{(stw,\Delta^{\prime}(s)\Delta(t)\vec{u})\mid M_{s,t}>0\}$* 4. 4.

return $R(s)$ for all $s\in S$

At any point and for all $s\in S$, the sets $R(s)$ and $R(s)_{\bot}$ span the same vector space, and this space is a subspace of $V(s)$. The sets $R(s)$ and $R(s)_{\bot}$ consist of linearly independent fibres over $s$, and these fibres are possibly nonzero only in the $Q_{D,s}$-components. Hence $|\bigcup_{s\in S}R(s)|\leq|D|$ and thus there are at most $|D|$ iterations of the while loop that increase $\mathit{worklist}$. At every iteration where $\vec{u}$ is dependent on $R(t)_{\bot}$ the set $\mathit{worklist}$ decreases by one, and therefore the algorithm terminates. In Appendix B.3 we prove that in the end we have that $R(s)$ spans $V(s)$, and we analyse the runtime.

Example 3.16**.**

Let us return to our running example. We see that the vector $\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 of $B_{D,D}$. Fix the order $a<_{S}b$. Step 1 initialises $R(a)$ to $\{\Delta^{\prime}(a)\vec{y}\}$ and $R(b)$ to $\{\Delta^{\prime}(b)\vec{y}\}$, where $\Delta^{\prime}(a)\vec{y}=(2,1,0,1,0,2)^{\top}$ and $\Delta^{\prime}(b)\vec{y}=(0,0,3,0,3,0)^{\top}$. Step 2 computes $\Delta^{\prime}(a)\Delta(a)\vec{y}=(1,2,0,2,0,1)^{\top}$, which is linearly independent of $\Delta^{\prime}(a)\vec{y}$. However, $\Delta^{\prime}(b)\Delta(a)\vec{y}=(0,0,3,0,3,0)^{\top}=\Delta^{\prime}(b)\vec{y}$. Also, $\Delta^{\prime}(a)\Delta(b)\vec{y}=(3,0,0,0,0,3)^{\top}=2\Delta^{\prime}(a)\vec{y}-\Delta^{\prime}(a)\Delta(a)\vec{y}$ and $\Delta^{\prime}(b)\Delta(b)\vec{y}=(0,0,3,0,3,0)^{\top}=\Delta^{\prime}(b)\vec{y}$. One can check that $\Delta^{\prime}(a)\Delta(aa)\vec{y}=\Delta^{\prime}(a)\vec{y}$ and $\Delta^{\prime}(b)\Delta(aa)\vec{y}=\Delta^{\prime}(b)\vec{y}$. Hence the algorithm returns $R(a)=\{(2,1,0,1,0,2)^{\top},(1,2,0,2,0,1)^{\top}\}$ and $R(b)=\{(0,0,3,0,3,0)^{\top}\}$.

Fix $d=\langle q,s\rangle\in D$ for the rest of the paper. The following lemma characterises $\mathit{Co}(d)$-pseudo-cuts in a way that is efficiently computable:

Lemma 3.17**.**

A vector $\vec{\mu}\in\mathbb{R}^{D}$ with $\vec{\mu}_{d}=1$ and $\vec{\mu}_{e}=0$ for all $e\not\in\mathit{Co}(d)$ is a $\mathit{Co}(d)$-pseudo-cut if and only if $\vec{\mu}^{\top}\vec{r}=\vec{\mu}^{\top}\vec{y}$ holds for all $\vec{r}\in R(s)$.

For an intuition of the proof, consider the affine space, $\mathcal{F}\subseteq\mathbb{R}^{D}$, affinely spanned by those $\Delta^{\prime}(s)\Delta(w)\vec{y}$ for which $sw$ is enabled. This affine space was alluded to in the beginning of this subsection and is visualised as a blue straight line on the right of Figure 1. The shaded plane in this figure is the vector space of pseudo-cuts over $s$. This space is orthogonal to $\mathcal{F}$. The following lemma says that $\mathcal{F}$ is affinely spanned by the points in $R(s)$. This strengthens the property of $R(s)$ in Lemma 3.14 where $R(s)$ was defined to span a vector space.

Lemma 3.18**.**

Let $w\in S^{*}$ be such that $sw$ is enabled. By the definition of $R(s)$ there are $\gamma_{\vec{r}}\in\mathbb{R}^{D}$ for each $\vec{r}\in R(s)$ such that $\Delta^{\prime}(s)\Delta(w)\vec{y}=\sum_{\vec{r}\in R(s)}\gamma_{\vec{r}}\vec{r}$. We have $\sum_{\vec{r}\in R(s)}\gamma_{\vec{r}}=1$.

Proof 3.19**.**

Let $c$ be a cut containing $d$. Since $R(s)$ is a basis, for any $\vec{r}=\Delta^{\prime}(s)\Delta(w_{\vec{r}})\vec{y}\in R(s)$ the word $sw_{\vec{r}}$ is enabled. Therefore, $c\mathop{\triangleright}w_{\vec{r}}$ is a cut and by Lemma 3.7 we have $\boldsymbol{\left[\vphantom{c\mathop{\triangleright}w_{\vec{r}}}\right.}c\mathop{\triangleright}w_{\vec{r}}\boldsymbol{\left.\vphantom{c\mathop{\triangleright}w_{\vec{r}}}\right]}^{\top}\vec{y}=\boldsymbol{\left[\vphantom{c}\right.}c\boldsymbol{\left.\vphantom{c}\right]}^{\top}\vec{y}$. Hence $\boldsymbol{\left[\vphantom{c}\right.}c\boldsymbol{\left.\vphantom{c}\right]}^{\top}\vec{r}=\boldsymbol{\left[\vphantom{c}\right.}c\boldsymbol{\left.\vphantom{c}\right]}^{\top}\Delta^{\prime}(s)\Delta(w_{\vec{r}})\vec{y}=\boldsymbol{\left[\vphantom{c}\right.}c\boldsymbol{\left.\vphantom{c}\right]}^{\top}\Delta(w_{\vec{r}})\vec{y}=\boldsymbol{\left[\vphantom{c\mathop{\triangleright}w_{\vec{r}}}\right.}c\mathop{\triangleright}w_{\vec{r}}\boldsymbol{\left.\vphantom{c\mathop{\triangleright}w_{\vec{r}}}\right]}^{\top}\vec{y}=\boldsymbol{\left[\vphantom{c}\right.}c\boldsymbol{\left.\vphantom{c}\right]}^{\top}\vec{y}$. Moreover, we have:

[TABLE]

Therefore, $\sum_{\vec{r}\in R(s)}\gamma_{\vec{r}}=1$.

Now we can prove Lemma 3.17:

Proof 3.20** (Proof of Lemma 3.17).**

For the “if” direction, let $w$ be such that $sw$ is enabled, and it suffices to show that $\vec{\mu}^{\top}\Delta(w)\vec{y}=\vec{\mu}^{\top}\vec{y}$. By Lemma 3.18 there are $\gamma_{\vec{r}}$ such that $\Delta^{\prime}(s)\Delta(w)\vec{y}=\sum_{\vec{r}\in R(s)}\gamma_{\vec{r}}\vec{r}$ and $\sum_{\vec{r}\in R(s)}\gamma_{\vec{r}}=1$. We have:

[TABLE]

where the last equality is from Lemma 3.18.

*For the “only if” direction, suppose $\vec{\mu}$ is a $\mathit{Co}(d)$-pseudo-cut. Let $\vec{r}=\Delta^{\prime}(s)\Delta(w_{\vec{r}})\vec{y}\in R(s)$. Then $sw_{\vec{r}}$ is enabled and $\vec{\mu}^{\top}\vec{r}=\vec{\mu}^{\top}\Delta^{\prime}(s)\Delta(w_{\vec{r}})\vec{y}=\vec{\mu}^{\top}\Delta(w_{\vec{r}})\vec{y}=\vec{\mu}^{\top}\vec{y}$. *

Example 3.21**.**

In Example 3.10 we derived that $\vec{y}=(2,1,3,1,3,2)^{\top}$ and $R(a)=\{(2,1,0,1,0,2)^{\top},(1,2,0,2,0,1)^{\top}\}$. The cut vector $\vec{\mu}=(1,0,0,1,0,0)^{\top}$ from Example 3.11 satisfies $\vec{\mu}^{\top}\vec{r}=3=\vec{\mu}^{\top}\vec{y}$ for both $\vec{r}\in R(a)$.

Using Lemmas 3.8, 3.14 and 3.17 we obtain: {ourproposition}[]

Let $D\subseteq Q\times S$ be a recurrent SCC. Denote by $T_{D}$ the set of edges of $B_{D,D}$. For $t\in S$, let $E(t)$ denote the set of edges of $M$ that end in $t$, and let $Q_{D,t}=(Q\times\{t\})\cap D$. Let $d=\langle q,s\rangle\in D$. One can compute a $\mathit{Co}(d)$-pseudo-cut in time $O(|D|^{\kappa}+|Q||D|+|\delta||T_{D}|+|Q|^{2}\sum_{t\in S}|Q_{D,t}||E(t)|)$.

Now our main result follows, which we restate here: See 3.1

4 Discussion

We have analysed two algorithms for computing normalisers: the cut-based one by Baier et al. [2, 3], and a new one, which draws from techniques by Protasov and Voynov [15] 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 3.8).

The second approach combines a linear-algebra component to compute $R(s)$ with a combinatorial algorithm to compute the co-reachability set $\mathit{Co}(d)$. In terms of the automaton, the linear-algebra component runs in time $O(|Q|^{3})$ (Lemma 3.14), 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 $\mathit{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?

Appendix A The Number of Transitions Can Be Quadratic.

The example in Figure 3 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 3.

Appendix B Missing Proofs

B.1 Proof From Section 2

We prove Lemma 2 from the main body: See 2

Proof B.1**.**

Let $\mathcal{A}=(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 $\mathcal{A}$. 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 $\mathcal{L}(\mathcal{A}_{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 $\mathcal{A}\times\mathcal{A}$ with states $(Q\times Q)\cup\{r\}$ and alphabet \Sigma\cup\{\}$for a fresh letter$$$. There exists a transition between$(q,q^{\prime})$and$(s,s^{\prime})$labelled by$a\in\Sigma$if and only if there exist an$a$-transition between$q$and$s$and an$a$-transition between$q^{\prime}$and$s^{\prime}$. There also exists an$$$-transition between$r$and$(q,q)$for every$q\in Q_{0}$. The number of transitions in$\mathcal{A}\times\mathcal{A}$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^{\prime})$and$(s,s^{\prime})$such that there exist$a$-transitions from$q$to$s$and from$q^{\prime}$to$s^{\prime}$.

Finally we perform a breadth-first search on $\mathcal{A}\times\mathcal{A}$, starting in $r$, and remove $q$ from $\mathcal{A}$ every time we encounter an edge between $(s,s^{\prime})$ and $(q,q)$ with $s\neq s^{\prime}$. Since we had removed all unreachable states in $\mathcal{A}$, 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^{\prime})$ with $s\neq s^{\prime}$ to $(t^{\prime},t^{\prime})$ for some state $t^{\prime}$. Removing $t^{\prime}$ eliminates the diamond without altering the language of $\mathcal{A}$. Breadth-first search on $\mathcal{A}\times\mathcal{A}$ costs time $O(|\delta|^{2}|\Sigma|)$, concluding the proof.

B.2 Proofs From Section 3.2

We prove Lemma 3.8 from the main body: See 3.8

Proof B.2**.**

Let $P=(V,A)$ denote the graph with vertices in $V=\{(p,p^{\prime},s)\in Q\times Q\times S\mid(p,s),(p^{\prime},s)\in D\}$ and an edge from $(p,p^{\prime},s)$ to $(r,r^{\prime},t)$ whenever there are edges from $\langle p,s\rangle$ to $\langle r,t\rangle$ and from $\langle p^{\prime},s\rangle$ to $\langle r^{\prime},t\rangle$ in $B_{D,D}$. We have $|V|\leq|Q||D|$ and $|A|\leq|\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^{\prime}_{i},s_{i})$. Let $v_{0}v_{1}\ldots v_{n}$ be a path from $(q,q,s)$ to $(q,q^{\prime},s)$ in $P$, $v_{0}=(q,q,s)$ and $v_{n}=(q,q^{\prime},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^{\prime},s\rangle\}\subseteq\langle q,s\rangle\mathop{\triangleright}w$. We can (breadth-first) search $P$ to calculate $\mathit{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^{\prime},s)$ for each $e=\langle q^{\prime},s\rangle\in\mathit{Co}(d)$. Since $\mathit{Co}(d)$ is a fibre, we have $|\mathit{Co}(d)|\leq|Q|$. Hence we can compute in time $O(|Q||D|+|\delta||T|+|Q||V|)\leq O(|Q|^{2}|D|+|\delta||T|)$ the list $\mathit{CoPath}(d)$ with $|\mathit{CoPath}(d)(e)|\leq|Q||D|$.

We prove Proposition 3.8 from the main body: See 3.8

Proof B.3**.**

We continue from the proof sketch in the main body. Step 1 of the algorithm computes $\mathit{Co}(d)$ and $\mathit{CoPath}(d)$ in time $O(|Q|^{2}|D|+|\delta||T|)$ using Lemma 3.8. We have $|\mathit{CoPath}(d)(e)|\leq|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 $\mathit{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 3.10 from the main body:

See 3.10

Proof B.4**.**

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

B.3 Proofs From Section 3.3

The following lemma is used in the proof of Lemma 3.14: {ourlemma}[]

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^{\prime}(t)\Delta(x)\vec{y}=\sum_{u\in U}\gamma_{u}\Delta^{\prime}(t)\Delta(u)\vec{y}$ for some $\gamma_{u}\in\mathbb{R}$, $u\in U$. Let $s\in S$ and $w\in S^{*}$. Then there exists a set $U^{\prime}$ of words $u^{\prime}\ll_{S}wtx$ such that $\Delta^{\prime}(s)\Delta(wtx)\vec{y}=\sum_{u^{\prime}\in U^{\prime}}\gamma_{u^{\prime}}\Delta^{\prime}(s)\Delta(u^{\prime})\vec{y}$ holds for some $\gamma_{u^{\prime}}\in\mathbb{R}$, $u^{\prime}\in U^{\prime}$.

Proof B.5**.**

We have:

[TABLE]

*Hence choose $U^{\prime}=\{wtu\mid u\in U\}$. *

Now we can prove Lemma 3.14 from the main body: See 3.14

Proof B.6**.**

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^{\prime}(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^{\prime}(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^{\prime}(s^{(n+1)})\Delta(w^{(n+1)})\vec{y}$ was visited by the algorithm: *

Then either $\Delta^{\prime}(s^{(n+1)})\Delta(w^{(n+1)})\vec{y}$ was shown to be dependent on $R(s^{(n+1)})$ at that time, or $\Delta^{\prime}(s^{(n+1)})\Delta(w^{(n+1)})\vec{y}$ was independent of $R(s^{(n+1)})$ at that time, after which $\Delta^{\prime}(s^{(n+1)})\Delta(w^{(n+1)})\vec{y}$ was added to $R(s^{(n+1)})$.

• •

*Or $\Delta^{\prime}(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^{\prime}(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^{\prime}(s^{(q)})\Delta(w^{(p)})\vec{y}$, with $w^{(p)}\ll_{S}w^{(q)}$. By Lemma B.3 the vector $\Delta^{\prime}(s^{(n+1)})\Delta(w^{(n+1)})\vec{y}$ is dependent on vectors of the form $\Delta^{\prime}(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^{\prime}(s^{(n+1)})\Delta(w^{(n+1)})\vec{y}$ is dependent on $R(s^{(n+1)})$.

*Concerning runtime, for every vector $\vec{u}=\Delta^{\prime}(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^{\prime}(s)\Delta(t)\vec{u}$ from $\vec{u}$ in time $O(|Q|^{2})$, as $\Delta^{\prime}(s)\Delta(t)$ is possibly nonzero only in a $|Q|\times|Q|$ submatrix. The algorithm adds $|E(t)|$ vectors to $\mathit{worklist}$ 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 3.21 from the main body:

See 3.21

Proof B.7**.**

*One can compute $\vec{y}$ in time $O(|D|^{\kappa})$. By Lemma 3.8, one can calculate $\mathit{Co}(d)$ in time $O(|Q||D|+|\delta||T_{D}|)$. By Lemma 3.14, 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 3.17 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 3.1 from the main body:

See 3.1

Proof B.8**.**

Denote by $\mathcal{D}$ the set of accepting recurrent SCCs. Using Proposition 3.21 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}|\leq|\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^{\prime}\in\mathcal{D}$, the sets $Q_{D,t}$ and $Q_{D^{\prime},t}$ are disjoint. Thus,

[TABLE]

Hence by Proposition 3.21, one can compute normalisers for all accepting recurrent SCCs in time $O(|Q|^{\kappa}|S|^{\kappa}+|Q|^{3}|E|+|\delta|^{2}|E|)$. Using Proposition 3.5 we get a total runtime of $O(|Q|^{\kappa}|S|^{\kappa}+|Q|^{3}|E|+|\delta|^{2}|E|)$.