论文标题
关于CTMDPS中有时的可达性的可定义性
On Decidability of Time-bounded Reachability in CTMDPs
论文作者
论文摘要
我们考虑连续时间马尔可夫决策过程的时间限制的可达性问题。我们表明，该问题是Schanuel猜想的可决定性的。我们的决策程序依赖于最佳策略的结构以及对实物理论的条件可决定性（根据Schanuel的猜想）的结构，并以指数和三角函数在有限域上扩展。我们进一步表明，任何无条件的可决定性结果都将意味着有限的连续Skolem问题无条件的可决定性，或者等效地，检查指数多项式是否在有界间隔中具有非区分零。我们注意到，后一种问题也可以根据Schanuel的猜想来确定，但是寻找无条件的决策程序仍然是长期以来的开放问题。
We consider the time-bounded reachability problem for continuous-time Markov decision processes. We show that the problem is decidable subject to Schanuel's conjecture. Our decision procedure relies on the structure of optimal policies and the conditional decidability (under Schanuel's conjecture) of the theory of reals extended with exponential and trigonometric functions over bounded domains. We further show that any unconditional decidability result would imply unconditional decidability of the bounded continuous Skolem problem, or equivalently, the problem of checking if an exponential polynomial has a non-tangential zero in a bounded interval. We note that the latter problems are also decidable subject to Schanuel's conjecture but finding unconditional decision procedures remain longstanding open problems.
