Independence Abstractions and Models of Concurrency
Representations of concurrent systems rely on two fundamental notions: an atomic unit of behaviour called an event, and a property called independence asserting that certain events do not affect each other. We apply abstract interpretation to study models of concurrency by treating events and independence as abstractions. Events arise as Boolean abstractions of traces and independence leads to closure of behaviour under concurrent interleavings. Models of concurrent system such as Mazurkiewicz traces, pomsets, prime event structures, and transition systems with independence arise as abstractions that are complete in the abstract interpretation sense. Moreover, prime, algebraic domains, which are order-theoretic duals of prime event structures also arise as complete abstract domains. These results establish the first connections between complete abstractions and models of concurrency.
Sun 15 Jan
|14:00 - 14:30|
|14:30 - 15:00|
|15:00 - 15:30|
Vincent BotbolCEA LIST + LIP6 Université Pierre & Marie Curie, Tristan Le GallCEA LIST, Emmanuel ChaillouxLIP6 - UPMCMedia Attached File Attached