Clock-Dependent Probabilistic Timed Automata with One Clock and No Memory

Clock-dependent probabilistic timed automata extend probabilistic timed automata by letting the probabilities of discrete transitions depend on the exact values of clock variables. The probabilistic reachability problem for clock-dependent probabilistic timed automata has been shown previously to be undecidable. We consider a subclass with one clock and in which nondeterministic choice is made in a memoryless fashion, i.e., nondeterministic choice depends the current state only. We show that, for this subclass, the reachability problem can be solved by constructing and analysing a finite-state parametric Markov chain using established methods.