2006
On Alternative Construction of LTL Tableau
ŠIMŠA, JiříZákladní údaje
Originální název
On Alternative Construction of LTL Tableau
Název česky
O alternativní konstrukci LTL tabla
Autoři
Vydání
Mikulov, Czech Republic, 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006), od s. 222-229, 8 s. 2006
Nakladatel
FI MU Report Series
Další údaje
Jazyk
angličtina
Typ výsledku
Stať ve sborníku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Česká republika
Utajení
není předmětem státního či obchodního tajemství
Organizační jednotka
Fakulta informatiky
Klíčová slova anglicky
model checking; linear temporal logic; tableau construction
Změněno: 7. 12. 2006 12:13, Mgr. Jiří Šimša
V originále
Linear Temporal Logic (LTL) is a well established and extensively studied formalism in the field of formal verification. In certain applications of LTL, such as model-checking, it is convenient to identify a formula of LTL with an automata that accepts precisely the inputs that satisfy the formula. In this paper, we adopt this, automata-theoretic, approach and present a construction of such an automata. Unlike other existing constructions, our construction is based on the idea of iterative formula unfolding and normalization.
Česky
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í.
Návaznosti
| GA201/06/1338, projekt VaV |
| ||
| 1ET408050503, projekt VaV |
|