Sampled Semantics of Timed Automata

TL;DR

This paper investigates the relationship between dense and sampled semantics of timed automata, focusing on whether all qualitative behaviors in dense time can be reproduced with a fixed sampling rate, and proves this problem is decidable.

Contribution

It introduces and proves the decidability of the sampling problem, linking dense and sampled semantics of timed automata.

Findings

The sampling problem for timed automata is decidable.

A fixed sampling rate can reproduce all qualitative behaviors of a timed automaton.

The results bridge the gap between dense and sampled semantics in system modeling.

Abstract

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.