ČERNÁ, Ivana and Radek PELÁNEK. Relating Hierarchy of Temporal Properties to Model Checking. In Mathematical Foundations of Computer Science (MFCS 2003). Bratislava (Slovensko): Springer-Verlag, 2003. p. 318-327. ISBN 3-540-40671-9.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Relating Hierarchy of Temporal Properties to Model Checking
Authors ČERNÁ, Ivana (203 Czech Republic, guarantor) and Radek PELÁNEK (203 Czech Republic).
Edition Bratislava (Slovensko), Mathematical Foundations of Computer Science (MFCS 2003), p. 318-327, 10 pp. 2003.
Publisher Springer-Verlag
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Germany
Confidentiality degree is not subject to a state or trade secret
RIV identification code RIV/00216224:14330/03:00008590
Organization unit Faculty of Informatics
ISBN 3-540-40671-9
UT WoS 000185947800026
Keywords in English temporal logic; automata over infinite words; model checking
Tags automata over infinite words, Model checking, temporal logic
Tags International impact, Reviewed
Changed by Changed by: prof. RNDr. Ivana Černá, CSc., učo 1419. Changed: 8. 6. 2009 16:09.
The hierarchy of properties as overviewed by Manna and Pnueli relates language, topology, $\omega$-automata, and linear temporal logic classifications of properties. We provide new characterisations of this hierarchy in terms of automata with B\"uchi, co-B\"uchi, and Streett acceptance condition and in terms of Until-Release hierarchies. Afterwards, we analyse the complexity of the model checking problem for particular classes of the hierarchy and thanks to the new characterisations we identify those linear time temporal properties for which the model checking problem can be solved more efficiently than in the general case
GA201/03/0509, research and development projectName: Automatizovaná verifikace paralelních a distribuovaných systémů
Investor: Czech Science Foundation, Standard Projects
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, Research Intents
PrintDisplayed: 2. 8. 2021 23:20