ŠIMŠA, Jiří. On Alternative Construction of LTL Tableau. In 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006). Mikulov, Czech Republic: FI MU Report Series, 2006, p. 222-229.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name On Alternative Construction of LTL Tableau
Name in Czech O alternativní konstrukci LTL tabla
Authors ŠIMŠA, Jiří.
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
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Czech Republic
Confidentiality degree is not subject to a state or trade secret
Organization unit Faculty of Informatics
Keywords in English model checking; linear temporal logic; tableau construction
Tags linear temporal logic, Model checking, tableau construction
Changed by Changed by: Mgr. Jiří Šimša, učo 60360. Changed: 7/12/2006 12:13.
Abstract
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.
Abstract (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 projectName: Automatizovaná verifikace softwaru
Investor: Czech Science Foundation, Automated software verification
1ET408050503, research and development projectName: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems
PrintDisplayed: 26/4/2024 18:35