Publication details
On Sampled Semantics of Timed Systems
| Basic information | |
|---|---|
| Original title: | On Sampled Semantics of Timed Systems |
| Authors: | Radek Pelánek, Pavel Krčál |
| Further information | |
|---|---|
| Citation: | PELÁNEK, Radek  - KRČÁL, Pavel. On Sampled Semantics of Timed Systems. In Foundations of Software Technology and Theoretical Computer Science. India : Springer, 2005. ISBN 978-3-540-30495-1, pp. 310-321. Hyderabad. |
| Original language: | English |
| Field: | Informatika |
| Type: | Article in Proceedings |
| Keywords: | model checking; timed automata; non-emptiness problems; decidability |
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:
- Automated Verification of Parallel and Distributed Systems
- Integrated approach to education of PhD students in the area of parallel and distributed systems
- Techniques for automatic verification and validation of software nad hardware systems
- Institute for Theoretical Computer Science
- Highly Parallel and Distributed Computing Systems
