Shuffling posets on trajectories (technical report)

TL;DR

This paper investigates how the shuffle on trajectories operator can be applied to partially ordered sets (posets) in choreographies, aiming to enhance expressive power and understand the conditions under which shuffles preserve poset structure.

Contribution

It characterizes when shuffles of posets result in a single poset, advancing the theoretical understanding of concurrency modeling in choreographic languages.

Findings

Identifies conditions for shuffles of posets to produce a poset

Enhances the theoretical framework for modeling concurrent interactions

Supports more expressive choreographic language design

Abstract

Choreographies describe possible sequences of interactions among a set of agents. We aim to join two lines of research on choreographies: the use of the shuffle on trajectories operator to design more expressive choreographic languages, and the use of models featuring partial orders, to compactly represent concurrency between agents. Specifically, in this paper, we explore the application of the shuffle on trajectories operator to individual posets, and we give a characterisation of shuffles of posets which again yield an individual poset.