摘要：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.
关键词：CTMDP; Time bounded reachability; Continuous Skolem Problem; Schanuelâs Conjecture
