Relating Hierarchy of Temporal Properties to Model Checking

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

Result language
angličtina
Original language name
Relating Hierarchy of 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 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
Czech name
—
Czech description
—

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ů

Article name in the collection
Mathematical Foundations of Computer Science (MFCS 2003)
ISBN
3-540-40671-9
ISSN
—
e-ISSN
—
Number of pages
10
Pages from-to
318-327
Publisher name
Springer-Verlag
Place of publication
Bratislava (Slovensko)
Event location
Bratislava
Event date
Jan 1, 2003
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—

Similar results(10)