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, 12 s. ISBN 978-3-540-30495-1.
Další formáty:   BibTeX LaTeX RIS
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 (203 Česká republika, garant) a Pavel KRČÁL (203 Česká republika).
Vydání India, Foundations of Software Technology and Theoretical Computer Science, od s. 310-321, 12 s. 2005.
Nakladatel Springer
Další údaje
Originální 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
Změnil Změnil: doc. Mgr. Radek Pelánek, Ph.D., učo 4297. Změněno: 23. 6. 2009 12:59.
Anotace
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.
Anotace č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 VaVNázev: Automatizovaná verifikace paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Standardní projekty
GD102/05/H050, projekt VaVNázev: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Doktorské granty
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumné záměry
1ET408050503, projekt VaVNázev: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Akademie věd ČR, Informační společnost (Národní program výzkumu)
1M0545, projekt VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumná centra (Národní program výzkumu)
VytisknoutZobrazeno: 29. 2. 2020 08:31