Sampled Semantics of Timed Automata

Sampled semantics of timed automata is a nite approximation of their dense time behavior. While the former is closer to the actual software or hardware systems ed granularity of time, the abstract character of the latter makes it appealing for system modeling and verication. 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 xed sampling rate. More formally, the 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.

• Type: Journal
• Year: 2010
• Where: CORR
• Authors: Parosh Aziz Abdulla, Pavel Krcál, Wang Yi
• Keywords: CORR 2010, Dense Time, Dense Time Behavior, Education, Semantics