Publication details
Relating Hierarchy of Linear Temporal Properties to Model Checking
| Basic information | |
|---|---|
| Original title: | Relating Hierarchy of Linear Temporal Properties to Model Checking |
| Authors: | Ivana Černá, Radek Pelánek |
| Further information | |
|---|---|
| Citation: | ČERNÁ, Ivana  - PELÁNEK, Radek. Relating Hierarchy of Linear Temporal Properties to Model Checking. Brno, Czech Republic : FI MU, 2003. Technical report FIMU-RS-2003-03. |
| Original language: | English |
| Field: | Informatika |
| WWW: |  http://www.fi.muni.cz/reports/2003/abstract/FIMU-RS-2003-03.shtml |
| Type: | R&D Presentation |
| Keywords: | temporal logic; automata over infinite words; hierarchy of properties |
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.
Related projects:
- Automated Verification of Parallel and Distributed Systems
- Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing
