  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.
