论文标题
概率定时自动机，一个时钟和初始化的时钟依赖性概率
Probabilistic Timed Automata with One Clock and Initialised Clock-Dependent Probabilities
论文作者
论文摘要
与时钟相关的概率定时自动机扩展了具有离散概率选择的经典定时自动机，其中允许概率取决于时钟的确切值。先前的工作表明，与至少三个时钟的时钟相关概率定时自动机的定量可及性问题是不可确定的。在本文中，我们考虑了具有一个时钟的概率定时自动机的子类，该概率定时自动机具有一个时钟，具有仿射函数描述的时钟依赖性，并且满足初始化条件，要求在以非平常时钟依赖性边缘的某个点上，时钟必须具有integer值。我们提出了一种在多项式时间定量和定性的可及性问题中求解这种单锁初始化的时钟依赖性概率时机自动机的方法。我们的结果是通过转换向马尔可夫决策过程的转换而获得的。
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.
