Sampled Semantics of Timed Automata
Sampled Semantics of Timed Automata
复制标题
定时自动机的采样语义
DOI：
10.2168/lmcs-6(3:14)2010
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
W. Yi
中科院分区：
文献类型：
--
作者：
P. Abdulla;P. Krcál;W. Yi
时间自动机的采样语义是其稠密时间行为的有限近似。前者更接近于实际的软件或硬件系统，具有固定的时间粒度，而后者的抽象特性使其更适合于系统建模和验证。我们研究这两个语义之间的关系的一个方面，即检查系统是否表现出一些定性（untimed）的行为，在密集的时间，不能复制的任何实现与一个固定的采样率。更正式地说，采样问题是决定是否存在一个采样率，使得在密集时间语义中被给定的时间自动机接受的所有定性行为（非时间语言）也可以在采样语义中被接受。我们证明了这个问题是可判定的。
Sampled semantics of timed automata is a finite approximation of their dense time behavior. While the former is closer to the actual software or hardware systems with a fixed granularity of time, the abstract character of the latter makes it appealing for system modeling and verification. We study one aspect of the relation between these two semantics, namely checking whether the system exhibits some qualitative (untimed) behaviors in the dense time which cannot be reproduced by any implementation with a fixed sampling rate. More formally, the \emph{sampling problem} is to decide whether there is a sampling rate such that all qualitative behaviors (the untimed language) accepted by a given timed automaton in dense time semantics can be also accepted in sampled semantics. We show that this problem is decidable.