Relating Hierarchy of Temporal Properties to Model Checking

Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

ČERNÁ Ivana PELÁNEK Radek

Rok publikování 2003
Druh Článek ve sborníku
Konference Mathematical Foundations of Computer Science (MFCS 2003)
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Obor Informatika
Klíčová slova temporal logic; automata over infinite words; model checking
Popis 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
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.