粗糙的抽象使芝诺行为难以检测
Coarse abstractions make Zeno behaviours difficult to detect
摘要：
一个时间自动机的无限运行是芝诺，如果它只跨越有限的时间。这样的运行被认为是不可行的，因此重要的是检测它们，或者双重地找到非Zeno的运行。近年来，时间自动机的可达性检验方法得到了很大的改进。我们表明，这些非常有效的优化测试的芝诺运行成本高。特别是，我们展示了NP-完备性的LU外推Behrmann等人。我们详细分析了这种复杂性的来源，并给出了外推算子的一般条件，保证了Zenoness检查的多项式复杂性（低）。我们提出了一个轻微的削弱满足这些条件的LU外推。
英文摘要：
An infinite run of a timed automaton is Zeno if it spans only a finite amount of time. Such runs are considered unfeasible and hence it is important to detect them, or dually, find runs that are non-Zeno. Over the years important improvements have been obtained in checking reachability properties for timed automata. We show that some of these very efficient optimizations make testing for Zeno runs costly. In particular we show NP-completeness for the LU-extrapolation of Behrmann et al. We analyze the source of this complexity in detail and give general conditions on extrapolation operators that guarantee a (low) polynomial complexity of Zenoness checking. We propose a slight weakening of the LU-extrapolation that satisfies these conditions.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
