Informace o publikaci
Deeper Connections between LTL and Alternating Automata
| Název česky | Hlubší spojitosti mezi LTL a alternujícími automaty |
|---|---|
| Autoři | |
| Rok publikování | 2005 |
| Druh | Článek ve sborníku |
| Konference | Implementation and Application of Automata |
| Fakulta / Pracoviště MU | |
| Citace | |
| Obor | Informatika |
| Klíčová slova | LTL; alternating automata; model checking |
| Popis | Je známo, že lineární temporální logika (LTL) má stejnou vyjadřovací sílu jako alternujicí 1-weak automaty (A1W automaty, také nazývané lineární automaty nebo velmi slabé automaty). Překlad LTL formulí na jazykově ekvivalentní A1W automat byl popsán v [MSS88]. Opačný překlad byl nezávisle vyvinut v [Roh97] a [LT00]. V první části článku ukazujeme, že druhý převod zbytečně plýtvá temporálními operátory a ukazujeme, jak jej zlepšit. Druhá část článku ukazuje přímou spojitost mezi fragmenty hierarchie Until-Release [CP03] a hloubkou alternace akceptujících a zamítajících stavů v A1W automatu. Na závěr ukazujeme některé důsledky a aplikace těchto výsledků. |
| Související projekty: |