Global vs. local model checking: a comparison of verification techniques for infinite state systems
Tobias Schuele, Klaus Schneider · 2004
Global and local model checking procedures follow rad-ically different paradigms: while global approaches are based on fixpoint computation, local approaches are re-lated to deduction and induction. For the verification of fi-nite state systems, this may result in different runtimes. For the verification of infinite state systems, however, the differ-ences are far more important. Since most problems are un-decidable 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 µ-calculus properties of infinite state systems. In particular, we show how they can benefit from each other and present appropri-ate extensions. 1.