The conventional perspective on Markov chains considers decision problems concerning the probabilities of temporal properties being satisfied by traces of visited states. However, consider the following query made of a stochastic system modelling the weather: given the conditions today, will there be a day with less than 50\% chance of rain? The conventional perspective is ill-equipped to decide such problems regarding the evolution of the initial distribution. The alternate perspective we consider views Markov chains as distribution transformers: the focus is on the sequence of distributions on states at each step, where the evolution is driven by the underlying stochastic transition matrix. More precisely, given an initial distribution vector $\mu$, a stochastic update transition matrix $M$, we ask whether the ensuing sequence of distributions $(\mu, M\mu, M^2\mu, \dots)$ satisfies a given temporal property. This is a special case of the model-checking problem for linear dynamical systems, which is not known to be decidable in full generality. The goal of this article is to delineate the classes of instances for which this problem can be solved, under the assumption that the dynamics is governed by stochastic matrices.

翻译：传统视角下的马尔可夫链研究关注于状态轨迹满足时序性质的概率判定问题。然而，考虑以下针对天气随机系统的查询：给定今日天气条件，未来是否存在某日降雨概率低于50%？传统方法难以处理此类涉及初始分布演化的判定问题。本文采用的替代视角将马尔可夫链视为分布变换器：关注点在于每一步状态分布的演化序列，其演化过程由底层随机转移矩阵驱动。更精确地说，给定初始分布向量 $\mu$ 和随机更新转移矩阵 $M$，我们研究由此产生的分布序列 $(\mu, M\mu, M^2\mu, \dots)$ 是否满足给定的时序性质。这是线性动力系统模型检验问题的特例，而该问题在一般情形下的可判定性尚未可知。本文旨在动力学受随机矩阵约束的前提下，界定该问题可解的实例类别。