Other formats:
BibTeX
LaTeX
RIS
@inproceedings{489732,
author = {Černá, Ivana and Pelánek, Radek},
address = {Bratislava (Slovensko)},
booktitle = {Mathematical Foundations of Computer Science (MFCS 2003)},
keywords = {temporal logic; automata over infinite words; model checking},
language = {eng},
location = {Bratislava (Slovensko)},
isbn = {3-540-40671-9},
pages = {318-327},
publisher = {Springer-Verlag},
title = {Relating Hierarchy of Temporal Properties to Model Checking},
year = {2003}
}
TY - JOUR
ID - 489732
AU - Černá, Ivana - Pelánek, Radek
PY - 2003
TI - Relating Hierarchy of Temporal Properties to Model Checking
PB - Springer-Verlag
CY - Bratislava (Slovensko)
SN - 3540406719
KW - temporal logic
KW - automata over infinite words
KW - model checking
N2 - 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
ER -
ČERNÁ, Ivana and Radek PELÁNEK. Relating Hierarchy of Temporal Properties to Model Checking. In \textit{Mathematical Foundations of Computer Science (MFCS 2003)}. Bratislava (Slovensko): Springer-Verlag. p.~318-327. ISBN~3-540-40671-9. 2003.
|
