On Alternative Construction of LTL Tableau

Logo poskytovatele

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Název česky O alternativní konstrukci LTL tabla
Autoři

ŠIMŠA Jiří

Rok publikování 2006
Druh Článek ve sborníku
Konference 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006)
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Obor Informatika
Klíčová slova model checking; linear temporal logic; tableau construction
Popis Lineární temporální logika (LTL) je zaběhnutý a rozsáhle studovaný formalismus z oblasti formální verifikace. V určitých aplikacích LTL, jako například ověřování modelů, je vhodné identifikovat formuli LTL s automatem, který akceptuje právě ty vstupy, které splňují formuli. V tomto článku osvojujeme tento, automato-teoretický, přístup and prezentujeme konstrukci takového automatu. Narozdíl od již existujících konstrukcí, je naše konstrukce založena na iterativní expanzi a normování formulí.
Související projekty:

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