On Sampled Semantics of Timed Systems

PELÁNEK, Radek and Pavel KRČÁL. On Sampled Semantics of Timed Systems. In Foundations of Software Technology and Theoretical Computer Science. India: Springer, 2005, p. 310-321. ISBN 978-3-540-30495-1.

Basic information

Original name

On Sampled Semantics of Timed Systems

Name in Czech

O diskrétní sémantice časových automatů

Authors

PELÁNEK, Radek (203 Czech Republic, guarantor) and Pavel KRČÁL (203 Czech Republic)

Edition

India, Foundations of Software Technology and Theoretical Computer Science, p. 310-321, 12 pp. 2005

Publisher

Springer

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

India

Confidentiality degree

není předmětem státního či obchodního tajemství

RIV identification code

RIV/00216224:14330/05:00012726

Organization unit

Faculty of Informatics

ISBN

978-3-540-30495-1

UT WoS

000234885800025

Keywords in English

model checking; timed automata; non-emptiness problems; decidability

Tags

decidability, Model checking, non-emptiness problems, timed automata

Tags

International impact, Reviewed

---

Abstract

V originále

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.

In Czech

Časové automaty můžeme uvažovat s dvěma typy sémantik - sémantika hustého času a diskrétní sémantika. Nejtypičtějšími příklady jsou reálná sémantika a vzorkovací sémantika (tj. diskrétní sémantika s pevným časovým krokem epsilon). V tomto článku studujeme vztah mezi reálnou a vzorkovací sémantikou vzhledem k různým ekvivalencím chování. Také studujeme problém dosažitelnosti ve vzorkovací sémantice pro automaty se stopkami. Naším hlavním technickým výsledkem je pak rozhodnutelnost problému neprázdnosti jazyka nekonečných slov zadaného časového automatu v nějaké vzorkovací sémantice (tento problém byl dříve chybně označen jako nerozhodnutelný). Náš důkaz využívá nové charakterizace dosažitelnosti mezi konfiguracemi časového automatu.

---

Links

GA201/03/0509, research and development project	Name: Automatizovaná verifikace paralelních a distribuovaných systémů Investor: Czech Science Foundation, Automated Verification of Parallel and Distributed Systems
GD102/05/H050, research and development project	Name: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů Investor: Czech Science Foundation, Integrated approach to education of PhD students in the area of parallel and distributed systems
MSM0021622419, plan (intention)	Name: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems
1ET408050503, research and development project	Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems
1M0545, research and development project	Name: Institut Teoretické Informatiky Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science