Revisiting digitization, robustness, and decidability for timed automata
Revisiting digitization, robustness, and decidability for timed automata
复制标题
重新审视定时自动机的数字化、鲁棒性和可判定性
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
J. Worrell
中科院分区：
文献类型：
--
作者：
Joël Ouaknine;J. Worrell
我们考虑了与时间自动机的数字化技术的使用有关的几个问题。这些非常成功的技术将密集时间语言包含问题简化为离散时间，但仅当实现在数字化下关闭并且规范在逆数字化下关闭时才适用。我们证明了，对于时间自动机，前者(实现在数字化下是否闭合)是可判定的，而后者是不可判定的。我们还研究了与时间自动机的稳健语义相关的数字化问题。健壮建模方法通过去除等价性测试的语义引入了时间模糊性。自五年前引入以来，对健壮语义学的研究表明，它产生了与标准语义学大致相同的理论。本文表明，令人惊讶的是，情况并非如此：健壮语义明显不那么容易处理，并且在许多关键方面与标准语义不同。特别是，健壮的语义产生了一个不可判定(非规则)的离散时间理论，这与标准语义形成了鲜明的对比。这使得将数字化技术与健壮的语义一起应用几乎是不可能的。从积极的方面来看，我们证明了时间自动机的健壮语言仍然是递归的。
We consider several questions related to the use of digitization techniques for timed automata. These very successful techniques reduce dense-time language inclusion problems to discrete time, but are applicable only when the implementation is closed under digitization and the specification is closed under inverse digitization. We show that, for timed automata, the former (whether the implementation is closed under digitization) is decidable, but not the latter. We also investigate digitization questions in connection with the robust semantics for timed automata. The robust modeling approach introduces a timing fuzziness through the semantic removal of equality testing. Since its introduction half a decade ago, research into the robust semantics has suggested that it yields roughly the same theory as the standard semantics. This paper shows that, surprisingly, this is not the case: the robust semantics is significantly less tractable, and differs from the standard semantics in many key respects. In particular, the robust semantics yields an undecidable (nonregular) discrete-time theory, in stark contrast with the standard semantics. This makes it virtually impossible to apply digitization techniques together with the robust semantics. On the positive side, we show that the robust languages of timed automata remain recursive.