Types & Choreographies
Realisability of Branching Pomsets
Luc Edixhoven, Sung-Shik Jongmans
Presenter: Luc Edixhoven
Session Chair: EmÃlio Tuosto
A communication protocol is realisable if it can be faithfully implemented in a distributed fashion by communicating agents. Pomsets offer a way to compactly represent concurrency in communication protocols and have been recently used for the purpose of realisability analysis. In this paper we focus on the recently introduced branching pomsets, which also compactly represent choices. We define well-formedness conditions on branching pomsets, inspired by multiparty session types, and we prove that the well-formedness of a branching pomset is a sufficient condition for the realisability of the represented communication protocol.