Relating Hierarchy of Linear Temporal Properties to Model Checking
by
Ivana Černá,
Radek Pelánek,
April 2003, 18 pages.
FIMU-RS-2003-03.
Available as Postscript,
PDF.
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 Buchi, co-Buchi, and Streett acceptance condition and in
terms of Until-Release alternation hierarchy. Afterwards, we analyse the complex
ity
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.