While the concept of modules forming a synchronised statement is easy, there is a variety of different formalisms or specifications which approach it differently.

1 Asynchronous modules

A typical assumption in the terminology of automatons is, that two events never happen at the same time. If it is desired to execute two statements from two different modules at the same time, they thus need to be synchronised, which means, that they become a single event. The event can fire if the guards in both of those statements are true. Such a synchronisation is typically realised using the action labels, specified within the otherwise empty brackets before a statement. If several statement from different modules share a common action label, e.g. [arrival] and if their guards are all true at once, they can together fire a transition, realised by an ensemble of the updates.

2 Synchronous modules

If a network of modules is synchronised in its entirety by using the sync keyword in the class specification, it means that at any time step, each modules fires an action (these actions form together a single synchronised statement). Specifically, any subset of currently enabled statements (by their guards) can be executed at the same time. The subset is realised by non–deterministically choosing exactly a single statement from each module. A module, which should be idle at certain steps, should thus provide a statement without an update (called sometimes an epsilon action), as othewise a global deadlock would occur.

Let there be a network A of fully asynchronous modules, i.e. no sync keyword and no action labels. Let S be like A, but synchronised using sync in its class specification, and with an empty statement added to each module. See that transitions in S are a superset of these in A. Any transition possible in A can be realised in S by executing a single non--empty statement, synchronised only with empty statements from the other modules. At the same time S, as opposed to A, does not posess a mechanism which prevents more than a single non--empty statement to form a single event.

In other words, it can be said that A posesses a global lock, which takes care, that only an update from a single statement is realised at a given moment. In turn, S is deprived of such a lock.

Networks like A and S are on two opposite poles. A requires an explicit synchronisation to make given statements a single event, while S requires explicit guards to prevent given statements from becoming a single event.

Models that use A, possibly completed with synchronising action labels, are traditionally used in modelling environments like Prism. There is no problem, though, in specifying S in Prism: all statements should be given the same action label, and possibly some modules should be completed with null statements (the epsilon actions).

Models that start with S are popular when studying certain multi--agent system (MAS). A MAS can be seen as a loose set of automatons, and thus no global anti--synchronisation locks like in the case of A, yet empty statements may still allow for an (effectively) interleaved execution. The lack of such a lock can be advantageous simply because in real–life situations there is often no such a lock, and two events can happen at a time close enough to be regarded in practice as a single event. On the contrary, specifying a network not synchronised by default, i.e. which assumes such a global lock, may in specific situations lead to the lack of a carefully designed mechanism explicitly built-in into the model, which prevents a harmful synchronisation (instead of that global lock), and modelling some real-life device which prevents e.g. two trains from entering a single track. A special care may thus be needed, when interpreting/realising a system with a global anti--synchronisation locks: just disregarding that lock may lead to an incorrect physical implementation with harmful clashes.

3 Realising a global lock

A simple example: let there be a turnaround specified in a not globally synchronised MDP:

    class mdp;
   
    module train1 { 
        Z{W, E} location := W; 

        []  location == W -> location := E;
    };
    module train2 { 
        Z{W, E} location := E; 

        []  location == E -> location := W;
    };

If we would analyse a property of this network whether the two trains ever ride through the turnaround at the same time, the answer would be no: Train 1 passes through the turnaround always before or after Train 2. No problem, the global lock discussed provides that. In reality, though, a naive implementation of the model, i.e. only of what is explicitly given in the model source, would have the same property true.

While in this simple model the issue is obvious, and also it is easy to remember, that the global lock inherent to the model's class should be implemented as well, this may become more complex in larger, more complicated models, including the implementation of the global lock, which might be much more complex than needed. One of the advantages of using a model checker is to found out issues like that in the turnaround model and warn us, that we should redesign the model. We may choose a synchronous class just for that: to make the model checker help up in a precise design of all the anti-clash mechanisms required.

4 Action labels

So there are no for synchronisation labels in a synchronised network of modules. Yet, we can (and often do) label statements in such a case: by action labels. Statements with a common action label form a conceptual group (let us call one such group a). It is similar to statements with a common synchronisation label. The role of an action label is intuitive: only one action can be realised at a time step. For example, when transitions represented by a fire (together), no actions outside a can participate.

See the similarity of action labels to synchronisation labels: they both define a group which fires together. Yet, a synchronisation label provides synchronisation, a concept which can not be replaced merely by guards (but can sometimes be replaced by replacement `bulk' statements which joins several guards and updates). On the contrary, an action label limits possible synchronisation cases, being thus replacable by more restrictive guards. In fact, there is an alternative to action labels in a globally synchronised network: a protocol connects states to actions, these in turn can be made obligatory in guards.