Partial model checking

A major obstacle in applying finite-state model checking to the verification of large systems is the combinatorial explosion of the state space arising when many loosely coupled parallel processes are considered. The problem also known as the state-explosion problem has been attacked from various sides. This paper presents a new approach based on partial model checking where parts of the concurrent system are gradually removed while transforming the specification accordingly. When the intermediate specifications constructed in this manner can be kept small, the state-explosion problem is avoided. Experimental results with a prototype implemented in Standard ML, shows that for Milner´s Scheduler-an often used benchmark-this approach improves on the published results on binary decision diagrams and is comparable to results obtained using generalized decision diagrams. Specifications are expressed in a variant of the modal μ-calculus