Partial Model Checking with ROBDDs

This paper introduces a technique for localizing model checking of concurrent state-based systems. The technique, called partial model checking, isfully automatic and performs model checking by gradually specializing the specification with respect to the concurrent components one by one,computing a `concurrent weakest precondition.' Specifications are invariance properties and the concurrent components sets of transitions. Bothare expressed as predicates represented by Reduced Ordered Binary Decision Diagrams (ROBDDs). The self-reducing properties of ROBDDs areimportant for the success of the technique. We describe experimental results obtained on four different examples.