| Summary: | Clock-dependent probabilistic timed automata extend classical timed automata
with discrete probabilistic choice, where the probabilities are allowed to
depend on the exact values of the clocks. Previous work has shown that the
quantitative reachability problem for clock-dependent probabilistic timed
automata with at least three clocks is undecidable. In this paper, we consider
the subclass of clock-dependent probabilistic timed automata that have one
clock, that have clock dependencies described by affine functions, and that
satisfy an initialisation condition requiring that, at some point between
taking edges with non-trivial clock dependencies, the clock must have an
integer value. We present an approach for solving in polynomial time
quantitative and qualitative reachability problems of such one-clock
initialised clock-dependent probabilistic timed automata. Our results are
obtained by a transformation to interval Markov decision processes.
|
|---|