Revisiting Resistance Speeds Up I/O Efficient LTL Model Checking

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