On Sampled Semantics of Timed Systems

Investor logo
Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

PELÁNEK Radek KRČÁL Pavel

Year of publication 2005
Type Article in Proceedings
Conference Foundations of Software Technology and Theoretical Computer Science
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords model checking; timed automata; non-emptiness problems; decidability
Description 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). We investigate the relations between real semantics and sampled semantics with respect to different behavioral equivalences. Also, we study decidability of reachability problem for stopwatch automata with sampled semantics. Finally, our main technical contribution is decidability of non-emptiness of a timed automaton omega-language in some sampled semantics (this problem was previously wrongly classified as undecidable). For the proof we employ a novel characterization of reachability relations between configurations of a timed automaton.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.