On Conditions for Modular Verification in Systems of Synchronising Components

Property preservation is investigated as an approach tomodular verification, leading to reduction of the property verificationtimefor formal models. For modelling purposes, formalisms withmulti-waysynchronisations are considered. For the modular verificationtechniqueto work, a specific type of synchronisation is required forwhich a necessary condition is identified. It is a requirement on thesemantics of theformalism, which is restricted to permit simultaneousexecution only of component moves that make reference to each other.