Skolem and positivity completeness of ergodic Markov chains

INFORMATION PROCESSING LETTERS(2024)

引用 0|浏览0
暂无评分
摘要
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 nth 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.
更多
查看译文
关键词
Formal methods,Ergodic Markov chains,Reachability,Model checking,Linear recurrence sequences
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要