Deeper Connections between LTL and Alternating Automata

Logo poskytovatele
Logo poskytovatele

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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.