| Identifikační kód | RIV/00216224:14330/12:00057483 |
|---|
| Název v anglickém jazyce | Deterministic Automata for the (F,G)-fragment of LTL |
|---|
| Druh | D - Článek ve sborníku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2012 |
|---|
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
|---|
| Počet výskytů výsledku | 2 |
|---|
| Počet tvůrců celkem | 2 |
|---|
| Počet domácích tvůrců | 1 |
|---|
| Výčet všech uvedených jednotlivých tvůrců | Jan Křetínský (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 3503054)
Javier Esparza (státní příslušnost: ES - Španělské království) |
|---|
| Popis výsledku v anglickém jazyce | When dealing with linear temporal logic properties in the setting of e.g. games or probabilistic systems, one often needs to express them as deterministic omega-automata. In order to translate LTL to deterministic omega-automata, the traditional approachfirst translates the formula to a non-deterministic Buchi automaton. Then a determinization procedure such as of Safra is performed yielding a deterministic omega-automaton. We present a direct translation of the (F,G)-fragment of LTL into deterministicomega-automata with no determinization procedure involved. Since our approach is tailored to LTL, we often avoid the typically unnecessarily large blowup caused by general determinization algorithms. We investigate the complexity of this translation andprovide experimental results and compare them to the traditional method. |
|---|
| Klíčová slova oddělená středníkem | linear temporal logic; automata; determinism |
|---|
| Stránka www, na které se nachází výsledek | - |
|---|
| DOI výsledku | 10.1007/978-3-642-31424-7_7 |
|---|