Reachability Relations and Sampled Semantics of Timed Systems
2005 (English)Report (Other scientific)
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.
Place, publisher, year, edition, pages
Faculty of Informatics, Masaryk University Brno, Czechia , 2005.
, FIMU-RS, 2005-09
IdentifiersURN: urn:nbn:se:uu:diva-19168OAI: oai:DiVA.org:uu-19168DiVA: diva2:46940