Computing maximum reachability probabilities in Markovian timed automata
Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre
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.