Branching Pomsets for Choreographies

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 operational semantics.