The StateMate modelling language constructs covered in this paper are Activity charts, modelling the functional decomposition of a design into subunits called activities as well as the information flow between these, and Statecharts, modelling reactive behaviour using the well established approach of hierarchically organized state-machines. We strive for a verication approach which is compositional w.r.t. the decomposition of systems into subsystems. This will allow activities of “reasonable” complexity to be veried using symbolic model checking [5], [4], [19]. Larger activities will be veried on the basis of proof-systems relating properties of individual activities to properties of compound activities, using the well known assumption commitment paradigm [1], [21], [15]. A key topic for this paper is the construction of so called compositional models, which are “rich enough” to model the StateMate parallel composition by intersection of the innite traces generated by the components of the parallel composition. Roughly, compositional models have to provide room for padding arbitrary (but still “legal”) environment interactions into computations of a component. Alternatively, the construction of compositional models can be phrased as a requirement on the model to support a sufficiently rich class of observables for assumption-commitment style reasoning to be complete. In this sense, this paper derives the set of atomic propositions included as observables in the assumption- commitment style temporal logic supported by the verication tool.