HomeNewsCase StudiesPeoplePublications
[CHKM11b] T. Chen, T. Han, J.-P. Katoen and A. Mereacre. Reachability Probabilities in Markovian Timed Automata. In Proc. 50th IEEE Conference on Decision and Control and European Control Conference (CDC-ECC'11), pages 7075-7080, IEEE Press. December 2011. [pdf] [bib]
Downloads:  pdf pdf (260 KB)  bib bib
Abstract. 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.