On Sampled Semantics of Timed Systems
| Název česky | O diskrétní sémantice časových automatů |
|---|---|
| Autoři | |
| Rok publikování | 2005 |
| Druh | Článek ve sborníku |
| Konference | Foundations of Software Technology and Theoretical Computer Science |
| Fakulta / Pracoviště MU | |
| Citace | |
| Obor | Informatika |
| Klíčová slova | model checking; timed automata; non-emptiness problems; decidability |
| Popis | Č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. |
| Související projekty: |
|