Global vs. local model checking: a comparison of verification techniques for infinite state systems

Global and local model checking procedures follow radically different paradigms: while global approaches are based on fixpoint computation, local approaches are related to deduction and induction. For the verification finite state systems, this may result in different runtimes. For the verification of infinite state systems, however the differences are far more important. Since most problems are undecidable for such systems, it may be the case that one of the procedures does not terminate. In this paper we compare global and local procedures for model checking p-calculus properties of infinite state systems. In particular we show how they can benefit from each other and present appropriate extensions.