Relating Hierarchy of Temporal Properties to Model Checking

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

ČERNÁ Ivana PELÁNEK Radek

Year of publication 2003
Type Article in Proceedings
Conference Mathematical Foundations of Computer Science (MFCS 2003)
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords temporal logic; automata over infinite words; model checking
Description 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
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.