Compositional Model Checking

In model checking, we aim to efficiently compute if a process satisfies a property. As systems become larger, determining if a process satisfies a property becomes increasingly hard to do. Often, large systems consist of multiple smaller systems working in parallel. The compositional model checking technique, originally from H. R. Andersen [1], exploits this fact. In this presentation, we explain the compositional model checking technique for processes described by linear process equations, which are lists of condition-action-effect clauses, and properties described by modal equation systems, an equational variant of the modal mu-calculus. In short, compositional model checking consists of two alternating steps. In the first step, one of the process' components is removed from the process description and its behavior is incorporated into the property, yielding a new property to be checked on the remaining components. In the second step, this new property is reduced in complexity, if possible. After these two steps, the entire model checking problem is easier to solve. This can be repeated at liberty.