Deeper Connections between LTL  and Alternating Automata

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

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
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:	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