Informace o publikaci

The stuttering principle revisited

Logo poskytovatele
Název česky Znovu o principu periodických vzorů
Autoři

KUČERA Antonín STREJČEK Jan

Rok publikování 2005
Druh Článek v odborném periodiku
Časopis / Zdroj Acta informatica
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Obor Informatika
Klíčová slova linear temporal logic; stuttering
Popis Je známo, že LTL formule bez operátoru "next" jsou invariantní vzhledem k ekvivalenci na slovech obsahující právě ty dvojice, které mají stejné vzorky neopakujících se písmen. V tomto článku je tento princip rozšířen na obecné LTL formule s danou hlobkou zanoření operátorů "next" a "until". Užitím této techniky je dále dokázana sémantická striktnost tří přirozených hierarchií LTL formulí, které jsou paramatrizované hloubkou zanoření zmiňovaných operátorů. Dále je podána efektivní chrakterizace jazyků definivatelných v LTL formulí s omezenou hloubkou zanoření operátoru "next".
Související projekty:

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

Další info