Interval Traces with Mutex Relation

Interval traces can model sophisticated behaviours of concurrent systems under the assumptions that all observations/system runs are represented by interval orders and simultaneity is not necessarily transitive. What they cannot model is the case when a and b are considered independent, interleavings ab and ba are deemed equivalent, but simultaneous execution of a and b is disallowed. We introduce a new kind of interval traces, incorporating a …