ČERNÁ, Ivana a Radek PELÁNEK. Relating Hierarchy of Temporal Properties to Model Checking. In Mathematical Foundations of Computer Science (MFCS 2003). Bratislava (Slovensko): Springer-Verlag, 2003. s. 318-327, 10 s. ISBN 3-540-40671-9.
Další formáty:   BibTeX LaTeX RIS
Zá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
Originální 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
Štítky automata over infinite words, Model checking, temporal logic
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnila: prof. RNDr. Ivana Černá, CSc., učo 1419. Změněno: 8. 6. 2009 16:09.
Anotace
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 VaVNázev: Automatizovaná verifikace paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Standardní projekty
MSM 143300001, záměrNázev: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumné záměry
VytisknoutZobrazeno: 21. 2. 2020 17:06