论文标题
概率定时自动机的最小见证人
Minimal witnesses for probabilistic timed automata
论文作者
论文摘要
证明子系统已被证明是对概率系统分析的一个有用概念，例如，作为有关给定财产为什么保留或作为改进算法的输入的诊断信息。本文介绍了概率定时自动机（PTA）中有关可及性问题的见证子系统。使用新的操作对差矩阵，可以将PTA的有限状态分配商的Farkas证书转化为见证子系统。我们介绍了在三个最小值概念下计算最小见证子系统的算法，这些算法从不同的角度捕获了定时行为，并讨论了它们的复杂性。
Witnessing subsystems have proven to be a useful concept in the analysis of probabilistic systems, for example as diagnostic information on why a given property holds or as input to refinement algorithms. This paper introduces witnessing subsystems for reachability problems in probabilistic timed automata (PTA). Using a new operation on difference bounds matrices, it is shown how Farkas certificates of finite-state bisimulation quotients of a PTA can be translated into witnessing subsystems. We present algorithms for the computation of minimal witnessing subsystems under three notions of minimality, which capture the timed behavior from different perspectives, and discuss their complexity.
