Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:On Compositional Method and its Limitations
Authors: Alexander Rabinovich
Date:Jan 2001
The compositional approach reduces the verification of a property P of a system C(S1, . . .,Sn) assembled from the components S1, . . ., Sn to the verification of other properties P1, . . ., Pn on the components of the system. There are two parameters here: (1) The specification language 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 P of SPEC and every n-ary operator C in OP will construct formulas P1, . . .,Pn such that C(S1, . . . , Sn) satisfies P iff S1 satisfies P1, S2 satisfies P2, . . . and Sn satisfies Pn. We will show that the composition theorem is realizable when the specification language 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 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.
2001 by The University of Edinburgh. All Rights Reserved
Links To Paper
No links available
Bibtex format
author = { Alexander Rabinovich },
title = {On Compositional Method and its Limitations},
year = 2001,
month = {Jan},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh