Here's one suggestion on how to do that. Specify the two semantics, say, by formulas CoarseSpec and FineSpec. Then define a mapping that computes the "coarse" state from the "fine" state, by restricting to rounds that all processes have already executed, and prove that for any fine-grained execution the result of the mapping is a coarse-grained execution. To be a little more concrete, let's assume your coarse-grained spec looks something like this. --- MODULE Coarse --- CONSTANT Proc \* the processes of the algorithm VARIABLE x \* the local states of each process Init == x = [p \in Proc |-> init(p)] \* initialize every process Next == x' = [p \in Proc |-> f(x,p)] \* all processes execute in lock-step Spec == Init /\ [][Next]_x \* ignoring liveness for simplicity ===== Fine-grained executions are specified by interleaving the processes. In order to simplify the statement of the relation between the two semantics, let's record for every process the history of its past states. (In practice, you probably want to introduce a history variable separate from the "real" specification.) --- MODULE Fine --- CONSTANT Proc VARIABLE y Init == y = [p \in Proc |-> << ... >>] \* singleton sequence containing initial state Next == \E p \in Proc : y' = [y EXCEPT ![p] = Append(@, ...)] \* process p moves and records its new state Spec == Init /\ [][Next]_y (* Now recover the abstract state for the last round that all processes executed. Note that the state of the fine-grained spec may need to be more detailed: the operator g (not defined here) retrieves the abstract state of process p. *) Min(S) == CHOOSE n \in S : \A m \in S : n <= m abs == LET n == Min( {Len[y][p] : p \in Proc} ) IN [p \in Proc |-> g(y[p][n], p)] C == INSTANCE Coarse WITH x <- abs THEOREM Spec => C!Spec ===== Does this make sense? Stephan |