Independence abstractions and models of concurrency

Abstract

Mathematical representations of concurrent systems rely on two fundamental notions: an atomic unit of behaviour called an event, and a constraint called independence which asserts that the order in which certain events occur does not affect the final configuration of the system. We apply abstract interpretation to study models of concurrency by treating events and independence as abstractions. Events arise as Boolean abstractions of traces. Independence is a parameter to an abstraction that adds certain permutations to a set of sequences of events. Our main result is that several models of concurrent system are a composition of an event abstraction and an independence specification. These models include Mazurkiewicz traces, pomsets, prime event structures, and transition systems with independence. These results establish the first connections between abstraction interpretation and event-based models of concurrency and show that there is a precise sense in which independence is a form of abstraction.