A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties
| Authors | |
|---|---|
| Year of publication | 2009 |
| Type | Article in Proceedings |
| Conference | Formal Methods and Software Engineering |
| MU Faculty or unit | |
| Citation | |
| Doi | http://dx.doi.org/10.1007/978-3-642-10373-5_21 |
| Field | Informatics |
| Keywords | on-the-fly; parallel; LTL Model Checking |
| Description | 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: |
|