Branching Pomsets for Choreographies
From MaRDI portal
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.
Cites work
- A core model for choreographic programming
- Deadlock-freedom-by-design, multiparty asynchronous global programming
- Event structure semantics for multiparty sessions
- Introduction to bisimulation and coinduction
- Modeling concurrency with partial orders
- Multiparty Asynchronous Session Types
- Multiparty asynchronous session types
- Process algebra with action dependencies
- Realisability of pomsets
- Realizability and verification of MSC graphs
This page was built for publication: Branching Pomsets for Choreographies
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6122640)
