Skip to main content

Model Checking Markov Chains Against Unambiguous Automata: The Qualitative Case

This is my first blog post. The purpose of this blog is to describe some neat ideas from my research. Ideally only one idea per post, which explains the title of this blog.

Today I start with a classical topic from probabilistic verification: model checking Markov chains against $\omega$-regular specifications. I will focus on specifications given by Büchi automata, which are automata like this one:

This Büchi automaton accepts all infinite words over $\{a,b\}$ that start with $a$. The automaton is nondeterministic. The automaton is also unambiguous, which means that every infinite word has at most one accepting run.

A Markov chain, on the other hand, generates infinite words. A Markov chain looks like this:

For instance, with probability $\frac12 \cdot \frac12 \cdot 1 = \frac14$ it generates an infinite word that starts with $a b a$. For simplicity, we consider only a very simple Markov chain in this post:

This Markov chain generates an infinite word over $\{a,b\}$ uniformly at random. Having fixed this random word generator, we consider the following problem:
Given a nondeterministic Büchi automaton.
Is the probability that it accepts a random (infinite) word positive?
Let's make two further assumptions: The given automaton is strongly connected (every state is reachable from every other state) and all states are accepting:

These assumptions don't take much away from the key challenges. In fact, the problem is PSPACE-complete, with or without all mentioned assumptions. The only thing that will make the problem easier is if the given automaton is unambiguous. And that is what this post is about.

For perspective, let's first solve the problem for possibly ambiguous automata. We determinize the automaton (starting from state 1) with the standard subset construction:
Remembering that the letters have probability 1/2 each, we see a Markov chain shine through:
That Markov chain, call it $\mathcal{M}_{\mathit{det}}$, may have two kinds of bottom SCCs: a rejecting one, which is the one with the empty set $\emptyset$, and accepting ones, which are the other bottom SCCs. In the example there is one rejecting and one accepting bottom SCC. The probability that the given automaton accepts a random word is equal to the probability that $\mathcal{M}_{\mathit{det}}$ reaches an accepting bottom SCC, here $\frac12$.
The probability of accepting a random word is positive if and only if $\, \mathcal{M}_{\mathit{det}}$ has an accepting bottom SCC.
The determinized automaton is of exponential size, so the proposition does not directly lead to a polynomial-time algorithm.

In the unambiguous case we can do better: there is a polynomial-time algorithm. Consider again our unambiguous automaton

and its transition matrices \[\begin{aligned} T(a) &= \begin{pmatrix} 1 & 0 & 1 \\ 1 & 0 & 1 \\ 0 & 0 & 0 \end{pmatrix} \\[1em] T(b) &= \begin{pmatrix} 0 & 0 & 0 \\ 0 & 1 & 0 \\ 0 & 1 & 0 \end{pmatrix} \end{aligned} \] and the transition matrix of an "average" letter \[ T \ = \ \frac12 (T(a) + T(b)) \ = \ \begin{pmatrix} \frac12 & 0 & \frac12 \\ \frac12 & \frac12 & \frac12 \\ 0 & \frac12 & 0 \end{pmatrix}\,. \] More precisely, the $(i,j)$-entry of $T$ is the probability that a random letter labels a transition from state $i$ to state $j$. This generalizes smoothly to random finite words:
The $(i,j)$-entry of $\ T^n$ is the probability that a random word of length $n$ labels a path from state $i$ to state $j$.
For this property, unambiguousness of the automaton is crucial: any word labels at most 1 path from $i$ to $j$.

Let's analyze the limit behaviour of the matrix powers $T, T^2, T^3, \ldots$ By the proposition, all entries of $T^n$ are at most 1. There are two cases:
  • $T, T^2, T^3, \ldots$ converges to the zero matrix.
  • $T, T^2, T^3, \ldots$ does not converge to the zero matrix.
By strong connectedness, either all or no entries of $T^n$ converge to 0 for $n \to \infty$.
  • If the Markov chain $\mathcal{M}_{\mathit{det}}$ does not have an accepting bottom SCC then an infinite random word will almost surely lead to the rejecting bottom SCC. So the probability that a random infinite word labels an automaton path from a start state is zero. By the proposition, we are in the first case.
  • If the Markov chain $\mathcal{M}_{\mathit{det}}$ has an accepting bottom SCC then some finite word $w$ (which has positive probability) leads to this accepting bottom SCC, and all infinite extensions of $w$ label infinite paths of the automaton. So the probability that a random infinite word labels an automaton path is positive. By the proposition, we are in the second case.
