The following technical report is available from http://aib.informatik.rwth-aachen.de:

Computing maximum reachability probabilities in Markovian timed automata Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre AIB 2010-06

We propose a novel stochastic extension of timed automata, i.e. Markovian Timed Automata (MTA). We study the problem of optimizing the reachability probabilities in this model. Two variants are considered, namely, the time-bounded and unbounded reachability. In each case, we propose Bellman equations to characterize the probability. For the former, we provide two approaches to solve the Bellman equations, namely, the discretization and a reduction to Hamilton-Jacobi-Bellman equations. For the latter, we show that in the single-clock case, the problem can be reduced to solving a system of linear equations, whose coefficients are the time-bounded reachability probabilities in CTMDPs.