Deeper Connections between LTL and Alternating Automata

PELÁNEK, Radek a Jan STREJČEK. Deeper Connections between LTL and Alternating Automata. In Implementation and Application of Automata. Berlin, Heidelberg: Springer-Verlag. s. 238-249. ISBN 978-3-540-31023-5. 2005.

Základní údaje

• Originální název: Deeper Connections between LTL and Alternating Automata
• Název česky: Hlubší spojitosti mezi LTL a alternujícími automaty
• Autoři: PELÁNEK, Radek (203 Česká republika) a Jan STREJČEK (203 Česká republika, garant).
• Vydání: Berlin, Heidelberg, Implementation and Application of Automata, od s. 238-249, 12 s. 2005.
• Nakladatel: Springer-Verlag

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Stať ve sborníku
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Francie
• Utajení: není předmětem státního či obchodního tajemství
• Kód RIV: RIV/00216224:14330/05:00012729
• Organizační jednotka: Fakulta informatiky
• ISBN: 978-3-540-31023-5
• UT WoS: 000236480300020
• Klíčová slova anglicky: LTL; alternating automata; model checking
• Štítky: alternating automata, LTL, Model checking
• Příznaky: Mezinárodní význam, Recenzováno

Anotace

It is known that Linear Temporal Logic (LTL) has the same expressive power as alternating 1-weak automata (A1W automata, also called alternating linear automata or very weak alternating automata). A~translation of LTL formulae into a language equivalent A1W automata has been introduced in [MSS88]. The inverse translation has been developed independently in [Roh97] and [LT00]. In the first part of the paper we show that the latter translation wastes temporal operators and we propose some improvements of this translation. The second part of the paper draws a direct connection between fragments of the Until-Release hierarchy [CP03] and alternation depth of nonaccepting and accepting states in A1W automata. We also indicate some corollaries and applications of these results.

Anotace česky

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ů.

Návaznosti

• GA201/03/0509, projekt VaV: Název: Automatizovaná verifikace paralelních a distribuovaných systémů

Investor: Grantová agentura ČR, Automatizovaná verifikace paralelních a distribuovaných systémů

• GD102/05/H050, projekt VaV: Název: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů

Investor: Grantová agentura ČR, Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů

• MSM0021622419, záměr: Název: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy

• 1M0545, projekt VaV: Název: Institut Teoretické Informatiky

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky