Behaviour of systems is described by formal languages: the sets of all sequences of actions. Regarding ion, alphabetic language homomorphisms are compute abstract behaviours. To avoid loss of t information when moving to the abstract bstracting homomorphisms have to satisfy a certain property called simplicity on the concrete t abstracted) behaviour. To be suitable for verification of so called cooperating systems, a modified type of satisfaction relation for system properties (approximate satisfaction) is considered. The well known state space explosion problem is tackled by a compositional method formalised by so called cooperation products of formal languages.