论文标题
概率定时自动机的向后无关：复制报告
Backwards Reachability for Probabilistic Timed Automata: A Replication Report
论文作者
论文摘要
向后可达性是一种基于高效区域的方法，用于检查概率定时自动机W.R.T. PTCTL属性。但是，当前的实现仅限于可及性属性的最大概率。在本文中，我们报告了我们作为适度工具集的一部分向后无关的新实施。它对最低和最大概率的支持，直到公式使其成为当今最普遍的实施。我们将其行为与呈现向后无关技术的原始论文中报道的实验结果进行了比较。
Backwards reachability is an efficient zone-based approach for model checking probabilistic timed automata w.r.t. PTCTL properties. Current implementations, however, are restricted to maximum probabilities of reachability properties. In this paper, we report on our new implementation of backwards reachability as part of the Modest Toolset. Its support for minimum and maximum probabilities of until formulas makes it the most general implementation available today. We compare its behaviour to the experimental results reported in the original papers presenting the backwards reachability technique.
