Reachability probabilities in Markovian Timed Automata

We propose a novel stochastic extension of timed automata, i.e. Markovian Timed Automata. We study the problem of optimizing time-bounded reachability probabilities in this model, i.e., the maximum likelihood to hit a set of goal locations within a given deadline. We propose Bellman equations to characterize the probability, and provide two approaches to solve the Bellman equations, namely, a discretization and a reduction to Hamilton-Jacobi-Bellman equations.