Search space partition and case basis exploration for reducing model checking complexity

Abstract

The main disadvantage of model checking is the state explosion problem that can occur if the system being verified has many asynchronous components. Many approaches have been proposed to deal with this challenge. This paper extends an approach that suggests combining static analysis and partition of model checking tasks into different cases for reducing the complexity of model checking and introduces algorithms and a tool for the static analysis. This extended approach and the tool are then applied to models of known authentication protocols and operating procedures, which shows that the approach and the tool could have a wide range of applications.