Sampled semantics of timed automata is a finite approximation of their densetime behavior. While the former is closer to the actual software or hardwaresystems with a fixed granularity of time, the abstract character of the lattermakes it appealing for system modeling and verification. We study one aspect ofthe relation between these two semantics, namely checking whether the systemexhibits some qualitative (untimed) behaviors in the dense time which cannot bereproduced by any implementation with a fixed sampling rate. More formally, theemph{sampling problem} is to decide whether there is a sampling rate such thatall qualitative behaviors (the untimed language) accepted by a given timedautomaton in dense time semantics can be also accepted in sampled semantics. Weshow that this problem is decidable.
展开▼
