Quantitative Temporal Simulation and Refinement Distances for Timed Systems
Quantitative Temporal Simulation and Refinement Distances for Timed Systems
复制标题
定时系统的定量时间模拟和细化距离
DOI：
--
复制
发表时间：
2015
影响因子：
6.8
通讯作者：
Vinayak S. Prabhu
中科院分区：
文献类型：
--
作者：
K. Chatterjee;Vinayak S. Prabhu
我们介绍了定量的改进和定时模拟（定向）指标，并为定时系统纳入Zenoness检查。 ：（1）可能出现的最大正时不匹配，（2）“稳态”最大正时不匹配，其中初始瞬态正时不匹配被忽略，并且（3）（3）（长期）平均正时不匹配这三种不匹配构成了我们的活动时间的三种重要类型。为了计算定量模拟距离的值，我们使用了游戏理论公式，我们在任何所需的准确度中进行了定量模拟距离。 （1）最终决定 - 级别目标，（2）我们提出了用于计算图形游戏中这些目标的最佳值的算法，然后使用这些算法来计算定时自动机上的定时模拟距离。
We introduce quantitative timed refinement and timed simulation (directed) metrics, incorporating zenoness checks, for timed systems. These metrics assign positive real numbers which quantify the timing mismatches between two timed systems, amongst non-zeno runs. We quantify timing mismatches in three ways: (1) the maximal timing mismatch that can arise, (2) the “steady-state” maximal timing mismatches, where initial transient timing mismatches are ignored; and (3) the (long-run) average timing mismatches amongst two systems. These three kinds of mismatches constitute three important types of timing differences. Our event times are the global times, measured from the start of the system execution, not just the time durations of individual steps. We present algorithms over timed automata for computing the three quantitative simulation distances to within any desired degree of accuracy. In order to compute the values of the quantitative simulation distances, we use a game theoretic formulation. We introduce two new kinds of objectives for two player games on finite-state game graphs: (1) eventual debit-sum level objectives, and (2) average debit-sum level objectives. We present algorithms for computing the optimal values for these objectives in graph games, and then use these algorithms to compute the values of the timed simulation distances over timed automata.