What is decidable about the Stochastic Reachability Problem?

Abstract

We consider the open Stochastic Reachability Problem: given a stochastic matrix $K\in\mathbb{Q}^{d\times d}$, probability distributions $x,y\in\mathbb{Q}^d$, and a non-negative constant $r\in\mathbb{Q}$, determine whether there exists an $n\in\mathbb{N}$ such that $x^\top K^n y =r$. The restriction to random walks, the Markov Reachability Problem, is the task of determining whether there exists an $n\in\mathbb{N}$ such that the probability of travelling from a source state to a target state in $n$ steps is equal to $r$. We establish decidability results for: walks on undirected graphs, hyperplane walks, Bernoulli walks on cycles, and circulant walks on certain finite groups. We illustrate this note with examples from self-organising lists and card shuffling.