Branching Pomsets for Choreographies
Luc Edixhoven (Open University (Heerlen), CWI (Amsterdam),, Netherlands), Sung-Shik Jongmans (Open University (Heerlen), CWI, (Amsterdam), Netherlands), Jos\'e Proen\c{c}a (CISTER, ISEP, Polytechnic, Institute of Porto, Portugal), Guillermina Cledou (HASLab, INESC TEC and

TL;DR
This paper introduces branching pomsets, an extension of pomsets that efficiently represent choices in choreographies, and demonstrates their bisimilarity to operational semantics.
Contribution
It proposes branching pomsets to compactly encode choices in choreographies, improving over traditional pomsets.
Findings
Branching pomsets can represent choices with fewer elements.
Encoded choreographies are bisimilar to their operational semantics.
The approach simplifies the representation of concurrent interactions.
Abstract
Choreographic languages describe possible sequences of interactions among a set of agents. Typical models are based on languages or automata over sending and receiving actions. Pomsets provide a more compact alternative by using a partial order over these actions and by not making explicit the possible interleaving of concurrent actions. However, pomsets offer no compact representation of choices. For example, if an agent Alice can send one of two possible messages to Bob three times, one would need a set of 2 * 2 * 2 distinct pomsets to represent all possible branches of Alice's behaviour. This paper proposes an extension of pomsets, named branching pomsets, with a branching structure that can represent Alice's behaviour using 2 + 2 + 2 ordered actions. We encode choreographies as branching pomsets and show that the pomset semantics of the encoded choreographies are bisimilar to their…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
