Publication details
A Time
-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties
| Basic information | |
|---|---|
| Original title: | A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties |
| Authors: | Jiří Barnat, Luboš Brim, Petr Ročkai |
| Further information | |
|---|---|
| Citation: | BARNAT, Jiří - BRIM, Luboš - ROČKAI, Petr. A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties. In Formal Methods and Software Engineering. Germany : Springer Berlin / Heidelberg, 2009. ISBN 978-3-642-10372-8, pp. 407-425. 2009, Rio de Janeiro. |
| Original language: | English |
| Field: | Informatika |
| Type: | Article in Proceedings |
| Keywords: | on-the-fly; parallel; LTL Model Checking |
One of the most important open problems of parallel LTL model-checking is to design an on-the-fly scalable parallel algorithm with linear time complexity. Such an algorithm would give the optimality we have in sequential LTL model-checking. In this paper we give a partial solution to the problem. We propose an algorithm that has the required properties for a very rich subset of LTL properties, namely those expressible by weak Buchi automata.
Related projects:
- Techniques for automatic verification and validation of software nad hardware systems
- Realistic application of formal methods in component systems
- Highly Parallel and Distributed Computing Systems
- Verification and Analysis of Large-Scale Computer Systems
- Automated formal verification using modern hardware
