Klever

Current strategy for verification of process instances generated by EMG takes the state space as a cartesian product of instance states. It means that for proving safety now it is required to explore all diferrent combinations of instance states. Intuitively verification explores all different interleavings of parallel instances.
The first observation come from Partial Order Reduction methods (POR): if the process actions are independent (the result of two actions a||b does not depend on the order a;b or b;a) then we require to explore only one sequence (e.g. a;b).
Second observation comes from practice where most of the errors are not related to different interleaving but manifest itself on a sequence of actions inside one struct of handlers or between the structs of handlers known to be dependent (e.g. probe-open)

The task is to develop a new verification strategy that first of all will explore state space without interleavings except for process instances known to be depended. And only after that may consider interleavings.
Thus errors which are exposed without interleavings will be found first. Moreover, in case if we explored all state space without interleaving we are sure that the system is Safe under the assumption that all process instances that were not regarded as dependent are independent.

Known issues where state explosion takes place are 5c256d21, 214c97a12.