Abstract of Paper

Relating Hierarchy of Temporal Properties to Model Checking
by Ivana Cerna and Radek Pelanek

Abstract:

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.