Revisiting Resistance Speeds Up I/O Efficient LTL Model Checking

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š ŠIMEČEK Pavel WEBER Michael
Year of publication	2008
Type	Article in Proceedings
Conference	Tools and Algorithms for the Construction and Analysis of Systems
MU Faculty or unit	Faculty of Informatics
Citation
Field	Informatics
Keywords	I/O efficient; accepting cycle detection; revisiting resistance
Description	Revisiting resistance graph algorithms are those, whose correctness is not vulnerable to repeated edge exploration. Revisiting resistant I/O efficient graph algorithms exhibit considerable speed-up in practice in comparison to non-revisiting resistant algorithms. In the paper we present a new revisiting resistant I/O efficient LTL model checking algorithm. We analyze its theoretical I/O complexity and we experimentally compare its performance to already existing I/O efficient LTL model checking algorithms.
Related projects:	Techniques for automatic verification and validation of software nad hardware systems Realistic application of formal methods in component systems Institute for Theoretical Computer Science Highly Parallel and Distributed Computing Systems Automated software verification