Shuffling posets on trajectories
(technical report)

Distributed systems are becoming ever more important. However, designing and implementing them is difficult. The complexity resulting from concurrency and dependencies among agents makes the process error-prone and debugging non-trivial. As a consequence, much research has been dedicated to analysing communication patterns, or protocols, among sets of agents in distributed systems. Examples of such research goals are to show the presence or absence of certain safety properties in a given system, to automate such analysis, and to guarantee the presence of desirable properties by construction.

Part of this research deals with choreographies. Choreographies can be used as global specifications for asynchronously communicating agents, and contain certain safety properties by construction. As a drawback, choreographic languages typically have limitations on their expressiveness, since they rely on grammatical constructs for their safety properties, which exclude some communication patterns. We have recently shown that the shuffle on trajectories operator can be used to specify choreographies without compromising expressiveness [2]. Consequently, it could serve as a basis for more expressive choreographic languages.

Other recent work on choreographies includes the use of models featuring partial orders, such as event structures [1] and pomsets [6, 3], to represent and analyse the behaviour of choreographies. By using a partial order to explicitly capture causal dependencies between pairs of actions, these models avoid the exponential blowup from, e.g., parallel composition of finite state machines.

We aim to join these two lines of research by extending the shuffle on trajectories operator from words, i.e., totally ordered traces, and languages to partially ordered traces and sets thereof. In this paper, as a first step, we explore the application of the shuffle on trajectories operator to individual partially ordered sets, or posets. The main challenge is that the resulting behaviour cannot always be represented as one poset and may require a set of them. In particular, we give a characterisation of shuffles of posets which again yield an individual poset.

We recall the basic definitions from [2]. The shuffle on trajectories operator is a powerful variation of the traditional shuffle operator¹¹1In concurrency theory, the shuffle operator is also known as free interleaving, non-communication merge, or parallel composition., which adds a control trajectory (or a set thereof) to restrict the permitted orders of interleaving. This allows for fine-grained control over orderings when shuffling words or languages. The binary operator was defined — and its properties thoroughly studied — by Mateescu et al. [4]; a multiary variant was introduced slightly later [5].

When defined on words, the shuffle on trajectories takes $n$ words and a trajectory, which is a word over the alphabet $\{1,\ldots,n\}$. This trajectory specifies the exact order of interleaving of the shuffled words: in Figure 1, the trajectory 1221112112 specifies that the result should first take a symbol from the first word, then from the second, then again from the second and so on.

Formally, let $w_{1},\ldots,w_{n}$ be finite words over some alphabet and let $t$ be a finite word over the alphabet $\{1,\ldots,n\}$. Let $\varepsilon$ be the empty word. Then:

We note that $\shuffle^{n}_{t}(w_{1},\ldots,w_{n})$ is only defined if the number of occurrences of $i$ in $t$ precisely matches the length of $w_{i}$ for every $i$. We then say that $t$ fits $w_{i}$.

The shuffle on trajectories operator naturally generalises to languages: the shuffle of a number of languages on a set (i.e., a language) of trajectories is defined as the set of all valid shuffles of words in the languages for which the trajectory fits all the words. Formally:

As the operator’s arity is clear from its operands, we typically omit it.

Partially ordered sets, or posets for short, consist of a set of nodes $E$ (events), and a partial order²²2Recall that a partial order is reflexive, transitive and antisymmetric. $\leq$ defining dependencies between pairs of events — i.e., an event can only fire if all events preceding it in the partial order have already fired. We write $a<b$ to denote that $a\leq b$ and $a\neq b$. We write $a\geq b$ resp. $a>b$ to denote that $b\leq a$ resp. $b<a$. We write $a\not\gtrless b$ to denote that $a\not\leq b$ and $b\not\leq a$; we then say that $a$ and $b$ are concurrent. We occasionally write $E_{P},\leq_{P}$, $<_{P}$, $\geq_{P}$, $>_{P}$ and $\not\gtrless_{P}$ to specify that the set of events or relation belongs to poset $P$, but where this is clear from context we typically omit the subscript.

The behaviour (or language) of a poset $P$, written $L(P)$, is the set of all maximal traces, i.e., maximal sequences of its events, that abide by $\leq$. In this sense, posets can be considered a generalisation of words with concurrency: they feature a fixed set of symbols (events)³³3There is a difference between words and posets in the sense that the events in a poset must be unique, whereas a word may contain duplicate symbols. It would be more accurate to say that words generalise to labelled posets, or lposets, and from there to partially ordered multisets, or pomsets. However, in this paper we focus on posets, where all symbols are thus unique., but they can allow multiple orderings of them instead of only a single one. Concurrent events can happen in any order. Consequently, all traces obtained from a trace in $L(P)$ by swapping adjacent concurrent events must also be in $L(P)$. In fact, any trace in $L(P)$ can be obtained from any other trace in $L(P)$ in this fashion.

