D 2003

Relating Hierarchy of Temporal Properties to Model Checking

ČERNÁ, Ivana and Radek PELÁNEK

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

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

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

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

Tags

International impact, Reviewed
Změněno: 8/6/2009 16:09, prof. RNDr. Ivana Černá, CSc.

Abstract

V originále

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

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