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 mutex relation, that can model these kind of cases. We discuss the soundness of this concept and show how it can be applied in the domain of Petri nets.