PELÁNEK, Radek. LTL Hierarchies and Model Checking. In Proceedings of the Eight ESSLLI Student Session. Wien: TU Wien, 2003, p. 245-254, 9 pp.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name LTL Hierarchies and Model Checking
Authors PELÁNEK, Radek (203 Czech Republic, guarantor).
Edition Wien, Proceedings of the Eight ESSLLI Student Session, p. 245-254, 9 pp. 2003.
Publisher TU Wien
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Austria
Confidentiality degree is not subject to a state or trade secret
RIV identification code RIV/00216224:14330/03:00008596
Organization unit Faculty of Informatics
Keywords in English LTL; model checking
Tags LTL, Model checking
Tags International impact, Reviewed
Changed by Changed by: doc. Mgr. Radek Pelánek, Ph.D., učo 4297. Changed: 21/11/2006 14:02.
Abstract
We propose a new hierarchy of LTL formulas based on alternations of Until and Release operators and show that it is more relevant to model checking then previously studied hierarchies. Moreover, we study practically used formulas and conclude that in most cases it is possible to use specialized algorithms which are more efficient then general algorithm for LTL model checking.
Links
GA201/03/0509, research and development projectName: Automatizovaná verifikace paralelních a distribuovaných systémů
Investor: Czech Science Foundation, Automated Verification of Parallel and Distributed Systems
MSM 143300001, plan (intention)Name: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministry of Education, Youth and Sports of the CR, Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing
PrintDisplayed: 25/4/2024 01:00