key: cord-0060871-mghjdqfd
authors: Fahrenberg, Uli; Johansen, Christian; Struth, Georg; Bahadur Thapa, Ratan
title: Generating Posets Beyond N
date: 2020-04-01
journal: Relational and Algebraic Methods in Computer Science
DOI: 10.1007/978-3-030-43520-2_6
sha: df41a035e8bbb69db74a21ebb500515608ebada4
doc_id: 60871
cord_uid: mghjdqfd

We introduce iposets—posets with interfaces—equipped with a novel gluing composition along interfaces and the standard parallel composition. We study their basic algebraic properties as well as the hierarchy of gluing-parallel posets generated from singletons by finitary applications of the two compositions. We show that not only series-parallel posets, but also interval orders, which seem more interesting for modelling concurrent and distributed systems, can be generated, but not all posets. Generating posets is also important for constructing free algebras for concurrent semirings and Kleene algebras that allow compositional reasoning about such systems.

This work is inspired by Tony Hoare's programme of building graph models of concurrent Kleene algebra (CKA) [14] for real-world applications. CKA extends the sequential compositions, nondeterministic choices and unbounded finite iterations of imperative programs modelled by Kleene algebra into concurrency, adding operations of parallel composition and iteration, and a weak interchange law for the sequential-parallel interaction. Such algebras have a long history in concurrency theory, dating back at least to Winkowski [38] . Commutative Kleene algebra-the parallel part of CKA-has been investigated by Pilling and Conway [3] . A double semiring with weak interchange-CKA without iteration-has been introduced by Gischer [10] ; its free algebras have been studied by Bloom and Esik [1] . CKA, like Gischer's concurrent semiring, has both interleaving and true concurrency models, that is, shuffle as well as pomset languages. Series-parallel pomset languages, which are generated from singletons by finitary applications of sequential and parallel compositions, form free algebras in this class [21, 25] (at least when parallel iteration is ignored). The inherent compositionality of algebra is thus balanced by the generative properties of this model. Yet despite this and other theoretical work, applications of CKA remain rare.

One reason is that series-parallel pomsets are not expressive enough for many real-world applications: even simple producer-consumer examples cannot be modelled [27] . Tests, which are needed for the control structure of concurrent programs, and assertions are hard to capture in models of CKA (see [19] and its discussion in [20] ). Finally, it remains unclear how modal operators could be defined over graph models akin to pomset languages, which is desirable for concurrent dynamic algebras and logics beyond alternating nondeterminism [9, 31] .

