A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties

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 B

• Type: Journal
• Year: 2009
• Where: ICFEM
• Authors: Jiri Barnat, Lubos Brim, Petr Rockai
• Keywords: ICFEM 2009, Ltl Model-checking, Parallel Ltl Model-checking, Scalable Parallel Algorithm, Software Engineering