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 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 15:30 | |||
14:00 30mTalk | Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms VMCAI | ||
14:30 30mTalk | Independence Abstractions and Models of Concurrency VMCAI | ||
15:00 30mTalk | Static Analysis of Communicating Process using Symbolic Transducers VMCAI Vincent Botbol CEA LIST + LIP6 Université Pierre & Marie Curie, Tristan Le Gall CEA LIST, Emmanuel Chailloux LIP6 - UPMC Media Attached File Attached |