LTL Hierarchies and Model Checking

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.

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

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Austria

Confidentiality degree

není předmětem státního či obchodního tajemství

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

---

Abstract

V originále

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 project	Name: 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