A natural approach to generating more expressive pomset languages is to "cut across" pomsets in more general ways when (de)composing them. This can be achieved by (de)composing along interfaces, and this idea can be traced back again to Winkowski [38] ; see also [4, 6, 28] for interface-based compositions of graphs and posets, or [15, 29, 30] for recent interface-based graph models for CKA. As a side effect, interfaces may yield notions of tests, assertions or modalities. When they consist of events, cutting across them presumes that they extend in time and thus form intervals. Interval orders [7, 37] of events with duration have been applied widely in partial order semantics of concurrent and distributed systems [17, 22, 23, [33] [34] [35] [36] and the verification of weak memory models [13] , yet generating them remains an open problem [18] .

Our main contribution lies in a new class and algebra of posets with interfaces (iposets) based on these ideas. We introduce a new gluing composition that acts like standard serial po(m)set composition outside of interfaces, yet glues together interface events, thus composing events that did not end in one component with those that did not start in the other one. Our definitions are categorical so that isomorphism classes of posets are considered ab initio. Their decoration with labels is then routine, so that we may focus on posets instead of pomsets.

Our technical results concern the hierarchy of gluing-parallel posets generated by finitary applications of this gluing composition and the standard parallel composition of po(m)sets, starting from singleton iposets. 1 Thus all series-parallel pomsets can be generated, but also all interval orders are captured at the second alternation level of the hierarchy. Beyond that, we show that the gluingparallel hierarchy does not collapse and that posets with certain zigzag-shaped induced subposets are excluded. A precise characterisation of the generated (i) posets remains open. Series-parallel posets, by comparison, exclude precisely those posets with induced N-shaped subposets; interval orders those with induced subposets 2+2, which makes the two classes incomparable. Iposets thus retain the pleasant compositionality properties of series-parallel pomsets and the wide applicability of interval orders in concurrency and distributed computing.

In addition, we establish a bijection between isomorphism classes of interval orders and certain equivalence classes of interval sequences [33] , and we study the basic algebraic properties of iposets, including weak interchange laws and a Levi lemma. The relationship between gluing-parallel ipo(m)set languages and CKA is left for another article.

A poset (P, ≤ P ) is a set P equipped with a partial order ≤ P ; a reflexive, transitive, antisymmetric relation on P (for which we often write ≤). A morphism of posets P and Q is an order-preserving function f : P → Q, that is, x ≤ P y implies f (x) ≤ Q f (y). Posets and their morphisms define the category Pos.

A poset is linear if each pair of elements is comparable with respect to its order. We write < for the strict part of ≤. We write [n], for n ≥ 1, for the discrete

The isomorphisms in Pos are order bijections: bijective functions f : P → Q for which x ≤ P y ⇔ f (x) ≤ Q f (y). We write P ∼ = Q if posets P and Q are isomorphic. We generally consider posets up-to isomorphism and assume that all posets are finite.

Concurrency theory often considers (isomorphism classes of) posets with points labelled by letters from some alphabet, which represent actions of some concurrent system. These are known as partial words or pomsets. As we are mainly interested in structural aspects of concurrency, we ignore such labels.

Series-parallel posets form a well investigated class that can be generated from the singleton poset by finitary applications of two compositions. Their labelled variants generalise rational languages into concurrency. For arbitrary posets, these compositions are defined as follows. Definition 1. Let P 1 = (P 1 , ≤ 1 ) and P 2 = (P 2 , ≤ 2 ) be posets.

1. Their serial composition is the poset P 1 ; P 2 = (P 1 P 2 , ≤ 1 ∪ ≤ 2 ∪ P 1 × P 2 ). 2. Their parallel composition is the poset P 1 ⊗ P 2 = (P 1 P 2 , ≤ 1 ∪ ≤ 2 ).

Here, means disjoint union (coproduct) of sets. We generalise serial composition to a gluing composition in Sect. 4 

Also note that parallel composition is the coproduct in Pos, hence ⊗ is also defined for morphisms.

By definition, a poset is series-parallel (an sp-poset) if it is either empty or can be obtained from the singleton poset by applying the serial and parallel compositions a finite number of times. It is well known [12, 32] Sp-po(m)sets form double monoids with respect to serial and parallel composition, and with the empty poset as shared unit-in fact the free algebras in this class. Compositionality of the recursive definition of sp-po(m)sets is thus reflected by the compositionality of their algebraic properties, which is often considered desirable for concurrent systems [36] . Yet sp-posets are, in fact, too compositional for many applications: even simple consumer-producer problems inevitably generate N's [27] , as shown in Fig. 1 that contains the N spanned by c 1 , c 2 , p 2 , and p 3 as an induced subposet among others.

Interval orders [7, 37] form another class of posets that are ubiquitous in concurrent and distributed computing. Intuitively, they are isomorphic to sets of intervals on the real line that are ordered whenever they do not overlap.

An interval order is a relational structure (P, <) with < irreflexive such that w < y and x < z imply w < z or x < y, for all w, x, y, z ∈ P .

Transitivity of < follows. An alternative geometric characterisation is that interval orders are precisely those posets that do not contain the induced subposet 2+2 = · / / · · / / · . The intuition is captured by Fishburn's theorem [7] , which implies that a finite poset P is an interval order if and only if it has an interval representation: a pair of functions b, e : P → Q into some linear order (Q, < Q ) such that b(x) < Q e(x) for all x ∈ P , and x < P y iff e(x) < Q b(y) for all x, y ∈ P . By the first condition, pairs (b(x), e(x)) correspond to intervals

We write ρ I (P ) for the set of interval representations of P . Each representation can be rearranged so that all endpoints of intervals are distinct ( [11] , Lemma 1.5). We henceforth assume that all interval presentations have this property. It then holds that |Q| = 2|P |, and we can fix Q as the target type of any interval representation of P .

Finally, with relation on the set of maximal antichains of poset P given by

it is known that P is an interval order if and only if is a strict linear order [8] .

Interval orders occur implicitly in the ST-traces of Petri nets [33] . In a pure order-theoretic setting, these are interval sequences, that is, sequences of b(x) and e(x), with x from some finite set P , in which each b(x) occurs exactly once and each e(x) at most once and only after the corresponding b(x). An interval sequence is closed if each e(x) occurs exactly once [33, 36] . An interval trace [18] is an equivalence class of interval sequences modulo the relations

for all x, y ∈ P . We write ≈ * for the congruence generated by ≈ on interval sequences. We identify interval sequences and interval traces with the Hasse diagrams of their linear orders over Q.

Proof. Trivial.

We write σ (b,e) (P ) for the interval sequence of interval order P and (b, e) ∈ ρ I (P ), and Σ(P ) for the set of all interval sequences of interval representations of P .

and, for all v, w ∈ P , v < P w ⇔ e(v) < P b(w) still holds. In addition, (b , e) generates σ . An analogous result for σ = σ 1 e(x)e(y)σ 2 and σ = σ 1 e(y)e(x)σ 2 holds by opposition. The result for ≈ * then follows by a simple induction.

Let P be an interval order. If (b, e), (b , e ) ∈ ρ I (P ) assign b and e to elements of P in interval sequences, then σ (b,e) (P ) ≈ * σ (b ,e ) (P ).

Proof. Let ≺ 1 and ≺ 2 be the orderings of the interval sequences for (b, e) and

in ≺ 1 and ≺ 2 and, by opposition, there is no e(z) in ≺ 1 or ≺ 2 between the positions of b(x) in ≺ 1 and ≺ 2 . But this means that the positions of e(x) and b(x) can be rearranged by ≈ * .

Proof. By Lemmas 4 and 5, and by properties of interval representations. 

We write P min (P max ) for the sets of minimal (maximal) elements of P .

Injection s : [n] → P represents the source interface of P and t : [m] → P its target interface. We write (s, P, t) : n → m for the iposet s : [n] → P ← [m] : t. Figure 2 shows some examples of iposets. Elements of source and target interfaces are depicted as filled half-circles to indicate the unfinished nature of the events they represent.

Next we define a sequential gluing composition on iposets whose interfaces agree and we adapt the standard parallel composition of posets to iposets.

Parallel composition of iposets thus puts components "side by side": it is the disjoint union of posets and interfaces. Gluing composition puts iposets "one after the other", P 1 before P 2 , but glues their interfaces together (and adds arrows from all points in P 1 that are not in its target interface to all points in P 2 that are not in its source interface). As explained in the introduction, it thus glues events which did not end in P 1 with those that did not start in P 2 . Figures 3  and 4 show examples. The filled half-circles in source and target interfaces are glued to unfilled circles in these diagrams. We define identity iposets id n = (id, [n], id) : n → n, for n ≥ 0. For convenience, we generalise this notation to other discrete posets with interfaces: for k, ≤ n, we write k id n for the iposet (f n k , [n], f n ) : k → , where f n k : [k] → [n] is the (identity) injection x → x (similarly for f n ). Hence id n = n id n n .

Iposets form a small category with natural numbers as objects, iposets (s, P, t) : n → m as morphisms, as composition, and identities id n .

Checking the associativity and unit laws is routine. The following example shows that gluing composition is not commutative, as expected: Perhaps more unexpectedly, parallel composition need not be commutative, as the namings of interfaces in P ⊗ Q may differ from those in Q ⊗ P . One can of course rename interfaces using symmetries: iposets (s, [n], t) : n → n with s and t bijective. Yet Fig. 5 shows two parallel compositions where renaming of interfaces and gluing with another iposet yields non-isomorphic posets.

The iposets P : n → m, Q : k → are mapped by ⊗ to P ⊗Q : n+k → m+ , which has the signature of a tensor on the small category of Proposition 9. Yet gluing and parallel composition need not satisfy an interchange law:

Hence ⊗ is not a tensor, and iposets do not form a (strict) monoidal category (let alone a PROP). This situation differs from gluing compositions where interfaces of iposets are defined by all minimal and maximal elements [38] , and also from sequential compositions with interfaces similar to ours but where interfaces disappear and no other order is induced [6, 28] . All of these give rise to PROPs. Instead of the interchange law above, we will state a lax interchange law in Proposition 12; the precise categorical relation between gluing and parallel composition is left open for future work. What we will need here is that iposets with ⊗ form a graded monoid over N × N, i.e., that there is a grading function (a monoid morphism) from iposets into N × N. The grading function maps an iposet P : n → m to the tuple (n, m), with addition on tuples defined component-wise. The proof is routine.

A morphism of iposets is a commuting diagram

where ν and μ are strictly order preserving with respect to < N and f is an order morphism between P and P . Intuitively, iposet morphisms are thus order morphisms that also preserve interfaces and their order in N. We write iPos for the so-defined category. An iposet morphism (ν, f, μ) is an isomorphism if ν, f and μ are order isomorphisms. Hence n = n , m = m , ν = id : n → n, and μ = id : m → m in the diagram above. In particular, iposets related by a symmetry (s, [n], t) : n → n need not be isomorphic. We write P ∼ = Q if there exists an isomorphism ϕ : P → Q. The following lemma shows ⊗ and respect isomorphisms. Lemma 11. Let P, P , Q, Q be iposets. Then P ∼ = P and Q ∼ = Q imply P ⊗ Q ∼ = P ⊗ Q and P Q ∼ = P Q .

Proof. Let ϕ : P → P and ψ : Q → Q be (the poset components of) isomorphisms. Define the functions ϕ ⊗ ψ : P Q → P Q and ϕ ψ :

, and easily seen to be an isomorphism as well.

We write P Q if there is a bijective (on points) morphism ϕ : Q → P between iposets P and Q. Intuitively, P Q if P has more arrows and is therefore less parallel than Q, while interfaces are preserved. Similar relations on posets and pomsets, sometimes called subsumption, are well studied [10, 12] . In particular, is a preorder on (finite) iposets and a partial order up-to isomorphism.

(

Proof. Let P = (P ⊗ P ) (Q ⊗ Q ) and P r = (P Q) ⊗ (P Q ). First, P = (P Q) /tP ≡sQ (P Q ) /t P ≡s Q = (P Q P Q ) tP ≡sQ,t P ≡s Q = P r , by definition of ⊗. Hence both posets have the same points, and we may choose ϕ : P r → P to be the identity. It remains to show that ϕ is order preserving, which means that every arrow in P r must be in P .

Hence suppose x ≤ Pr y, that is, x ≤ P Q y or x ≤ P Q y. In the first case, if x ≤ P y or x ≤ Q y, then x ≤ P ⊗P y or x ≤ Q⊗Q y and therefore x ≤ P y; and if x ∈ P \ t P and y ∈ Q \ s Q , then x ∈ P P \ t P ⊗P and y ∈ Q Q \ s Q⊗Q and therefore x ≤ P y, too. The second case is symmetric. Thus x ≤ P y holds in any case.

In sum, the algebra of iposets is similar to a concurrent monoid [14] , but is a partial operation with many units id k . As ⊗ is not a tensor, the categorical structure of iposets is somewhat unusual and deserves further exploration. 

We now derive further algebraic properties of iposets before turning to the iposets generated by gluing and parallel composition from singletons.

For an iposet P with order relation ≤ we write = ≤ ∩ ≥. Hence x y if and only if x and y are incomparable and therefore independent.

First, in addition to the lax interchange in Proposition 12, we present an equational interchange law as a witness that the equational theory of iPos given by the laws in Propositions 9 and 10 is not free. The lemmas that follow then show that this law is the only non-trivial additional identity.

For all iposets P , Q and k, ∈ {0, 1},

Proof (sketch). The interface between k id 1 1 and 1 id 1 forces these iposets to be glued separately to the rest in the gluing composition ( k id 1

On the one hand, the singleton iposets mentioned therefore do not interfere with compositions. On the other hand, Proposition 14 shows that some iposets can be decomposed both with respect to and ⊗.

Let S = { k id 1 | k, = 0, 1} denote the set of singleton iposets and C 1 = P 1 ⊗ · · · ⊗ P n P 1 , . . . , P n ∈ S the set of discrete iposets. The next lemma shows a kind of converse to the previous one: if an iposet is both -decomposable and ⊗-decomposable, then all components but one must be in S.

Let P = P 1 ⊗P 2 = Q 1 Q 2 such that P 1 = id 0 , P 2 = id 0 , and Q 1 = k id n n , Q 2 = n id k n for any k ≤ n. Then P 1 ∈ C 1 or P 2 ∈ C 1 .

Proof. Suppose P 1 / ∈ C 1 and P 2 / ∈ C 1 . Then P contains a 2+2: there are w, x ∈ P 1 and y, z ∈ P 2 for which w < P x, y < P z, w P y, w P z, x P y, and x P z.

If w, y / ∈ Q 2 , then w, y ∈ Q 1 \ t Q1 . As Q 2 = n id k n for any k ≤ n, there must be an element v ∈ Q 2 \ s Q2 . But then w ≤ P v and y ≤ P v, which yields arrows between w ∈ P 1 and y ∈ P 2 that contradict P = P 1 ⊗ P 2 . A dual argument rules out that x, z / ∈ Q 1 . It follows that w ∈ Q 2 or y ∈ Q 2 . Assume, without loss of generality, that w ∈ Q 2 . Then x ∈ Q 2 \ s Q2 because w < P1 x. Now if also y ∈ Q 2 , then by the same argument, z ∈ Q 2 \ s Q2 . Hence Q 2 contains two different points that are not in its starting interface; and as Q 1 \ t Q1 is non-empty, this again establishes a connection between x ∈ P 1 and z ∈ P 2 which cannot exist. Hence y / ∈ Q 2 , but then y ∈ Q 1 \ t Q1 , so that y ≤ P x, which contradicts x P y.

The next lemma generalises Levi's lemma for words [26] .

Let P Q = U V . Then there is an R so that either P = U R and R Q = V , or U = P R and R V = Q.

Proof (sketch). Obviously, P Q and U V have the same carrier set. By the assumption it is partitioned into three (disjoint) sets such that either P = U R and R Q = V , or U = P R and R V = Q. In the first case, it follows that P Q = U R Q and it remains to show that P Q = U R Q. If there are no interfaces, this is easy to see; otherwise, the proof is somewhat more tedious. The proof for the second case is similar.

It is instructive to find the two cases in the decomposition of N in Fig. 3 .

Levi's lemma is a factorisation property: every P Q = U V factorises either as U R Q or as P R V . Hence gluing decompositions are equal up-to associativity (and unit laws). For parallel composition, a Levi property as above does not hold, so we state a decomposition lemma directly: Lemma 17. Assume P 1 ⊗ · · · ⊗ P n = Q 1 ⊗ · · · ⊗ Q m , where each P i and Q j are (weakly) connected and not equal to id 0 . Then n = m, and there exists a permutation σ :

Proof. Let P = P 1 ⊗ · · · ⊗ P n , then P 1 , . . . , P n are the connected components of P , but so are Q 1 , . . . , Q m ; the claim follows.

The lemmas in this section are helpful for characterising the iposets generated by and ⊗ from singletons. This is the subject of the next section.

Recall that S is the set of singleton iposets. It contains the four iposets 0 id 0 1 , 0 id 1 1 , 1 id 0 1 and 1 id 1 1 , that is,

with mappings uniquely determined. We are interested in the sets of iposets generated from singletons using and ⊗. Strictly speaking, 0 id 0 1 should not count as a generator: it is equal to 0 id 1 1 1 id 0 1 by Proposition 14. We may view S as a (directed) graph or quiver on vertices 0, 1. Proof (sketch). Suppose (A, , ⊗, (1 i ) i≥0 ) is any category on N satisfying the equations of Propositions 9, 10 and 14. Let ϕ : S → A be any graph morphism that maps 0 to 0 and 1 to 1. We need to show that ϕ extends to a unique iposet morphismφ.

We can generate any id n from parallel compositions of id 1 . For any i ≥ 0, we mapφ(id i ) → 1 i , and we map any other singleton p ∈ S asφ(p) = ϕ(p). For complex iposets we proceed by induction on the number of elements, assuming that homomorphism laws hold for iposets with n elements.

If the top composition of the size n + 1 iposet P is , then an inductive application of Lemma 16 implies that the -decomposition of P is unique (up to associativity and unit laws), and we use associativity of to establish the homomorphism property ofφ. For ⊗ we proceed likewise, using the uniquedecomposition property of Lemma 17. Finally, if the top composition is ambiguous, then Lemma 15 forces the configuration in which Proposition 14 can be applied, yielding a parallel composition of the same size. Finally, this extension is unique, as it was forced by the construction.

For a more detailed proof, care need to be taken because morphisms between partial algebras need to be compatible with the definedness conditions of partial operations. The notion of free partial algebra can be found in Burmeister's lecture notes [2] . Categories are single-sorted partial algebras through their objectfree axiomatisation [24] .

Next we define hierarchies of iposets generated from S. (Removing 0 id 0 1 from S would change the hierarchy only for at most the first two alternations of and ⊗.) For any Q ⊆ iPos and ∈ {⊗, }, let Q = {P 1 · · · P n | n ∈ N, P 1 , . . . , P n ∈ Q} .

Then define C 0 = D 0 = S and, for all n ∈ N,

(this agrees with the C 1 notation used earlier). Finally, let

be the set of all iposets generated from S by application of ⊗ and .

Proof. We need to check the inclusions C n ⊆ C n+1 , D n ⊆ D n+1 , C n ⊆ D n+1 and D n ⊆ C n+1 . The first two are trivial by construction. For the third one, note that C 0 ⊆ C 0 = S = D 0 = D 1 . Since C n is constructed from C 0 by the same alternations of ⊗ and as D n+1 is constructed from D 1 , the inclusion holds. The proof of the fourth inclusion is similar.

Proof. For the forward direction, suppose P Q ∈ C 2 . First it is clear that all elements of C 1 are interval orders, so we will be done once we can show that the gluing composition of two interval orders is an interval order. This is precisely the proof of Lemma 15: if P Q contains a 2+2, then so do P or Q. Yet we also give a direct construction: Let σ P be the interval sequence for interval representation (b P , e P ) of P : n → m and σ Q the interval sequence for interval representation (b Q , e Q ) of Q : m → k. Then concatenate σ P and σ Q , rename b P , b Q as b and e P , e Q as e, delete e(t P (i)), b(s Q (i)) and replace e(s Q (i)) with e(t P (i)) for each i ∈ [m]. This yields the interval sequence for interval representation (b, e) of P Q and P Q is therefore an interval order. Figure 6 gives an example. For the backward direction, let P be an interval order and A P its set of maximal antichains. Then A P is totally ordered by the relation defined in Sect. 3. Now write A P = {P 1 , . . . , P k } such that P i P j for i < j. Then each P i is an element of S ⊗ . Write s 1 : [n 1 ] → P ← [n k+1 ] : t k for the sources and targets of P .

For i = 2, . . . , k, let [n i ] = P i−1 ∩ P i be the overlap and s i : [n i ] → P i , t i−1 : [n i ] → P i−1 the inclusions. Together with s 1 and t k this defines iposets s i : [n i ] → P i ← [n i+1 ] : t i . (Note that s 1 : [n 1 ] → P 1 because P 1 is the minimal element in A P ; similarly for t k : [n k+1 ] → P k .) It is clear that P = P 1 · · · P k ; see also [16, Prop. 2] .

In order to compare with series-parallel posets, we construct a similar hierarchy for these. Let T 0 = U 0 = S 0 = { 0 id 0 1 } and, for all n ∈ N,

Then, because any element of any T n or U n has empty interfaces and because is serial composition for all iposets with empty interfaces, we see that

is the set of series-parallel posets. Note that T n ⊆ C n and U n ⊆ D n for all n, hence alsoS 0 ⊆S. NowS 0 contains precisely the N-free posets whereas N is an interval order. Therefore N ∈ C 2 , which implies the next lemma. On the other hand, we will show below thatS 0 ⊆ C n for any n.

, there is an iposet with two non-trivial different decompositions.

Proof. Directly from Proposition 14.

Next we show that the C n hierarchy is infinite, by exposing a sequence of witnesses for C 2n−1 C 2n for all n ≥ 1.

Let Q = 0 id 0 1 , P 1 = Q Q, and for n ≥ 1, P n+1 = Q (P n ⊗ P n ). Note that all these are series-parallel posets. Graphically:

Lemma 24. P n ∈ C 2n \ C 2n−1 for all n ≥ 1.

Proof. By induction. For n = 1, P 1 / ∈ C 1 , but Q ∈ C 0 ⊆ C 1 and hence P 1 = Q Q ∈ C 2 = C 1 . Now for n ≥ 1, suppose C 2n−1 P n ∈ C 2n . We use Lemma 15 to show that P n ⊗ P n ∈ C 2n+1 \ C 2n : Obviously P n ⊗ P n ∈ C 2n+1 = C ⊗ 2n . If P n ⊗ P n ∈ C 2n = C 2n−1 , then P n ⊗ P n = Q 1 · · · Q k for some Q 1 , . . . , Q k ∈ C 2n−1 . Yet P n / ∈ C 1 , which contradicts Lemma 15. Now to P n+1 = Q (P n ⊗ P n ). Trivially, P n+1 ∈ C 2n+2 = C 2n+1 . Suppose P n+1 ∈ C 2n+1 = C ⊗ 2n . P n+1 is connected, hence not a parallel product, so that P n+1 must already be in C 2n = C 2n−1 and therefore P n+1 = R 1 R 2 . Then, by Levi's lemma, there is an iposet S such that either Q = R 1 S and S (P n ⊗P n ) = R 2 or R 1 = Q S and S R 2 = P n ⊗ P n . In the second case, S R 2 = P n ⊗ P n , which again contradicts Lemma 15; in the first case, both R 1 and S must be single points (with suitable interfaces), so that either R 1 = 0 id 1 1 and R 2 = P n+1 (with an extra starting interface) or R 1 = Q and R 2 = P n ⊗ P n . This shows that P n+1 = Q (P n ⊗ P n ) is the only non-trivial -decomposition of P n+1 . Thus P n ∈ C 2n−1 , a contradiction, and therefore P n+1 / ∈ C 2n+1 .

Corollary 25. C 2n−1 C 2n for all n ≥ 1, hence the C n hierarchy does not collapse, and neither does the D n hierarchy.

Proof. The last statement follows from D 2n−2 ⊆ C 2n−1 C 2n ⊆ D 2n+1 . Table 1 . Different types of posets with n points: all posets; sp-posets; gp-posets; (weakly) connected gp-posets; iposets with starting interfaces only; iposets; gp-iposets.

n P(n) SP(n) GP(n) GPC(n) SIP(n) IP(n) GPI(n) Using procedures to generate non-isomorphic posets of different types, we have used our software to verify that 1. all posets on five points are inS and therefore gp-posets; 2. NN, M, W, 3C, and LN are the only six-point posets that are not inS.

We provide tables of gluing-parallel decompositions of posets in an extended version [5] to prove these claims.

We have also used our software to count non-isomorphic posets and iposets of different types, see Table 1 . We note that P and SP are sequences no. A000112 and A003430, respectively, in the On-Line Encyclopedia of Integer Sequences (OEIS). 4 Sequences GPC, SIP, IP, and GPI are unknown to the OEIS.

The single iposet on two points which is not gluing-parallel is the symmetry [2] : 2 → 2 with s(1) = 1, s(2) = 2, t(1) = 2, and t(2) = 1. The prefix of GP we were able to compute equals the corresponding prefix of sequence no. A079566 in the OEIS,(see footnote 4) which counts the number of connected (undirected) graphs which have no induced 4-cycle C 4 . We leave it to the reader to ponder upon the relation between gp-posets and C 4 -free connected graphs.

Free shuffle algebras in language varieties

Lecture notes on universal algebras, many sorted algebras

Regular Algebra and Finite Machines

Graph Structure and Monadic Second-Order Logic. A Language-Theoretic Approach

Generating posets beyond N. CoRR

The algebra of directed acyclic graphs

Intransitive indifference with unequal indifference intervals

Interval Orders and Interval Graphs: A Study of Partially Ordered Sets

Concurrent dynamic algebra

The equational theory of pomsets

Tolerance Graphs

On partial languages

Linearizability: a correctness condition for concurrent objects

Concurrent Kleene algebra and its foundations

Developments in concurrent Kleene algebra

Modeling operational semantics with interval orders represented by sequences of antichains

Structure of concurrency

Modeling concurrency with interval traces

Concurrent Kleene algebra with tests and branching automata

Kleene algebra with observations

Concurrent Kleene algebra: free model and completeness

The mutual exclusion problem: part I -a theory of interprocess communication

On interprocess communication, part I: basic formalism

Categories for the Working Mathematician

Completeness theorems for pomset languages and concurrent Kleene algebras

On semigroups

Series-parallel languages and the bounded-width property

Presenting finite posets

Exploring an interface model for CKA

A discrete geometric model of concurrent program execution

Concurrent dynamic logic

The recognition of series parallel digraphs

The refinement theorem for ST-bisimulation semantics

Petri net models for algebraic theories of concurrency

Failures semantics based on interval semiwords is a congruence for refinement

Modular Construction and Partial Order Semantics of Petri Nets

A contribution to the theory of relative position

An algebraic characterization of the behaviour of non-sequential systems

Corollary 26. For all n ∈ N,S 0 ⊆ C n andS 0 ⊆ D n .Proof. As explained already above, P n ∈S 0 for all n. This and Lemma 24 imply the first statement. The second one follows from C n ⊆ D n+1 .We have seen that the C n and D n hierarchies are properly infinite and contain the set of sp-posets only in the limitS = n≥0 C n = n≥0 D n .Finally, we turn to the question of characterising this limitS geometrically. Given that a poset is series-parallel if and only if if it does not contain an induced subposet isomorphic to N, we aim for a similar characterisation of gp-(i)posets using forbidden subposets. We expose five such subposets, but leave the question of whether there are others to future work.Define the following five posets on six points: Assume first that a ∈ Q. Then a ≤ Q b, hence also b ∈ Q, but b / ∈ Q min , that is, b / ∈ s Q . Now e ≤ P Q b, which forces e ∈ t P and therefore e ∈ Q. This in turn implies that d, f ∈ Q and in particular e ≤ Q f . Thus f / ∈ Q min and therefore f / ∈ s Q , which forces c ∈ t P and therefore c ∈ Q. This shows that the NN lies entirely in Q.Finally assume that a / ∈ Q. Then a ∈ P \ t P , and as a ≤ P Q d and a ≤ P Q f , we must have d, f ∈ s Q and therefore d, f ∈ P . This forces c, e ∈ P and in particular e ≤ P f . Thus e / ∈ P max , whence e / ∈ t P . This in turn forces b ∈ s Q and therefore b ∈ P . This shows that NN lies entirely in P .

We have encoded most of the constructions in this paper with Python to experiment with gluing-parallel (i)posets. Notably, Proposition 27 is, in part, a result of these experiments. 3 Our prototype is rather inefficient, which explains why some numbers are "n.a.", that is, not available in Table 1 .