一句话：将单时钟初始化时钟依赖概率定时自动机转为区间MDP，证明其定量与定性可达性可在多项式时间求解。
时钟依赖概率定时自动机在经典定时自动机上加入离散概率选择，并允许转移概率依赖时钟的精确值；已有工作表明，至少三个时钟时其定量可达性问题不可判定。本文研究一个可判定子类：仅含一个时钟，时钟依赖由仿射函数描述，并满足初始化条件——在两次具有非平凡时钟依赖的边之间，时钟必须在某时刻取整数值。作者将此类单时钟初始化时钟依赖概率定时自动机转换为区间马尔可夫决策过程，从而证明其定量与定性可达性问题均可在多项式时间内求解。
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.
@article{paperbot1269,
title = {Probabilistic Timed Automata with One Clock and Initialised Clock-Dependent Probabilities},
author = {Jeremy Sproston},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 4},
year = {2021},
doi = {10.46298/lmcs-17(4:6)2021}
}