Detailed Information on Publication Record
2006
On Alternative Construction of LTL Tableau
ŠIMŠA, JiříBasic information
Original name
On Alternative Construction of LTL Tableau
Name in Czech
O alternativní konstrukci LTL tabla
Authors
Edition
Mikulov, Czech Republic, 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006), p. 222-229, 8 pp. 2006
Publisher
FI MU Report Series
Other information
Language
English
Type of outcome
Stať ve sborníku
Field of Study
10201 Computer sciences, information science, bioinformatics
Country of publisher
Czech Republic
Confidentiality degree
není předmětem státního či obchodního tajemství
Organization unit
Faculty of Informatics
Keywords in English
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.
In Czech
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í.
Links
| GA201/06/1338, research and development project |
| ||
| 1ET408050503, research and development project |
|