2003
Relating Hierarchy of Temporal Properties to Model Checking
ČERNÁ, Ivana a Radek PELÁNEKZákladní údaje
Originální název
Relating Hierarchy of Temporal Properties to Model Checking
Autoři
ČERNÁ, Ivana (203 Česká republika, garant) a Radek PELÁNEK (203 Česká republika)
Vydání
Bratislava (Slovensko), Mathematical Foundations of Computer Science (MFCS 2003), od s. 318-327, 10 s. 2003
Nakladatel
Springer-Verlag
Další údaje
Jazyk
angličtina
Typ výsledku
Stať ve sborníku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Německo
Utajení
není předmětem státního či obchodního tajemství
Kód RIV
RIV/00216224:14330/03:00008590
Organizační jednotka
Fakulta informatiky
ISBN
3-540-40671-9
UT WoS
000185947800026
Klíčová slova anglicky
temporal logic; automata over infinite words; model checking
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 8. 6. 2009 16:09, prof. RNDr. Ivana Černá, CSc.
Anotace
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
Návaznosti
| GA201/03/0509, projekt VaV |
| ||
| MSM 143300001, záměr |
|