On Alternative Construction of LTL Tableau
| Název česky | O alternativní konstrukci LTL tabla |
|---|---|
| Autoři | |
| 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 | |
| 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: |