Abstract

The compositional approach reduces the verification of a property $\varphi$ of a system $C(S_1,\dots,S_n)$ assembled from the components $S_1,\dots,S_n$ to the verification of other properties $\varphi_1,\dots, \varphi_n$ on the components of the system. There are two parameters here: (1) The specification language $L_{spec}$ in which properties are formulated. (2) The collection of operations $OP$ by which a complex system can be assembled from its components.

The ideal dream of compositionality (Composition Theorem) is to give an algorithm which for every formula $\varphi\in L_{spec}$ and every n-ary operator $C\in OP$ will construct formulas $\varphi_1,\dots, \varphi_n$ such that $C(S_1,\dots, S_n)$ satisfies $\varphi$ iff $S_1$ satisfies $\varphi_1$, $S_2$ satisfies $\varphi_2$, \dots and $S_n$ satisfies $\varphi_n$.

We will show that the composition theorem is realizable when the specification language $L_{spec}$ is the multi-modal logic and the set of operations $OP$ consists of a wide variety of product (``parallel composition'') operators. On the other hand, we will show if $L_{spec}$ can express ``there is a path such that all the nodes of the path have a property $p$'', then (even non-algorithmic version of) the composition theorem fails for very simple parallel operators.