It follows that the probability of accepting a random word is positive if and only if $T, T^2, T^3, \ldots$ does not converge to the zero matrix.

Since all entries of $T^n$ are at most $1$, standard matrix theory says that the spectral radius of $T$ (i.e., the largest absolute value of the eigenvalues of $T$) is at most $1$. We also have that $T, T^2, T^3, \ldots$ converges to the zero matrix if and only if the spectral radius of $T$ is less than $1$. So:
The probability of accepting a random word is positive if and only if the spectral radius of $\ T$ is $1$.
The spectral radius of $T$ is $1$ if and only if $T$ has an eigenvector with eigenvalue $1$, i.e., a nonzero vector $x$ with $T x = x$. This amounts to checking the satisfiability of a linear system of equations. In our example we have: \[ T \begin{pmatrix}1 \\ 2 \\ 1 \end{pmatrix} \ = \ \begin{pmatrix} \frac12 & 0 & \frac12 \\ \frac12 & \frac12 & \frac12 \\ 0 & \frac12 & 0 \end{pmatrix} \begin{pmatrix}1 \\ 2 \\ 1 \end{pmatrix} \ = \ \begin{pmatrix}1 \\ 2 \\ 1 \end{pmatrix} \] We get:
Given an unambiguous Büchi automaton, one can decide in polynomial time whether the probability that it accepts a random word is positive.
A Markov chain may also be input:
Given a Markov chain and an unambiguous Büchi automaton, one can decide in polynomial time whether the probability is positive that the automaton accepts a word randomly generated by the Markov chain.
This result may be sharpened by replacing "polynomial time" by the complexity class "NC", which captures problems that can be efficiently solved in parallel. This combines nicely with a translation from LTL to unambiguous Büchi automata: the translation is exponential but can be computed by a PSPACE-transducer. Altogether, we obtain a PSPACE algorithm for model checking Markov chains against LTL. The problem is PSPACE-complete, so this automata-theoretic algorithm is optimal.

In a forthcoming post I'll show that in addition to comparing the probability with zero one can compute the probability equally efficiently.

The material from this post is from a CAV'16 paper by Christel Baier, Joachim Klein, Sascha Klüppelholz, David Müller, James Worrell, and myself.

Comments

Popular posts from this blog

Unambiguous Automata: From PSPACE to P

Computer science is about leveraging mathematical structure, for instance, in order to accelerate algorithms. More often than we'd like we can't accelerate much: For instance, checking two NFAs for language inclusion or equivalence is PSPACE-complete. Even the problem whether an NFA accepts all words is PSPACE-complete. For DFAs, those problems are easy. This means that for NFAs we can't do much better than determinizing (using the subset construction and incurring an exponential blowup) and solving the resulting DFA problem.

In this post I'll discuss an automata problem that seems to call for determinization and is, in fact, PSPACE-complete for NFAs. But there is an efficient algorithm for unambiguous automata.

Here is an example of an unambiguous automaton:
The notion of accepting states is not used in this post. By unambiguousness I just mean that the automaton has no diamonds, that is, for any states $q, r$, any word $w$ labels at most one path from $q$ to $r$. (…

Infinitely many states and no memory

Markov Decision Processes (MDPs) are Markov chains plus nondeterminism: some states are random, the others are controlled (nondeterministic). In the pictures, the random states are round, and the controlled state are squares:
The random states come with a distribution over successor states, but in the controlled states a controller chooses a successor state (or a probability distribution over the successor states). For instance, the controller could stay on the leftmost column forever, by always choosing to go one state down. Or the controller could go right at some point; in the random state a successor is picked randomly, either the initial state or the state on the right, according to the blue probabilities.

What objective should the controller aim at? In this post, the objective will be the following: visit green states infinitely often, and red states only finitely often. Here is the previous MDP with colours:
Since the controller wants to visit (infinitely many) green states…