论文标题
编舞
Branching Pomsets for Choreographies
论文作者
论文摘要
编舞语言描述了一组代理之间可能的相互作用序列。典型的模型基于发送和接收操作的语言或自动机。 Pomset通过在这些动作上使用部分顺序，而不明确地交织并发动作来提供更紧凑的替代方案。但是，Pomsets不提供选择的紧凑表示。例如，如果代理商爱丽丝（Alice）可以向鲍勃（Bob）发送两次可能的两次消息之一，则需要一组2 * 2 * 2个不同的pomsets来表示爱丽丝行为的所有可能分支。本文提出了一个名为Branching Pomsets的Pomset的扩展，其分支结构可以使用2 + 2 + 2订购的动作代表爱丽丝的行为。我们将编码编码为分支机构，并表明编码编排的Pomset语义与其操作语义是偶然的。
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.
