We consider the following decision problems: given a finite, rational Markov chain, source and target states, and a rational threshold, does there exist an n such that the probability of reaching the target from the source in n steps is equal to the threshold (resp. crosses the threshold)? These problems are known to be equivalent to the Skolem (resp. Positivity) problems for Linear Recurrence Sequences (LRS). These are number-theoretic problems whose decidability has been open for decades. We present a short, self-contained, and elementary reduction from LRS to Markov Chains that improves the state of the art as follows: (a) We reduce to ergodic Markov Chains, a class that is widely used in Model Checking. (b) We reduce LRS to Markov Chains of significantly lower order than before. We thus get sharper hardness results for a more ubiquitous class of Markov Chains. Immediate applications include problems in modeling biological systems, and regular automata-based counting problems.
翻译:我们考虑以下判定问题:给定一个有限的有理马尔可夫链、源状态与目标状态,以及一个有理阈值,是否存在自然数n使得从源状态出发经过n步到达目标状态的概率等于该阈值(或跨越该阈值)?这些问题已知等价于线性递推序列(LRS)的Skolem问题(或正定性问题)。这些数论问题的可判定性已悬而未决数十年。我们提出一个简洁、自包含且初等的从LRS到马尔可夫链的归约,其在以下方面改进了现有技术:(a)我们将问题归约到遍历马尔可夫链——一种在模型检验中广泛使用的类别;(b)与现有结果相比,我们将LRS归约到阶数显著更低的马尔可夫链。由此,我们为更普遍的马尔可夫链类获得了更强的难解性结果。直接应用包括生物学系统建模问题及基于正则自动机的计数问题。