Relating Hierarchy of Linear Temporal Properties to Model Checking

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F03%3A00024523" target="_blank" >RIV/00216224:14330/03:00024523 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
Relating Hierarchy of Linear Temporal Properties to Model Checking
Original language 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 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.
Czech name
Hierarchie lineárních temporálních vlastností a ověřování modelů
Czech description
Hierarchie vlastností byla zavedena v pracích Manny a Pnueliho. Hierarchie ukazuje na vztahy mezi jazykmi, topologií, automaty nad nekonečnými slovy a lineárními temporálními vlastnostmi. Článek poskytuje novou charakterizaci této hierarchie v termínechakceptačních podmínek automatů nad nekonečnými slovy. Dále ukazujeme souvislost mezi vyjádřitelností vlastnosti a složitostí jejího ověřování pro konečně stavové modely.

Project
<a href="/en/project/GA201%2F03%2F0509" target="_blank" >GA201/03/0509: Automated Verification of Parallel and Distributed Systems</a><br>
Continuities
Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year
2003
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)