Verification of Cooperating Systems - An Approach Based on Formal Languages
Peter Ochsenschläger, Jürgen Repp, Roland Rieke · 2000
Behaviour of systems is described by formal languages: the sets of all sequences of actions. Regarding abstraction, alphabetic language homomorphisms are used to compute abstract behaviours. To avoid loss of level, abstracting homomorphisms have to satisfy a certain property called simplicity on the concrete (i.e. not 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.