Robust Analysis of Timed Automata via Channel Machines
Robust Analysis of Timed Automata via Channel Machines
复制标题
通过通道机进行定时自动机的鲁棒分析
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Pierre
中科院分区：
文献类型：
--
作者：
P. Bouyer;N. Markey;Pierre
尽管定时系统的形式验证已成为一个非常活跃的研究领域，但定时自动机的理想化数学语义无法忠实地实现。因此，一些工作重点关注了时间自动机的修改语义，以确保可实现性，以及用于安全的鲁棒模型检查算法，并且后来设计了 LTL 属性。最近，提出了一种新方法，它将定时自动机的（标准）模型检查减少到通道机上的其他验证问题。由于将修改后的语义作为定时系统网络的新编码，我们提出了两种方法的原始组合，并证明了 coFlat-MTL（MTL 的一个大片段）的鲁棒模型检查是 EXPSPACE-Complete。
Whereas formal verification of timed systems has become a very active field of research, the idealised mathematical semantics of timed automata cannot be faithfully implemented. Several works have thus focused on a modified semantics of timed automata which ensures implementability, and robust model-checking algorithms for safety, and later LTL properties have been designed. Recently, a new approach has been proposed, which reduces (standard) model-checking of timed automata to other verification problems on channel machines. Thanks to a new encoding of the modified semantics as a network of timed systems, we propose an original combination of both approaches, and prove that robust model-checking for coFlat-MTL, a large fragment of MTL, is EXPSPACE-Complete.