Deeper Connections between LTL and Alternating Automata

• Název česky: Hlubší spojitosti mezi LTL a alternujícími automaty
• Autoři: PELÁNEK Radek; STREJČEK Jan
• Rok publikování: 2005
• Druh: Článek ve sborníku
• Konference: Implementation and Application of Automata
• Fakulta / Pracoviště MU: Fakulta informatiky
• 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

• Automatizovaná verifikace paralelních a distribuovaných systémů
• Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
• Institut Teoretické Informatiky
• Vysoce paralelní a distribuované výpočetní systémy