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

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.

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
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:	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