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.

翻译：以时间为依存的自定义自动数据扩展经典定时自动数据, 且具有离散的概率选择, 允许概率取决于时钟的确切值。 先前的工作已经显示, 至少 3 个时钟的基于时钟的根据时间的概率自动数据, 其数量可达性问题无法确定 。 在本文中, 我们考虑一个亚类的基于时钟的基于时钟的根据时间性定时自动数据, 它有一个时钟, 由直角函数描述时钟的依存性, 并且满足初始化条件, 要求时间在与非三时钟依赖性边缘的某个点上, 时钟必须具有整数值 。 我们提出一个方法来解决这种一时钟的基于时钟的根据时钟的不稳定性定时数的自动数据。 我们的结果通过转换到间隔 Markov 的决策过程获得 。