Personal tools
You are here: Home Events Abstract Archives 2001 On Compositional method and its limitations

On Compositional method and its limitations

Alexander Rabinovich Tel Aviv University 4pm, Tuesday 23 January 2001 Room 2511, JCMB, King's Buildings

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.

Document Actions