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

• Authors: BARNAT Jiří; BRIM Luboš; ROČKAI Petr
• Year of publication: 2009
• Type: Article in Proceedings
• Conference: Formal Methods and Software Engineering
• MU Faculty or unit: Faculty of Informatics
• 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

• 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