We consider the following Markov Reachability decision problems that view Markov Chains as Linear Dynamical Systems: given a finite, rational Markov Chain, source and target states, and a rational threshold, does the probability of reaching the target from the source at the $n^{th}$ step: (i) equal the threshold for some $n$? (ii) cross the threshold for some $n$? (iii) cross the threshold for infinitely many $n$? These problems are respectively known to be equivalent to the Skolem, Positivity, and Ultimate Positivity problems for Linear Recurrence Sequences (LRS), number-theoretic problems whose decidability has been open for decades. We present an elementary reduction from LRS Problems to Markov Reachability Problems that improves the state of the art as follows. (a) We map LRS to ergodic (irreducible and aperiodic) Markov Chains that are ubiquitous, not least by virtue of their spectral structure, and (b) our reduction maps LRS of order $k$ to Markov Chains of order $k+1$: a substantial improvement over the previous reduction that mapped LRS of order $k$ to reducible and periodic Markov chains of order $4k+5$. This contribution is significant in view of the fact that the number-theoretic hardness of verifying Linear Dynamical Systems can often be mitigated by spectral assumptions and restrictions on order.
翻译:我们考虑将马尔可夫链视为线性动力系统的以下马尔可夫可达性判定问题:给定一个有限有理马尔可夫链、源状态与目标状态以及一个有理阈值,判断从源状态出发在第$n$步到达目标状态的概率:(i) 是否存在某个$n$使得该概率等于阈值?(ii) 是否存在某个$n$使得该概率跨越阈值?(iii) 是否存在无穷多个$n$使得该概率跨越阈值?这些问题分别等价于线性递归序列(LRS)的Skolem问题、正性问题和终极正性问题——这些数论问题的可判定性已悬而未决数十年。本文提出一种从LRS问题到马尔可夫可达性问题的初等归约,在以下方面改进了现有技术:(a) 将LRS映射到遍历的(不可约且非周期的)马尔可夫链,这类链因其谱结构而普遍存在;(b) 该归约将$k$阶LRS映射到$k+1$阶马尔可夫链,相较于此前将$k$阶LRS映射到$4k+5$阶可约周期马尔可夫链的归约实现了显著改进。鉴于验证线性动力系统的数论难度通常可通过谱假设与阶数限制得到缓解,这一贡献具有重要意义。