Deeper Connections between LTL  and Alternating Automata

Varování

Publikace nespadá pod Ústav výpočetní techniky, 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