Reachability problems for Markov chains |
| |
Authors: | S Akshay Timos Antonopoulos Joël Ouaknine James Worrell |
| |
Affiliation: | 1. Department of Computer Science and Engineering, Indian Institute of Technology Bombay, India;2. Department of Computer Science, University of Oxford, UK |
| |
Abstract: | We consider the following decision problem: given a finite Markov chain with distinguished source and target states, and given a rational number r, does there exist an integer n such that the probability to reach the target from the source in n steps is r? This problem, which is not known to be decidable, lies at the heart of many model checking questions on Markov chains. We provide evidence of the hardness of the problem by giving a reduction from the Skolem Problem: a number-theoretic decision problem whose decidability has been open for many decades. |
| |
Keywords: | Formal methods Skolem problem Positivity problem Probabilistic model checking Markov chains |
本文献已被 ScienceDirect 等数据库收录! |