Compositionality and bisimulation: a negative result

In the last years there have been several attempts at defining new logics or at using existing ones to specify properties of reactive and concurrent systems. The gain of associating suitable logics, such as modal or temporal logics, to communicating systems is the possibility of using deductive methods to prove properties. To provide modularity in the specification and verification of concurrent systems the compositional denotation by logic assertions of concurrent systems, specified by a process algebra like CCS, becomes an important research issue.