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归约到阶数显著低于此前结果的马尔可夫链。由此为更普遍的马尔可夫链类获得更精确的困难性结果。直接应用包括生物系统建模中的问题以及基于正则自动机的计数问题。