Technical Reports

The report FIMU-RS-2005-09

Reachability Relations and Sampled Semantics of Timed Systems

by Pavel Krèál, Radek Pelánek, A full version of the paper presented at conference FSTTCS 2005. December 2005, 31 pages.

FIMU-RS-2005-09. Available as Postscript, PDF.

Abstract:

Timed systems can be considered with two types of semantics -- dense time semantics and discrete time semantics. The most typical examples of both of them are real semantics and sampled semantics (i.e., discrete semantics with a fixed time step epsilon). In this work, we study different aspects of sampled semantics. At first, we study reachability relations between configurations of a timed automaton and provide a novel effective characterization of reachability relations. This result is used for proving our main result --- decidability of non-emptiness of a timed automaton omega-language in some sampled semantics (this problem was previously wrongly classified as undecidable). Also, we study relations between real semantics and sampled semantics with respect to different behavioral equivalences. Finaly, we study decidability of reachability problem for stopwatch automata with sampled semantics.