On Sampled Semantics of Timed Systems

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

Základní údaje

Originální název

On Sampled Semantics of Timed Systems

Název česky

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

Autoři

PELÁNEK, Radek a Pavel KRČÁL

Vydání

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

Nakladatel

Springer

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Indie

Utajení

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

Kód RIV

RIV/00216224:14330/05:00012726

Organizační jednotka

Fakulta informatiky

ISBN

978-3-540-30495-1

UT WoS

000234885800025

Klíčová slova anglicky

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

Štítky

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

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

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.

Česky

Č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.

---

Návaznosti

GA201/03/0509, projekt VaV	Název: Automatizovaná verifikace paralelních a distribuovaných systémů Investor: Grantová agentura ČR, Automatizovaná verifikace paralelních a distribuovaných systémů
GD102/05/H050, projekt VaV	Název: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů Investor: Grantová agentura ČR, Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
MSM0021622419, záměr	Název: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1ET408050503, projekt VaV	Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů
1M0545, projekt VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky