Bounded saturation based CTL model checking

Abstract

Formal verification is becoming a fundamental step of safety-critical and model-based software development. As part of the verification process, model checking is one of the current advanced techniques to analyse the behaviour of a system. In this paper, we examine how the combination of two advanced model checking algorithms - namely bounded saturation and saturation based structural model checking - can be used to verify systems. Our work is the first attempt to combine these approaches, and this way we are able to handle and examine complex or even infinite state systems.