We note that the dependencies in a poset can also be observed in its set of traces. For example, if $a<b$ then $a$ will precede $b$ in every trace, and if $a\not\gtrless b$ then there will both be traces where $a$ precedes $b$ and traces where $b$ precedes $a$. Formally, we can extract the following relation $\leq_{L}$ from a set of traces $L\subseteq E^{*}$:

We then propose the following:

To model trajectories, which require duplicate symbols, we must also introduce labelled posets, or lposets. In these, every event is assigned a label, which is not necessarily unique. Its traces then use these labels instead of the events.

As a first step towards shuffling posets, we first reinterpret shuffles on words as posets. In other words: we consider the case where all posets, including the trajectory, are totally ordered and thus consist of a single trace. This is shown in Figure 3, which features the shuffle from Figure 1 interpreted as a poset. The traces ‘banana’ and ‘pear’ are present as totally ordered parts of the poset, and the trajectory adds additional dependencies between the two, as shown by the vertical (and diagonal) arrows.

Generalising this to arbitrary posets and lposets is not trivial, but we have some knowledge to assist us. Crucially, since we can determine the language of a poset, it must be so that the result of shuffling posets yields the same language as the shuffle of the languages of these posets, which is defined in Section 2:

If the result is an individual poset, by Proposition 1 it must then be:

For example, consider $\shuffle_{LP_{t_{1}}}(P_{1},P_{2})$, with $LP_{t_{1}}$, $P_{1}$ and $P_{2}$ as in Figure 2. $LP_{t_{1}}$ has traces 1121 and 1112, $P_{1}$ has traces $abcd$, $acbd$ and $cabd$, and $P_{2}$ has a single trace $e$. Shuffling these languages yields $L_{1}=\{abced,acbed,cabed,abcde,\allowbreak acbde,\allowbreak cabde\}$. From this we extract $\leq_{L_{1}}$, which contains all the dependencies present in $P_{1}$ and $P_{2}$ and, additionally, $a\leq_{L_{1}}e$, $b\leq_{L_{1}}e$ and $c\leq_{L_{1}}e$. This corresponds to poset $P_{r_{1}}$ in Figure 2, which indeed yields the language $L_{1}$.

However, now consider $\shuffle_{LP_{t_{2}}}(P_{1},P_{2})$, again as in Figure 2. $LP_{t_{2}}$ has traces 1211, 1121 and 1112, which yields $L_{2}=L_{1}\cup\{abecd,acebd,caebd\}$. From this we extract $\leq_{L_{2}}$, which still contains all the dependencies in $P_{1}$ and $P_{2}$, but otherwise only $a\leq_{L_{2}}e$: the traces $abecd$ and $acebd$ imply that $b$ and $c$ are concurrent with $e$. However, then the trace $aebcd$ should also be in $L_{2}$, which it is not. We can then conclude from Proposition 1 that there exists no poset $P$ such that $L(P)=L_{2}$. In fact, $L_{2}$ corresponds to a set of two posets, namely $P_{r_{2a}}$ and $P_{r_{2b}}$ in Figure 2.

We proceed by giving a characterisation of shuffles of posets for which the result corresponds to an individual poset. A key insight is that, if the result must correspond to an individual poset, then any two events which are concurrent in one of the operands of the shuffle must, in the resulting poset, have the same relation ($<$, $>$ or $\not\gtrless$) to any third event originating from another operand:

We can then group the events in every $P_{i}$ according to the reflexive and transitive closure of the concurrency relation $\not\gtrless_{P_{i}}$; two events which are related in this closure then belong to the same group. Note that, while the events in a group are partially ordered, the groups of every $P_{i}$ are, by construction, totally ordered. It follows from Lemma 1 that two events in the same group, even when not concurrent, must have the same relation to any event outside of their group in $P$. This in turn implies a similar condition on the trajectory lposet: any two $i$-labelled events in $LP_{t}$ that can match two events from the same group of $P_{i}$ must have the same relation to any $j$-labelled event in $LP_{t}$ (where $j$ is not necessarily unequal to $i$) that can match an event outside of their group.

Figure 4 shows $P_{r_{1}}$, corresponding to $\shuffle_{LP_{t_{1}}}(P_{1},P_{2})$, and $LP_{t_{1}}$ (from Figure 2), both restructured to show the groups of $P_{1}$ and $P_{2}$. This demonstrates an interesting parallel with Figure 3: both feature horizontal traces with additional arrows specifying dependencies between components of these traces. However, in Figure 3 the components consist of individual events, whereas in Figure 4 the components consist of posets. In this sense, shuffles resulting in individual posets generalise shuffles on traces.

Concluding, we can then characterise shuffles on posets which result in individual posets as those where the trajectory lposet is structured along the operand posets’ groups, as in Figure 4, possibly with dependencies between different operands’ groups.

Now that we have studied shuffles of posets resulting in individual posets, there are two evident avenues for future work: (1) shuffles of lposets, where one label may occur multiple times rather than just considering orderings of unique events and (2) shuffles of posets resulting in sets of posets and shuffles of sets of posets, where the main challenge may be to minimise the resulting number of posets.