The stuttering principle revisited

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	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:	Verifikace nekonečně stavových systémů Techniky automatické verifikace a validace softwarových a hardwarových systémů Institut Teoretické Informatiky Vysoce paralelní a distribuované výpočetní systémy