Eleftherios Matsikoudis

Edward A Lee

From Transitions to Executions

Interleaving theories have traditionally failed to integrate a satisfactory treatment of the so-called "finite delay property". This is generally attributed to the expansion law of such theories, but in truth, the problem is rooted in the concept of labelled transition system. We introduce a new type of system, in which, instead of labelled transitions, we have, essentially, sequences of labelled transitions. We call systems of this type labelled execution systems. We use a coalgebraic representation to obtain, in a canonical way, a suitable concept of bisimilarity among such systems, study the conditions under which that concept agrees with the intuitive understanding of equivalence of branching structure that one has for these systems, and examine their relationship with labelled transition systems, precisely characterizing the difference in expressive power and branching complexity between the two kinds of systems.

Introduction

The process algebra literature is dominated by the concept of labelled transition system. And to some extent, this is understandable. For process algebra emerged from the marriage of Plotkin's structural operational semantics (see [START_REF] Plotkin | A structural approach to operational semantics (Aarhus notes)[END_REF]) and Keller's named transition systems (see [START_REF] Robert | Formal verification of parallel programs[END_REF]) (see [34, chap. 12], [START_REF] Berger | An interview with Robin Milner[END_REF], [START_REF] Plotkin | The origins of structural operational semantics[END_REF], [START_REF] Jos | A brief history of process algebra[END_REF]). This marriage was the work of Robin Milner, and is most clearly expounded in [START_REF] Milner | Communication and Concurrency[END_REF], but was already present in [START_REF] Milner | Synthesis of communicating behaviour[END_REF], where the so-called "expansion law" was stated for the first time.

The expansion law has been a constant source of controversy in the theory of concurrency. In the language of Milner's CCS (see [START_REF] Milner | A calculus of communicating systems[END_REF], [START_REF] Milner | Communication and Concurrency[END_REF]), a typical equation asserted by the law is the following:

Here, 'a' and 'b' stand for arbitrary actions, '0' for the inactive agent, which is incapable of performing any action, '.' for sequential composition, '|' for parallel composition, and '+' for alternative composition. And the intended meaning of (1) is that the parallel execution of a and b is "equivalent", in some sense, to the indeterminate serialization of the two.

In order to justify the expansion law, and the blurring between causal dependence and temporal precedence resulting from it, Milner wrote the following in [30, p. 81]:

We do not yet know how to frame a sufficiently general law without, in a sense, explicating parallelism in terms of non-determinism. More precisely, this means that we explicate a (parallel) composition by presenting all serializations -or interleavings -of its possible atomic actions. This has the disadvantage that we lose distinction between causally necessary sequence, and sequence which is fictitiously imposed upon causally independent actions; . . . . However, it may be justified to ignore it if we can accept the view that, in observing (communicating with) a composite system, we make our observations in a definite time sequence, thereby causing a sequencing of actions which, for the system itself, are causally independent.

Effectively, what he argued for was a dichotomy between causation and observation in the theory of concurrency. And what he proposed as an observational view to the theory was the interleaving of the atomic actions of the various agents inside a system as would be perceived by a single, sequential observer outside the system. But what he failed to admit was that the expansion law is in fact inconsistent with that view.

To understand the mismatch, consider the following equation derived from the expansion law, again in the language of CCS: fix(X = a.X) | fix(X = b.X) = fix(X = a.X + b.X) .

(

) 2
Here, we use recursion expressions to define agents with infinite behaviour. Thus, fix(X = a.X) is an agent that forever iterates a, fix(X = b.X) one that forever iterates b, and fix(X = a.X + b.X) one that at each iteration, does either a or b, indeterminately choosing between the two. But whereas every infinite sequence over {a, b} is a trace of a possible execution of fix(X = a.X + b.X), not every such sequence is consistent with what could be perceived by a sequential observer of fix(X = a.X) | fix(X = b.X). Indeed, only those sequences that contain an infinite number of a's and an infinite number of b's are. For if fix(X = a.X) and fix(X = b.X) execute in parallel, each of them must eventually perform an infinite number of actions, and each of these actions must eventually be perceived by any sequential observer of fix(X = a.X) | fix(X = b.X).

All this goes unnoticed in the finite case, because interleaving the executions of two finite agents is ultimately equivalent to indeterminately alternating between the two. But the expansion law blindly carried that equivalence over to the infinite case. And this created confusion. Interleaving became synonymous with bounded indeterminacy (see [18, chap. 9]), and the observational view was robbed of its power to express properties like fairness (see [START_REF] Pnueli | The temporal semantics of concurrent programs[END_REF]) or the finite delay property (see [START_REF] Karp | Parallel program schemata[END_REF]) (e.g., see [START_REF] Park | On the semantics of fair parallelism[END_REF]).

Of course, it is not the expansion law per se that is to blame for this confusion. Interleaving is an operation on executions, not transitions. The problem is with the concept of labelled transition system.

The purpose of this work is to introduce a new kind of system, in which, instead of labelled transitions, one has, essentially, sequences of labelled transitions. We call systems of this kind labelled execution systems. Deferring the study of their potential use as semantic models of behaviour, our goal here is to develop a thorough understanding of the so-called "branching structure" of such systems. And the theory of coalgebra offers a convenient and powerful analytical framework to do so.

The main contributions of this work are the following: (i) we define labelled execution systems, (ii) we represent these systems coalgebraically, and use that representation to obtain, in a canonical way, a suitable concept of bisimilarity among such systems, (iii) we study the conditions under which that concept agrees with the intuitive understanding of equivalence of branching structure that one has for these systems, and (iv) we work out their relationship with labelled transition systems, precisely characterizing the difference in expressive power and branching complexity between the two kinds of systems.

Throughout this work, we assume a basic level of familiarity with the theory of universal coalgebra (e.g., see [START_REF] Jan | Universal coalgebra: a theory of systems[END_REF]), and in particular, with coalgebras over the category of all classes and all class functions between them (e.g., see [START_REF] Aczel | A final coalgebra theorem[END_REF]). This is a "surprisingly coalgebra-friendly category" (see [5, p. 3]), which is one of the main reasons for choosing to work with it. And while it is possible to avoid such a super-large category, by only considering endofunctors that are bounded in some suitable sense, we think that classes provide for a cleaner, unobscured presentation of our ideas.

For lack of space, we omit all proofs; they can be found in [START_REF] Matsikoudis | Labelled execution systems[END_REF].

Labelled Transition Systems and Coalgebras

The concept of labelled transition system is of course the paradigmatic example of a coalgebra. Indeed, the theory of coalgebra was largely inspired by the study of that concept (e.g., see [START_REF] Aczel | A final coalgebra theorem[END_REF]). Here, we formalize it in a slightly different way, namely using a binary relation rather than a ternary one, and go through its coalgebraic handling anew with the intent of drawing the reader's attention to the unity of formal treatment between this section and the next.

Labelled Transition Systems

Assume a non-empty set L of labels.

Definition 1. An L-labelled transition system is an ordered pair S, T of a set S and a binary relation T : S ↔ L × S.

Assume an L-labelled transition system S, T .

We write s l --→ T s if and only if s T l, s . We call any s ∈ S a state of S, T , and any s, l, s ∈ graph T a transition of S, T .

Labelled transition systems have been around at least since Moore's work on finite automata in [START_REF] Moore | Gedanken-experiments on sequential machines[END_REF], where they appeared in tabular as well as pictorial form. In their present form, they seem to have been introduced by Keller in [START_REF] Robert | Formal verification of parallel programs[END_REF], where they were called named transition systems. And although Keller used them to model parallel computation, it was apparently Milner who first saw labels as shared vehicles of interaction, and labelled transition systems as models of communicating behaviour, paving the way for [START_REF] Milner | A Calculus of Communicating Systems[END_REF] and the advent of process algebra.

Assume L-labelled transition systems S 1 , T

(a) if s 1 l - -→ T1 s 1 , then there is s 2 such that s 2 l - -→ T2 s 2 and s 1 B s 2 ; (b) if s 2 l - -→ T2 s 2 , then there is s 1 such that s 1 l - -→ T1 s 1 and s 1 B s 2 .
We say that s 1 and s 2 are bisimilar among S 1 , T 1 and S 2 , T 2 if and only if there is a bisimulation B between S 1 , T 1 and S 2 , T 2 such that s 1 B s 2 .

The idea of bisimilarity is that for any path branching out of either one of the two states, there is a path branching out of the other one, that carries the same labels in the same order, and goes through states that are again related to the corresponding states of the first path in the same way. This last piece of recursion is what separates bisimilarity from trace equivalence, making the former sensitive to the branching potential of each state.

The concept of bisimulation is due to David Park (see [START_REF] Park | Concurrency and automata on infinite sequences[END_REF]), and is without doubt the most significant contribution of the theory of concurrency to the broader arena of computer science and mathematics at large.

Labelled Transition Coalgebras

Assume a binary relation R : S 1 ↔ S 2 , and a function f : S 1 → P S 2 . 1We write fun R for a function from S 1 to P S 2 such that for any

s 1 ∈ S 1 , (fun R)(s 1 ) = {s 2 | s 1 R s 2 } .
We write rel f for a binary relation between S 1 and S 2 such that for any s 1 ∈ S 1 and any s 2 ∈ S 2 ,

s 1 (rel f ) s 2 ⇐⇒ s 2 ∈ f (s 1 ) .
Proposition 1. The following are true:

(a) rel(fun R) = R; (b) fun(rel f ) = f .
Proposition 1 suggests an alternative, coalgebraic formalization of the concept of L-labelled transition system. The pertinent functor is of course the endofunctor Pow • (L × Id) on Class2 , namely the composite of the power-set endofunctor Pow on Class with the left product endofunctor L × Id on Class. An L-labelled transition system S, T can then be represented as a (Pow • (L × Id))coalgebra, namely as S, fun T , and conversely, a (Pow•(L×Id))-coalgebra C, τ as an L-labelled transition system, namely as C, rel τ , with the caveat that C be a set.

Definition 3. An L-labelled transition coalgebra is a (Pow•(L×Id))-coalgebra.
We write L-LTC for (Pow • (L × Id))-Coalg. 3Formally, we will treat L-labelled transition systems and L-labelled transition coalgebras as distinct concepts. But informally, we shall think of an L-labelled transition coalgebra as an L-labelled transition system, no matter how large the carrier of the coalgebra is.

Assume an L-labelled transition coalgebra C, τ .

We write c It is now possible to obtain the concept of bisimulation between labelled transition systems as an instance of the more general concept of coalgebraic bisimulation between labelled transition coalgebras.

Assume L-labelled transition coalgebras C 1 , τ

(a) if c 1 l - -→ τ1 c 1 , then there is c 2 such that c 2 l - -→ τ2 c 2 and c 1 B c 2 ; (b) if c 2 l - -→ τ2 c 2 , then there is c 1 such that c 1 l - -→ τ1 c 1 and c 1 B c 2 .
Proposition 4. B is a bisimulation between S 1 , T 1 and S 2 , T 2 if and only if B is a bisimulation between the L-labelled transition coalgebras S 1 , fun T 1 and S 2 , fun T 2 .

Labelled Execution Systems and Coalgebras

This section contains the main body of this work, where we define and study our newly proposed systems. For the most part, we treat these systems in the guise of coalgebras. But for the benefit of the non-coalgebraist, as well as the more application-oriented reader, we treat systems and coalgebras as formally distinct, and translate our results back into the relational language of systems.

Labelled Execution Systems

Definition 4. An L-labelled execution system is an ordered pair S, E of a set S and a binary relation E : S ↔ S (L × S). 4Assume an L-labelled execution system S, E . We write s E e if and only if s E e. We call any s ∈ S a state of S, E , and any s, e ∈ graph E an execution of S, E .

Notice that an execution is an ordered pair of a state and a sequence of ordered pairs of labels and states, instead of a single odd-length alternating sequence of states and labels, what might have seemed a more natural option. And while we do think that there is a certain clarity in distinguishing the starting state of an execution from any subsequent step, this was mainly a choice of mathematical convenience. Its merit will soon become apparent.

Labelled Execution Coalgebras

As our choice of formalization should have made obvious, the concept of labelled execution system is a direct generalization of that of labelled transition system. The idea of a single step from one state to another is replaced by that of an "admissible" path through the system over which a sequence of steps can be taken. The result is a more elaborate notion of branching structure. And if we are to associate this notion with behaviour of some kind, we need to understand what constitutes similarity and dissimilarity of it. In other words, we need a concept of branching equivalence suited to labelled execution systems. What should that concept be?

In [START_REF] Jan | On the foundations of final semantics: Nonstandard sets, metric spaces, partial orders[END_REF], Rutten and Turi propose a simple approach to this type of problem: all we have to do is find a suitable endofunctor to represent our systems coalgebraically. We can then use that endofunctor to instantiate the "parametric" concept of coalgebraic bisimulation and obtain not only the equivalence concept that we seek, but a model too that is fully abstract with respect to that concept, in the shape of a final coalgebra. 5 This is straightforward here.

We begin by composing the sequence-set endofunctor Seq on Class with the left product endofunctor L × Id on Class to obtain the endofunctor Seq • (L × Id) on Class, which assigns to every class C the class

Seq(L × C) = {s | there is S such that S ⊆ L × C and s ∈ S S} ,
and to every class function f :

C 1 → C 2 a class function Seq(L × f ) from Seq(L × C 1 ) to Seq(L × C 2 ) such that for every s ∈ Seq(L × C 1 ), (Seq(L × f ))(s) = if s = ; l, f (c) • (Seq(L × f ))(s ) if s = l, c • s .
Despite the seeming circularity, the action of Seq • (L × Id) on class functions is well defined. It is just an instance of a definition by corecursion (see [START_REF] Barwise | Vicious Circles[END_REF]).

We

C 1 → C 2 a class function Pow Seq(L × f ) from Pow Seq(L × C 1 ) to Pow Seq(L × C 2 ) such that for every S ∈ Pow Seq(L × C 1 ), (Pow Seq(L × f ))(S) = {(Seq(L × f ))(s) | s ∈ S} .
Just as with labelled transition systems, we can use Proposition 1 to obtain our coalgebraic representation.

Definition 5. An L-labelled execution coalgebra is a (Pow • Seq • (L × Id))- coalgebra.
We write L-LEC for (Pow • Seq • (L × Id))-Coalg. Assume an L-labelled execution coalgebra C, ε . We write c ε e if and only if e ∈ ε(c). At this stage, we could already use Proposition 7 below as our definition of bisimulation between labelled execution systems. But we prefer a different, more operational one that will help us develop some insight into the concept.

Assume a binary class relation R :

C 1 ↔ C 2 .
We write Seq(L × R) for a binary class relation between Seq(L × C 1 ) and Seq(L × C 2 ) such that for every e 1 ∈ Seq(L × C 1 ) and every e 2 ∈ Seq(L × C 2 ),

e 1 Seq(L × R) e 2 ⇐⇒ there is e ∈ Seq(L × graph R)
such that e 1 = Seq(L × dpr R)(e) and e 2 = Seq(L × cpr R)(e). 7 Notice that Seq(L×R) is a simple lift of R to pairs of sequences over L×dom R and L × cod R. Our choice of notation may be justified by the fact that

Seq(L × R) = Seq(L × ((dpr R) -1 ; cpr R)) = (Seq(L × dpr R)) -1 ; Seq(L × cpr R) . Assume L-labelled execution coalgebras C 1 , ε 1 and C 2 , ε 2 . Proposition 6. B is a bisimulation between C 1 , ε 1 and C 2 , ε 2 if

Abrahamson Systems and Coalgebras

Informally, we can explain bisimilarity of states of labelled execution systems in the same way as we did in the case of labelled transition systems. Only now, paths are not implicitly inferred from a transition relation, but explicitly stipulated as part of the system structure. And this can have some peculiar side effects.

For example, consider two {l 0 , l 1 }-labelled execution systems, whose executions are as depicted in the following left and right frames respectively:

s 0 s 1 l 0 s 2 s 3 s 3 s 4 l 0 l 1
s 0 and s 2 are not bisimilar, simply because there is an execution starting from s 3 , and no execution starting from s 1 . But why should we care if there is? The only execution starting from s 2 has only one step, and is in perfect agreement with the only execution starting from s 0 . So, intuitively, there is no difference in branching potential between the two states. We must therefore conclude that bisimilarity is, in this case, inconsistent with our informal sense of equivalence of branching structure.

A plausible remedy for this would, informally, be the following: for any path beginning at a given state, discount any branch off that path that is not a suffix of another path beginning at that same state. And indeed, this would work for this particular case. But there are more problems.

Consider two {l 0 , l 1 , l 2 }-labelled execution systems, whose executions are those depicted in the following left and right frames respectively:

s 0 s 1 s 3 s 0 s 2 s 4 l 0 l 0 l 1 l 2 s 5 s 6 s 7 s 5 s 6 s 8 l 0 l 0 l 1 l 2
s 0 and s 5 are bisimilar, but intuitively, there is difference in branching potential between the two states: the two executions starting from s 0 diverge right away at s 0 , whereas those starting from s 5 diverge after the first step at s 6 . Of course, the explanation here is that there is no execution starting from s 6 , and so, conceptually, the choice between the diverging steps is already made at s 5 . But then, what is the point of having the two executions share the state s 6 ? By now, the reader should begin to suspect what the source of our problems is: what we have called "state" in our systems does not behave as such. In a type of system supposed to serve as a modelling device for processes of some kind, it is essential that "the future behavior depends only upon the current state, and not upon how that state was reached". And this is not always the case here. What we need to do is constrain the structure of our systems so that it is.

Of course, this idea is not new. The quote above is from [28, p. 176], where Lamport required that the set of paths in a path structure be suffix closed, in the sense that for any path in the set, any suffix of that path is again a path in the set. It was later observed in [START_REF] Emerson | Alternative semantics for temporal logics[END_REF] that this is not enough: one must also require that the set of paths be fusion closed, in the sense that for any prefix of a path in the set, and any suffix of another path in the set, if the former ends at the state at which the latter begins, then their fusion at that state is again a path in the set (see [START_REF] Vaughan | Process logic: Preliminary report[END_REF]). And apparently, it was Abrahamson, in [START_REF] Abrahamson | Decidability and Expressiveness of Logics of Programs[END_REF], that first considered path structures that satisfied both requirements (see [START_REF] Courcoubetis | Reasoning about fair concurrent programs[END_REF]).

We now adapt these requirements to our own setting. For generality, we work on the coalgebra side of the theory.

We say that C, ε is Abrahamson if and only if the following are true: Here, (i) corresponds to suffix closure, and (ii), assuming (i), to fusion closure. We consider the class of all Abrahamson systems, defined in a similar manner, to be the largest class of "well behaved" labelled execution systems that could be useful as semantic models of behaviour. It is then quite pleasing that the full subcategory of L-LEC comprised of all Abrahamson L-labelled execution coalgebras is a (Pow • Seq • (L × Id))-covariety, what implies the existence of a final coalgebra among them (see [START_REF] Matsikoudis | Labelled execution systems[END_REF]).

Underlying Labelled Transition Systems and Coalgebras

In an Abrahamson system, there is a clear notion of a "possible next step" relation, which induces the construction of an associated, or better, underlying labelled transition system. From a mathematical standpoint, this construction makes sense for a non-Abrahamson system as well, and is most conveniently carried out on the coalgebra side of the theory. Our choice of notation here is not arbitrary. We think of η as an operator that assigns to every class C a class function from its image under Pow • Seq • (L × Id) to its image under Pow • (L × Id). And what is interesting about this operator is that for every class function f :

C 1 → C 2 , η(C 2 ) • Pow Seq(L × f ) = Pow(L × f ) • η(C 1 ) . Thus, η is a natural transformation from Pow • Seq • (L × Id) to Pow • (L × Id).
The reason why it is of interest to us here that η is a natural transformation is a theorem by Rutten, according to which, every natural transformation ν from an endofunctor F 1 on Class to an endofunctor F 2 on Class induces a functor from F 1 -Coalg to F 2 -Coalg that assigns to every F 1 -coalgebra C, γ the F 2coalgebra C, η(C) • γ , and to every homomorphism h from an [42, thm. 15.1]). In a word, the induced functor preserves homomorphisms, and as a consequence, bisimulations too (see [42, lem. 5.3] and [21, thm. 5.11]).

F 1 -coalgebra C 1 , γ 1 to an F 1 -coalgebra C 2 , γ 2 that same class function h, which is now a homomorphism from the F 2 -coalgebra C 1 , η(C 1 ) • γ 1 to the F 2 -coalgebra C 2 , η(C 2 ) • γ 2 (see
In our case, the functor induced by η is a forgetful functor, which, informally, keeps only the first step, if any, from any execution starting from any state, and discards the rest.

Theorem 1. If h is a homomorphism from C 1 , ε 1 to C 2 , ε 2 , then h is a homomorphism from the L-labelled transition coalgebra C 1 , η(C 1 ) • ε 1 to the L-labelled transition coalgebra C 2 , η(C 2 ) • ε 2 . Corollary 1. If B is a bisimulation between C 1 , ε 1 and C 2 , ε 2 , then B is a bisimulation between the L-labelled transition coalgebras C 1 , η(C 1 ) • ε 1 and C 2 , η(C 2 ) • ε 2 .
Of course, we can translate all this back to the system side of the theory. Assume a binary relation E : S ↔ S (L × S). We write trans E for a binary relation between S and L × S such that for any s ∈ S and any l, s ∈ L × S, s (trans E) l, s ⇐⇒ there is e such that s E e, e = , and head e = l, s .

Proposition 8. trans E = rel(η(S) • fun E).

Theorem 2. If B is a bisimulation between S 1 , E 1 and S 2 , E 2 , then B is a bisimulation between the L-labelled transition systems S 1 , trans E 1 and S 2 , trans E 2 .

Generable Systems and Coalgebras

The converse of Theorem 2 is of course false. But it is instructive to see exactly where it fails. We go over it through a series of simple examples. First, suppose that S 1 , E 1 and S 2 , E 2 are two {l}-labelled execution systems, whose single executions are as depicted in the following left and right frames respectively:

s 0 s 1 l s 2 s 3 s 4 l l
Then s 0 and s 2 are bisimilar among the two {l}-labelled transition systems S 1 , trans E 1 and S 2 , trans E 2 , but not among S 1 , E 1 and S 2 , E 2 .

The problem is easy to spot here. The two systems have one execution each. But whereas the execution of the first system has only one step, the execution of the second has two. And that second step is dropped during the labelled transition system construction. Now suppose that S 1 , E 1 and S 2 , E 2 are two {l 0 , l 1 , l 2 }-labelled execution systems, whose executions are as depicted in the following left and right frames respectively:

s 0 s 1 s 2 s 1 s 2 s 1 s 3 l 0 l 1 l 2 l 1 s 4 s 5 s 7 s 5 s 6 s 5 s 7 l 0 l 1 l 2 l 2
Then s 0 and s 4 are bisimilar among the {l 0 , l 1 , l 2 }-labelled transition systems S 1 , trans E 1 and S 2 , trans E 2 , but not among S 1 , E 1 and S 2 , E 2 .

Here the problem is of a different nature. Every step of every execution is accounted for in the underlying labelled transition systems. However, the two longer executions, starting from s 0 and s 4 respectively, disagree on their second step, and that disagreement is masked by the agreement of executions starting from s 1 and s 5 respectively.

These two examples were specially chosen to target the two defining clauses of the Abrahamson property. Specifically, and informally, the systems in the first example are not suffix closed, thus violating clause (i) of the property, whereas those in the second are not fusion closed, thus violating clause (ii). Overall, none of them is Abrahamson. And since our construction was based on the idea of a "possible next step" relation, which, in the case of a non-Abrahamson system, is a conceptually ambiguous notion, it is no surprise that non-bisimilar states turn bisimilar in the constructed systems.

With Abrahamson systems, things get much more interesting. Consider then the {l 0 , l 1 }-labelled transition system, with l 0 = l 1 , portrayed in the following diagram:

s 0 s 1 s 2 s 3 l 0 l 0 l 1 l 0 l 0
The first {l 0 , l 1 }-labelled execution system that we wish to consider here is the unique Abrahamson system whose executions starting from s 0 correspond to all maximal paths in this diagram. The second is the one whose executions are all the executions of the first, except the single infinite execution stuttering around s 0 . And because of this exception, s 0 is not bisimilar with itself among the two systems.

This beautiful example is from [START_REF] Aczel | A semantic universe for the study of fairness[END_REF]. Here, it is perhaps convenient to think of the two systems as modelling the behaviour of two distinct processes, both initialized at s 0 . The first process will either loop around s 0 forever, or iterate through it for a finite, indeterminate number of times before progressing to s 1 .

From there on, a single indeterminate choice will decide its fate. The second process, on the other hand, is not allowed to loop around s 0 forever. It must eventually advance to s 1 , from where on it behaves just like the first one. What sets the behaviour of the two processes apart is, of course, the infinite stuttering around s 0 , permitted for the first process, but not the second. However, this is something that cannot be determined by the sequences of actions that the two processes perform in the course of their executions, for the trace of that infinite stuttering is matched by that of every infinite execution that eventually loops around s 2 . And yet the two processes ought to be distinguished. For during that infinite stuttering, the first process may always choose to branch off to a state from which it can perform l 1 , whereas, in every execution having that trace, the second must eventually reach a state from which it cannot ever do so.

With respect to the failure of the converse of Theorem 2, the problem here is the existence of an infinite path in the diagram that does not correspond to any execution of a system, but whose every finite prefix is a prefix of another path that does.

This too is something that has already come up in the investigation of path structures in temporal logic. In [START_REF] Emerson | Alternative semantics for temporal logics[END_REF], Emerson called a set of paths limit closed provided that for every infinite, strictly increasing chain of finite prefixes of paths in the set, the limit of that chain, in the standard topology of sequences, is again a path in the set. This property was apparently also first considered in [START_REF] Abrahamson | Decidability and Expressiveness of Logics of Programs[END_REF]. But it was Emerson in [START_REF] Emerson | Alternative semantics for temporal logics[END_REF] who proved the independence of all three closure properties, and the equivalence of their conjunction to the existence of a transition relation generating the given set of paths. Apart from the absence of labels, which has no bearing in this particular discussion, Emerson's setup was different in that paths were always infinite. But this too is of no importance in our examples, which, in light of Emerson's result, appear to implicate violation of limit closure in the failure of the underlying labelled transition system to subsume all the branching information relevant to a given Abrahamson system.

Our next example is perhaps the most curious one. Consider the simple {l}-labelled transition system portrayed in the following diagram: s l There are exactly three Abrahamson {l}-labelled execution systems that one can lay over this labelled transition system. The first is the one whose only execution corresponds to the only infinite path in the diagram. The second is the one whose executions correspond to all finite paths in the diagram. And of course, the third is the one whose executions are all executions of the first and second system. But s is not bisimilar with itself among any two of the three.

Informally, the second system is not limit closed, and this is one part of the problem. But the first and third are, and so there must be something more going on here. The answer is in the difference between Emerson's setup and ours mentioned earlier. Here, executions are not always infinite. In a system that is, informally, suffix closed, if there is a finite execution, then there is an empty execution. And an empty execution creates a type of branching that is impossible to mimic in a labelled transition system. In an Abrahamson system that is used to model the behaviour of a process, an empty execution can be used to model termination. But if there is another, non-empty execution starting from the same state, then termination becomes a branching choice, one that does not show up in the "possible next step" relation of the system. This feature of indeterminate termination, as we might call it, can seem a little odd at first, but is really a highly versatile mechanism, particularly useful in modelling idling in absence of input stimuli.

Finally, consider the labelled transition system of the following, trivial diagram: s There are exactly two labelled execution systems that one can lay over this labelled transition system: one that has one execution, the empty execution, and one that has no execution. And of course, s is not bisimilar with itself among the two.

This degenerate case deserves little comment. We only remark that in a suffix closed system, if a state has no execution starting from it, then it has no execution going through it.

At this point, we have found five possible causes of failure for the converse of Theorem 2. We have chosen our examples carefully, to examine each of the five separately and independently from one another. And we have observed how each of the first three connects to violation of one of the three closure properties that have been shown to collectively characterize sets of infinite paths generable by a transition relation. But finite paths add another dimension to the problem, rendering Emerson's characterization result obsolete. What we will show next is that impossibility of indeterminate termination, along with a non-triviality condition guarding against the occurrence of an isolated state, can be added to the conditions of suffix, fusion, and limit closure, to produce a complete characterization of system generability, insensitive to the length of the executions.

First, we need to make the notion of generability precise. For generality, we transfer ourselves again to the coalgebra side of the theory.

Assume a class function τ :

C → Pow(L × C), c ∈ C, and e ∈ Seq(L × C).
We say that e is a τ -orbit of c if and only if the following are true:

(i) one of the following is true: We say that τ generates ε if and only if gen τ = ε. We say that ε is generable if and only if there is a class function from C to Pow(L × C) that generates ε.

We say that C, ε is generable if and only if ε is generable.

Assume class functions τ 1 , τ 2 : C → Pow(L × C). Proposition 9. If τ 1 = τ 2 , then gen τ 1 = gen τ 2 .
Proposition 10. The following are true: Clause (a) of Theorem 3 corresponds to suffix closure, clause (b), conditioned on (a), to fusion closure, and clause (c) to limit closure. Clause (d) asserts the impossibility of indeterminate termination. Finally, clause (e) is the non-triviality condition discussed earlier, and essentially substitutes for Emerson's left totality condition on the generating transition relation (see [START_REF] Emerson | Alternative semantics for temporal logics[END_REF]).

(a) η(C) • gen τ = τ ; (b) if ε is generable, then ε = • ε).
Each of these five properties has come about in connection with a different cause of failure of the converse of Theorem 2, and hence of Theorem 1 and Corollary 1. And if we have been thorough enough, we should expect that the conjunction of all five properties be sufficient a condition for eliminating that failure altogether. This turns out to be the case.

Theorem 4. If C 1 , ε 1 and C 2 , ε 2 are generable, then h is a homomorphism from C 1 , ε 1 to C 2 , ε 2 if and only if h is a homomorphism from the L- labelled transition coalgebra C 1 , η(C 1 ) • ε 1 to the L-labelled transition coalgebra C 2 , η(C 2 ) • ε 2 . Corollary 2. If C 1 , ε 1 and C 2 , ε 2 are generable, then B is a bisimulation between C 1 , ε 1 and C 2 , ε 2 if and only if B is a bisimulation between the L- labelled transition coalgebra C 1 , η(C 1 ) • ε 1 and the L-labelled transition coalge- bra C 2 , η(C 2 ) • ε 2 .
Once more, we can translate all this back to the system side of the theory. Assume a binary relation T : S ↔ L × S.

We write E T (E) for a binary relation between S and S (L × S) such that for any s ∈ S and every e ∈ S (L × S), s E T (E) e ⇐⇒ either there is no l, s such that s T l, s , and e = , or there is l, s such that s T l, s , head e = l, s , and s E tail e. Proposition 11. E T (E) = rel G fun T (fun E).

We think of E T as a function on binary relations between S and S (L × S). And the reason that we are interested in this function is that it preserves the ordering of binary relations between S and S (L × S) induced by the inclusion relation on their graphs: for every binary relation

E 1 , E 2 : S ↔ S (L × S), if graph E 1 ⊆ graph E 2 , then graph E T (E 1 ) ⊆ graph E T (E 2 ) .
This ordering is of course a complete lattice, and hence, by Tarski's Latticetheoretical Fixpoint Theorem, so is the set of all fixed points of E T . We write exec T for the greatest fixed point of E T .

We say that T generates E if and only if exec T = E. We say that E is generable if and only if there is a binary relation between S and L × S that generates E. We say that S, E is generable if and only if E is generable. We would like to finish this section with a few remarks. Proposition 12 and Theorem 5 confirm what has been implicit throughout this section: generable labelled execution systems are just another representation of labelled transition systems. This is even more evident in the coalgebra side of the theory.

We write L-LEC gen for the category whose objects are all the generable L-labelled execution coalgebras, and arrows all the homomorphisms from one generable L-labelled execution coalgebra to another. Theorem 6. L-LEC gen and L-LTC are isomorphic.

Thus, for all practical purposes, generable labelled execution coalgebras are equivalent to labelled transition coalgebras.

In light of this equivalence, Theorem 3 does not just characterize generable labelled execution coalgebras. It marks the boundary between the expressive power of labelled transition coalgebras and labelled execution coalgebras. And what it implies is that there is no sense in choosing the latter over the former, unless we are willing to give up one or more of the five properties listed in the respective clauses of Theorem 3.

Related Work

As already argued in the introduction, what Milner advocated was a dichotomy between causation and observation in the theory of concurrency. But the expansion law, and its reckless use with agents with infinite behaviours, skewed that dichotomy into a controversy between so-called "true concurrency" and interleaving semantics. And in the midst of that controversy, interleaving came to be thought of as no more than bounded indeterminacy. However, the real cause of this was not the expansion law per se, but the use of labelled transition systems as models of agent behaviour.

Rather than generalizing transition systems into executions ones, and obtain a modelling structure that can do justice to the notion of interleaving, and ultimately to the observational view, efforts were steered toward decorating the former with all kinds of different pieces of information that would alleviate the various deficiencies of that misrepresented notion of interleaving (e.g., see [START_REF] Boudol | Permutation of transitions: An event structure semantics for CCS and SCCS[END_REF][START_REF] Degano | A partial ordering semantics for CCS[END_REF][START_REF] Darondeau | Causal trees: Interleaving + causality[END_REF][START_REF] Boudol | Observing localities[END_REF][START_REF] João | A causality-based semantics for CCS[END_REF]). And more often that not, the result was a kind of modelling structure that could no longer claim adherence to the observational view. The few attempts that did use executions directly, at least those that we are aware of (see [START_REF] Darondeau | On the observational semantics of fair parallelism[END_REF], [START_REF] Darondeau | About fair asynchrony[END_REF]), were not concerned with organizing them into structures and looking at their branching properties, and anyway, seem to have received only scant attention.

The first place where we do see executions organized into structures is not process algebra, but temporal logic. These so-called "path structures" (see Section 3.1) are quite popular in the beginning. We do not see a formal concept of bisimulation for them, but there is definitely interest in their branching properties. The notions of suffix, fusion, and limit closure are all defined in connection with path structures. Eventually, they give way to Kripke structures, inherited from modal logic, and claimed to provide "a setting more appropriate to concurrency" (see [20, p. 152]). They do not, we think. But despite the voiced arguments for a separation between implementation and correctness issues in reasoning about concurrent programs (e.g., see [START_REF] Courcoubetis | Reasoning about fair concurrent programs[END_REF]), transitions remain in the lead role.

In [START_REF] Hennessy | The power of the future perfect in program logics[END_REF], Hennessy and Stirling introduce what appears to be the first type of labelled execution system in the literature. They call systems of that type general transition systems, and in their definition, demand not only suffix and fusion closure, but prefix closure as well, with the justification that it "also appears to be natural" (see [24, p. 27]). They also define a concept of extended bisimulation for such systems, which is basically the same as our canonically derived concept of bisimulation between labelled executions systems (see Definition 6). The focus in [START_REF] Hennessy | The power of the future perfect in program logics[END_REF] is in logic, and specifically, in a generalization of Hennessy-Milner Logic (see [START_REF] Hennessy | Algebraic laws for nondeterminism and concurrency[END_REF]) to general transition systems. But what is surprising is that no attempt is later made to apply the ideas of general transition systems and extended bisimulations to the semantics of processes.

More than ten years later, these ideas pop up in a "very rough and incomplete draft" of Aczel (see [START_REF] Aczel | A semantic universe for the study of fairness[END_REF]), who is aware of Hennessy's work in [START_REF] Hennessy | Axiomatising finite delay operators[END_REF], a precursor of [START_REF] Hennessy | The power of the future perfect in program logics[END_REF], but apparently, unaware of the work in [START_REF] Hennessy | The power of the future perfect in program logics[END_REF] (see footnote in [3, p. 3]). Aczel's intention is to apply the final universe approach of [START_REF] Aczel | Final universes of processes[END_REF] to the semantics of Milner's SCCS with finite delay (see [START_REF] Milner | A finite delay operator in synchronous CCS[END_REF]). The proposed type of structure is a generalized type of labelled transition system, where each state is equipped with the set of all infinite sequences of transitions "admissible" from that state. An added condition of "stability" makes structures of that type ultimately equivalent to the general transition systems of [START_REF] Hennessy | The power of the future perfect in program logics[END_REF], but only because the latter are prefix closed. Eventually, these structures are represented as coalgebras over Class, and [2, thm. 2.2] is used to prove the existence of a final coalgebra in the full subcategory of all such coalgebras that are "stable".

The only other place where we find these ideas applied to the semantics of processes is [START_REF] Thomas | A fully abstract presheaf semantics of SCCS with finite delay[END_REF]. The starting point is again Milner's SCCS with finite delay, and the structures used are practically the same as in [START_REF] Aczel | A semantic universe for the study of fairness[END_REF]. But the approach is purely categorical. Indeed, the main goal in [START_REF] Thomas | A fully abstract presheaf semantics of SCCS with finite delay[END_REF] is showing how much can be done within category theory alone.

Comparing [START_REF] Hennessy | The power of the future perfect in program logics[END_REF], [START_REF] Aczel | A semantic universe for the study of fairness[END_REF], and [START_REF] Thomas | A fully abstract presheaf semantics of SCCS with finite delay[END_REF] with our work here, there are two things that we think stand out and would like to mention. First, regarding the general idea underlying the concept of labelled execution system, we find that in all three of [START_REF] Hennessy | The power of the future perfect in program logics[END_REF], [START_REF] Aczel | A semantic universe for the study of fairness[END_REF], and [START_REF] Thomas | A fully abstract presheaf semantics of SCCS with finite delay[END_REF], the notion of indeterminate termination, and its use in modelling the behaviour of reactive systems, has been completely overlooked. This is easy to put right in [START_REF] Hennessy | The power of the future perfect in program logics[END_REF], where prefix closure is an added feature, but not so in [START_REF] Aczel | A semantic universe for the study of fairness[END_REF] and [START_REF] Thomas | A fully abstract presheaf semantics of SCCS with finite delay[END_REF], where the property is practically built into the structure of a system. And second, regarding the formalization of the idea, we believe that the present approach represents a great simplification, both conceptually and notationally, over what was done in all three of [START_REF] Hennessy | The power of the future perfect in program logics[END_REF], [START_REF] Aczel | A semantic universe for the study of fairness[END_REF], and [START_REF] Thomas | A fully abstract presheaf semantics of SCCS with finite delay[END_REF].

It should be emphasized that the precedence of [START_REF] Hennessy | The power of the future perfect in program logics[END_REF], [START_REF] Aczel | A semantic universe for the study of fairness[END_REF], and [START_REF] Thomas | A fully abstract presheaf semantics of SCCS with finite delay[END_REF] over our work here is not causal, only temporal. Our ideas were developed, and for the most part, worked out before any acquaintance with these studies. The above review was mainly driven by our curiosity to understand why ideas that in retrospect seem so natural have not found their way into the household of the average concurrency theorist. In the end, one can only speculate. One thing is certain though: if matters of pedagogy have played any role in this, transition semantics have definitely profited from it; for people like pictures, and execution systems are impossible to draw.

Conclusion

The purpose of this work was to introduce the concept of labelled execution system, a generalization of that of labelled transition system that we believe can better accommodate the needs of an observational approach to concurrency theory. And as we saw in Section 3.5, in order for the use of labelled execution systems over labelled transition systems to be justified, one or more of the five properties listed in the respective clauses of Theorem 3 must be given up. But as we saw in Section 3.3, if we want our systems to be "well behaved", the first two of them must be hold on to. Therefore, if we ignore the rather uninteresting nontriviality condition, we are left with having to give up limit closure, impossibility of indeterminate termination, or both.

In fact, giving up any of these two properties has its own merit. For example, giving up limit closure enables us to faithfully model the finite delay property, so intrinsically bound to the notion of asynchronous parallelism. And possibility of indeterminate termination provides us with the means of simulating the behaviour of a capricious environment that may at any time cease to produce input stimuli.

Returning to the discussion in our introduction, it is not hard to see how one could use Abrahamson systems to provide a model for Milner's CCS that avoided "explicating parallelism in terms of non-determinism", at least in the stronger sense of the expansion law, and to be sure, distinguished between the two sides of (2). The critical step is of course in the treatment of parallel composition as a fair merge operation over the executions of the individual systems under composition, which, however, does not seem to present any particular difficulty (e.g., see [START_REF] Park | On the semantics of fair parallelism[END_REF]), and can be fitted to different notions of fairness, such as, for example, weak and strong fairness (see [START_REF] Krzysztof | Apt and Ernst-Rüiger Olderog. Proof rules and transformations dealing with fairness[END_REF]). But if one is really serious about this endeavour, one must also allow for abstraction, whereby certain actions of an agent become unobservable. And this calls for a suitably weakened version of bisimilarity among labelled execution systems. An interesting question then is whether such a weaker version can be canonically obtained by the coalgebraic methods used here. If possible, this could lead, through Theorem 6, to a coalgebraic characterization of weaker versions of bisimilarity among labelled transition systems as well, a goal that has heretofore remained elusive.

a. 0

 0 | b.0 = a.b.0 + b.a.0 .

Proposition 2 .

 2 c if and only if l, c ∈ τ (c). The following are true: (a) s l --→ T s if and only if s l --→ fun T s ; (b) if C is a set, then c l --→ τ c if and only if c l --→ rel τ c .

  can now compose Pow with the endofunctor Seq •(L × Id) to obtain the endofunctor Pow • Seq • (L × Id) on Class, which assigns to every class C the class Pow Seq(L × C) = {S | S is a set, and S ⊆ Seq(L × C)} , and to every class function f :

Proposition 5 .

 5 The following are true: (a) s T e if and only if s fun T e; (b) if C is a set, then c ε e if and only if c rel ε e.

  (i) for every c, l, c , and e , if c ε l, c • e , then c ε e ; (ii) for every c, l, c , e 1 , and e 2 , if c ε l, c •e 1 and c ε e 2 , then c ε l, c •e 2 .

  Assume a class C. We write η(C) for a class function from Pow Seq(L × C) to Pow(L × C) such that for every S ∈ Pow Seq(L × C), η(C)(S) = {head s | s ∈ S and s = } .

( 1 )

 1 τ (c) = ∅ and e = ; (2) there is l, c , and e such that l, c ∈ τ (c) and e = l, c • e ; (ii) for every n ∈ ω, if tail n e = , then one of the following is true: (1) there is l and c such that τ (c ) = ∅ and tail n e = l, c ; (2) there is l, c , l , c , and e such that l , c ∈ τ (c ) and tail n e = l, c • l , c • e . We write gen τ for a class function from C to Pow Seq(L × C) such that for any c ∈ C, (gen τ )(c) = {e | e ∈ Seq(L × C) and e is a τ -orbit of c} . Assume a class function ε : C → Pow Seq(L × C).

Theorem 3 .

 3 ε is generable if and only if the following are true: (a) for every c, l, c , and e , if l, c • e ∈ ε(c), then e ∈ ε(c ); (b) for every c, l, c , e 1 , and e 2 , if l, c • e 1 ∈ ε(c) and e 2 ∈ ε(c ), then l, c • e 2 ∈ ε(c); (c) for any c ∈ C and every infinite sequence s, if for every n ∈ ω, there is e ∈ ε(c) such that for every k < n + 1, tail k e = and head tail k s = head tail k e , then s ∈ ε(c); (d) for every c and e, if e ∈ ε(c) and ∈ ε(c), then e = ; (e) for any c ∈ C, ε(c) = ∅.

  1 and S 2 , T 2 . Definition 2. A bisimulation between S 1 , T 1 and S 2 , T 2 is a binary relation B : S 1 ↔ S 2 such that for any s 1 and s 2 such that s 1 B s 2 , the following are true:

  1 and C 2 , τ 2 . Proposition 3. B is a bisimulation between C 1 , τ 1 and C 2 , τ 2 if and only if B is a binary class relation between C 1 and C 2 , and for any c 1 and c 2 such that c 1 B c 2 , the following are true:

  and only if B is a binary class relation between C 1 , ε 1 and C 2 , ε 2 , and for any c 1 and c 2 such that c 1 B c 2 , the following are true: (a) if c 1 ε1 e 1 , then there is e 2 such that c 2 ε2 e 2 and e 1 Seq(L × B) e 2 ; (b) if c 2 ε2 e 2 , then there is e 1 such that c 1 ε1 e 1 and e 1 Seq(L × B) e 2 . Proposition 6 is similar to Proposition 3. The difference is that the local check of correspondence of transitions has been replaced by a non-local test of agreement along entire executions. Assume L-labelled execution systems S 1 , E 1 and S 2 , E 2 . We say that s 1 and s 2 are bisimilar among S 1 , E 1 and S 2 , E 2 if and only if there is a bisimulation B between S 1 , E 1 and S 2 , E 2 such that s 1 B s 2 . Proposition 7. B is a bisimulation between S 1 , E 1 and S 2 , E 2 if and only if B is a bisimulation between the L-labelled execution coalgebras S 1 , fun E 1 and S 2 , fun E 2 .

Definition 6.

A bisimulation between S 1 , E 1 and S 2 , E 2 is a binary relation B : S 1 ↔ S 2 such that for any s 1 and s 2 such that s 1 B s 2 , the following are true:

(a) if s 1 E1 e 1 , then there is e 2 such that s 2 E2 e 2 and e 1 Seq(L × B) e 2 ; (b) if s 2 E2 e 2 , then there is e 1 such that s 1 E1 e 1 and e 1 Seq(L × B) e 2 .

  Proposition 12. The following are true: (a) trans exec T = T ; (b) if E is generable, then exec trans E = E. Proposition 13. S, E is generable if and only if the L-labelled execution coalgebra S, fun E is generable. Theorem 5. If S 1 , E 1 and S 2 , E 2 are generable, then B is a bisimulation between S 1 , E 1 and S 2 , E 2 if and only if B is a bisimulation between the L-labelled transition systems S 1 , trans E 1 and S 2 , trans E 2 .

For every set S, we write P S for the power set of S, namely the set of all subsets of S.

We write Class for the category whose objects are all the classes, and arrows all the class functions.

For every endofunctor F on Class, we write F -Coalg for the category whose objects are all the F -coalgebras, and arrows all the homomorphisms from one F -coalgebra to another.

For every set S, we write S S for the sequence set of S, namely the set of all finite and infinite sequences over S.

The tacit assumption here is that the instantiated concept of bisimulation does indeed induce an equivalence concept, which is not always true (e.g., see[4, sec.

6]).

For every binary class relation R, we write dpr R for a class function from graph R to dom R such that for any c1, c2 ∈ graph R, (dpr R)( c1, c2 ) = c1, and cpr R for a class function from graph R to cod R such that for any c1, c2 ∈ graph R, (cpr R)( c1, c2 ) = c2. We call dpr R the domain projection map of R, and cpr R the codomain projection map of R.

Matsikoudis, Lee

Acknowledgement: We would like to thank the anonymous referees for their help in improving the presentation of this work.

This work was supported in part by the Center for Hybrid and Embedded Software Systems (CHESS) at UC Berkeley, which receives support from the National Science Foundation (NSF awards #0720882 (CSR-EHS: PRET), #1035672 (CPS: PTIDES), and #0931843 (ActionWebs)), the U. S. Army Research Office (ARO #W911NF-11-2-0038), the Air Force Research Lab (AFRL), the Multiscale Systems Center (MuSyC), one of six research centers funded under the Focus Center Research Program, a Semiconductor Research Corporation program, and the following companies: Bosch, National Instruments, Thales, and Toyota.


Pawe L Sobociński

Relational Presheaves as Labelled Transition Systems

We show that viewing labelled transition systems as relational presheaves captures several recently studied examples. This approach takes into account possible algebraic structure on labels. Weak closure of a labelled transition system is characterised as a left (2-)adjoint to a change-of-base functor.

A famous application of coalgebra [START_REF] Aczel | A final coalgebra theorem[END_REF][START_REF] Adamek | Introduction to coalgebra[END_REF] is as a pleasingly abstract setting for the theory of labelled transition systems (LTS). Indeed, an LTS is a coalgebra for the functor P(A × -), where A is the set of labels. LTSs are thus objects of the category of coalgebras for this functor. The arrows, in LTS terminology, are functional bisimulations. This category of coalgebras (modulo size issues) has a final object that gives a canonical notion of equivalence, although other approaches are available in general, see [START_REF] Staton | Relating coalgebraic notions of bisimulations[END_REF]. Ordinary bisimulations can be understood as spans of coalgebra morphisms. The coalgebraic approach has been fruitful: amongst many notable works we mention Turi and Plotkin's elegant approach to structural operational semantics congruence formats via bialgebras [START_REF] Turi | Towards a mathematical operational semantics[END_REF].

In another influential approach, Winskel and Nielsen [START_REF] Winskel | Presheaves as transition systems[END_REF] advocated the use of presheaf categories as a general semantic universe for the study of labelled transition systems. Morphisms turn out to be functional simulations, functional bi simulations can be characterised as open maps with respect to a canonical (via the Yoneda embedding) choice of path category [START_REF] Joyal | Bisimulation from open maps[END_REF]. Ordinary bisimulations are then spans of open maps, with some side conditions.

Both the coalgebraic approach and the presheaf approach have generated much subsequent research and have found several applications that we do not account for here. Concentrating on the theory of labelled transition systems, there are some limitations to both approaches. For example both take for granted that the set of labels A is monolithic and has no further structure. In fact, several labelled transition systems have "sets" of labels that are monoids [START_REF] Bruni | A connector algebra for P/T nets interactions[END_REF] or even categories [START_REF] Gadducci | The tile model[END_REF][START_REF] Leifer | Deriving bisimulation congruences for reactive systems[END_REF][START_REF] Mosses | Modular structural operational semantics[END_REF]. Such examples are more challenging to capture satisfactorily with the aforementioned approaches but some progress has been made-for instance, Bonchi and Montanari [START_REF] Bonchi | Reactive systems, (semi-)saturated semantics and coalgebras on presheaves[END_REF] captured labelled transition systems on reactive systems (in the sense of Leifer and Milner [24]) as certain coalgebras on presheaves.

There is also a certain mismatch between notions typically studied by concurrency theorists or researchers in the operational semantics of concurrent languages and the morphisms in categories of coalgebras or in presheaves. From the point of view of process theory, the morphisms in the aforementioned categories are not the notions typically studied: functional simulations and functional bisimulations1 instead of ordinary simulations and ordinary bisimulations.

Furthermore, the most natural notions of equivalence in applications are often weak (in the sense of Milner) and these tend to be technically challenging to capture in the coalgebra or presheaf settings. One can think of weak bisimulation as ordinary bisimulation on a labelled transition system that has been "saturated" with the silent τ -actions, but this is just another way of saying that τ is made the identity of a monoid of actions. Because the coalgebraic and presheaf approaches were not designed with a view to accommodate such algebraic structures on the set of labels, some work has to be performed in order to talk about weak equivalences, see for example [START_REF] Fiore | Weak bisimulation and open maps[END_REF][START_REF] Sokolova | Weak bisimulation for action-type coalgebras[END_REF].

In this paper we show that several recent examples of LTSs with algebraic structure can be seen as relational presheaves [START_REF] Rosenthal | The theory of Quantaloids[END_REF]. Relational presheaves are lax functors [START_REF] Kelly | Review of the elements of 2-categories[END_REF] (or, equivalently, morphisms of bicategories [START_REF] Bénabou | Introduction to bicategories, part 1[END_REF]) C op → Rel, where Rel is the locally partially ordered 2-category of relations. They have been called various names: specification structures [START_REF] Abramsky | Specification structures and propositionsas-types for concurrency[END_REF], relational variable sets [START_REF] Ghilardi | Relational and partial variable sets and basic predicate logic[END_REF], dynamic sets [START_REF] Stell | Granularity in change over time[END_REF], with several applications in Computer Science and related fields. Functors to Rel as a way of giving semantics to flowcharts were considered as early as 1972 by Burstall [START_REF] Burstall | An algebraic description of programs with assertions, verification and simulation[END_REF].

The typical examples of C that we shall consider will be monoids (i.e. categories with one object) and categories of contexts, in the sense of Leifer and Milner [24,[START_REF] Sobociński | Deriving process congruences from reaction rules[END_REF]. Ordinary A-labelled transition systems can be seen as instances of the former by considering the free monoid A * . A more interesting example where the label set is a non-free monoid is the LTS considered in [START_REF] Bruni | A connector algebra for P/T nets interactions[END_REF] or the LTSs that arise from expressions in the algebra of Span(Graph) [START_REF] Katis | Span(Graph): an algebra of transition systems[END_REF]. Weak derived LTS for reactive systems in the sense of Jensen [START_REF] Jensen | Mobile Processes in Bigraphs[END_REF], are examples of relational presheaves for C a category of contexts. Tile logics [START_REF] Gadducci | The tile model[END_REF] can also be seen as relational presheaves where C is not merely a monoid.

The morphisms of relational presheaves [START_REF] Rosenthal | The theory of Quantaloids[END_REF] are oplax natural transformations, and in the aforementioned examples these turn out to be ordinary simulations. This suggests the naturality of this abstract setting from the point of view of process theory. The fact that simulations are oplax natural transformations in a relational setting was observed by Jürgen Koslowski [START_REF] Koslowski | Simulations as a genuinely categorical concepts[END_REF].

Following Rosenthal, we denote the 2-category of relational presheaves by R * (C). Given relational presheaves h, h ∈ R * (C), morphisms h → h organise themselves in a sup-lattice and joins are preserved by composition, in other words R * (C) is a quantaloid [START_REF] Rosenthal | The theory of Quantaloids[END_REF]. Quantaloids have previously been used in the study of process equivalence by Abramsky and Vickers [START_REF] Abramsky | Quantales, observational logic and process semantics[END_REF]. Simulations and bisimulations have been investigated in the setting of categories enriched over quantaloids by Schmitt and Worytkiewicz [START_REF] Schmitt | Bisimulations of enrichments[END_REF].

The mathematical universe of relational presheaves with relational morphisms is rich. It is sometimes helpful to restrict to the subcategory of R * (C) with arrows the functional morphisms (i.e. functional simulations in the exam-ples). Following Rosenthal we shall refer to this category as R(C). Here, changeof-base functors u * always have left-adjoints and they have right-adjoints whenever u satisfies the weak factorisation lifting property [START_REF] Niefield | Change of base for relational variable sets[END_REF]. One consequence is that R(C) has limits that are computed pointwise.

Finally, and most importantly, several familiar constructions from the literature can be characterised as adjunctions. For example, we shall show that the weak-closure of a labelled transition system is actually a left (2-)adjoint to a change-of-base functor. In this sense, this paper continues the programme of [START_REF] Winskel | Models for concurrency[END_REF] in that category theory is used to clarify and distill constructions commonly used in the study of models of concurrency.

Examples

In order to motivate the more abstract developments we start here with a sightseeing tour of the examples that will turn out to be relational presheaves.

Example 1 (Ordinary labelled transition systems). A labelled transition system is a triple (X, A, T ) where T ⊆ X × A × X. The set X is called the statespace, A is a monolithic set of atomic actions and T is a set of transitions. We write x a -→ x for (x, a, x ) ∈ T . One way to describe such a structure using the coalgebraic approach is to use the functor P(A × -), where P is the (covariant) powerset endofunctor on Set. An LTS with label set A is a coalgebra for the P(A × -) Set-endofunctor, i.e. a function h :

X → P(A × X) (1)
There are several examples where the set A has more structure, in particular, when it's a monoid or even the set of arrows of a category. We list some of these examples below.

Example 2 (Weak labelled transition systems). Consider a special "silent" action τ that we intend to be unobservable. Define a weak LTS to be (X, A + {τ }, T ) where the set T of transitions is reflexive-transitive closed wrt to τ s, i.e. it is closed under the rules below

P τ -→ P P τ -→ Q Q a -→ R R τ -→ S P a -→ S (2)
It is easy to show that bisimilarity and weak bisimilarity coincide on a weak LTS. A weak LTS can be obtained from an LTS with τ -labels via reflexive-transitive τ -closure. In this paper we shall show that this construction arises as a left adjoint to a change-of-base functor (Lemma 12).

Example 3 (Monoidal structure on labels). An LTS with monoidal structure on labels is (X, M, T ) where M is a monoid with multiplication and unit ι, and where the set T of transitions is closed under the following two rules:

P ι - → P P a -→ Q Q b - → R P a b --→ R (3)
Notice that such LTSs are actually examples of categories, with objects the states, identities ι, and composition given by . See [START_REF] Bruni | A connector algebra for P/T nets interactions[END_REF] for a recent example of such an LTS in concurrency theory literature.

Example 4 (Contexts as labels). The contexts-as-labels approach was introduced by Leifer and Milner [24] and developed further in [START_REF] Bonchi | Saturated semantics for reactive systems[END_REF][START_REF] Bonchi | Reactive systems, (semi-)saturated semantics and coalgebras on presheaves[END_REF][START_REF] Sassone | Deriving bisimulation congruences using 2categories[END_REF][START_REF] Sassone | Locating reaction with 2-categories[END_REF]. Here we give only a very brief summary: suppose that C is a (2-)category with objects interfaces and arrows contexts; see [START_REF] Sobociński | Deriving process congruences from reaction rules[END_REF] for a number of concrete examples. There is a chosen object 0 as the ground interface, arrows with domain 0 are then the ground terms. Given a set of reaction-rules, which is a set of pairs of arrows r, r : 0 → X one generates a reaction relation by closing the rules with respect to reactive contexts: the arrows of a subcategory D of C. Then one can derive an LTS that has transitions of the form t c -→ t where t : 0 → X, c : X → Y , t : 0 → Y such that c • t t and c is the smallest context that makes this reduction possible. The notion of smallest is typically captured via a universal property, in C, of relative (local) pushouts.

Jensen [START_REF] Jensen | Mobile Processes in Bigraphs[END_REF]Definition 3.18] introduced the notion of weak bisimilarity for reactive systems (see also [START_REF] Bruni | Deriving weak bisimulation congruences from reduction systems[END_REF]), a construction that for every reactive system R with all RPOs, gives a reactive system W(R). The intuition is that reactions are composed to form reactions in W(R): for example (r, r ) and (s, s ) are composed to (p • r, q • s ) where p • r and q • s form an RPO, and "identity" reactions (r, r) are added for all r. Bisimilarity on the LTS derived from W(R) acts as a kind of weak bisimilarity in examples. We omit the details here and just mention two properties that are satisfied by this LTS:

1. u id -→ u for all u ∈ C, 2. if u a -→ v and v b - → w then u a;b --→ w.
Both are a consequence of [START_REF] Jensen | Mobile Processes in Bigraphs[END_REF]Lemma 3.2].

Example 5 (Tile systems). Tile systems [START_REF] Gadducci | The tile model[END_REF] are double categories, in which the vertical dimension can be viewed as (double) labelled transitions between the arrows of the horizontal category, considered as the statespace. The vertical dimension forms a category, and hence this labelled transition system is closed under composition and has identities.

LTSs: from coalgebras to relational presheaves

Seeing an LTS as a P(A × -) coalgebra (1) emphasises the statespace but wraps the labels within the definition of the functor. In order to consider possible extra structure of A we need to bring the labels out as first class citizens so:

h : X → P(A × X) h : X → P(X) A h : A → P(X) X (4)
That is, to give a standard P(A × -) coalgebra is to give an A-indexed family of P(-) coalgebras.

For the sequel, it makes sense to use the fact that P is a monad, and in particular we can use the composition in the Kleisli category Kl(P). 2 We can replace the conclusion of (4) by:

h : A → Kl(P)(X, X) (5)
If A is a monoid, then h should preserve the structure in some way. But, first, monoids are exactly one-object categories. So for a general category C, (5) generalises to a mapping h : C → Kl(P)

We shall now elucidate what properties the mapping (6) ought to satisfy. Of course, Kl(P) is another name for Rel, the locally partially ordered 2-category with objects sets, arrows relations and 2-cells inclusions.

A natural choice for ( 6) is that of relational presheaf, that is a lax functor from C op to Rel:

h : C op → Rel (7)
The laxness here means that:

h(b); h(a) ⊆ h(a; b) id h(x) ⊆ h(id x ) (8)
Morphisms of ϕ : h → h of relational presheaves C op → Rel are oplax natural transformations [START_REF] Ghilardi | Relational and partial variable sets and basic predicate logic[END_REF][START_REF] Niefield | Change of base for relational variable sets[END_REF]. This means, for each C ∈ C a relation ϕ C : h(C) / / h (C) such that the (lax) naturality condition is satisfied for each f : D → C in C, i.e.:

hC ϕ C / / hf _ h C h f _ hD ⊆ ϕ D / / h D (9)
The 2-category with objects relational presheaves and morphisms as above3 will be denoted R * (C). The subcategory with functional morphisms; those ϕ : h → h where ϕ C in ( 9) is a function4 for all C ∈ C will be denoted R(C). Taking a reactive system R with category of contexts C, the derived LTS on W(R) [START_REF] Jensen | Mobile Processes in Bigraphs[END_REF] is a relational presheaf. This is a direct consequence of [START_REF] Jensen | Mobile Processes in Bigraphs[END_REF]Lemma 3.22].

Proposition 8. Given a category of contexts C with all relative pushouts and a set of reaction rules R, the derived LTS on W(R) is a relational presheaf R * (C).

Similarly, taking C to be the product of the vertical category of any tile system with itself allows (the LTS generated by) any tile system to be considered as a relational presheaf.

Relational presheaves as labelled transition systems

The familiar Grothendieck construction instantiated to relational presheaves yields categories, which we can consider as LTSs. Definition 9. Let h : C op → Rel be a relational presheaf. Then the labelled transition system Γ (h) has: states: pairs (C, x) where C ∈ C and x ∈ h(C)

transitions: (C, x) f -→ (D, y) if C f -→ D is in C and x ∈ h(f )(y).
As a consequence of (8), Γ (h) is closed under the rules of (3). Indeed, if C has one object then Γ (h) is an LTS with a monoidal structure on labels, in the sense of Example 3.

Proposition 10. Morphisms ϕ : h → h are in a 1-1 correspondence with sim- ulations from Γ (h) to Γ (h ).
Niefield [START_REF] Niefield | Change of base for relational variable sets[END_REF] amongst other authors have studied R(C) and we can use some of the rich theory of relational presheaves to yield insights about the examples that we have identified. An example is the following result. Proposition 1. Limits exist and are computed pointwise in R(C).

Proof. Corollary 3.2 in [START_REF] Niefield | Change of base for relational variable sets[END_REF]. Now R * (C) is a locally partially-ordered 2-category, with natural transformations ordered pointwise by inclusion (these are the modifications [START_REF] Kelly | Review of the elements of 2-categories[END_REF] in this simple setting). It is well-known that the hom-posets of R * (C) are complete suplattices 5 and this is the generalisation of the fact that simulations are closed under unions. Proof. We give the proof of this well-known result only to give the flavour of the relational calculus that is used when manipulating morphisms of R * (C). Suppose that {ϕ i } i∈I is a family of morphisms from h to h in R * (C). It suffices to show that i∈I ϕ i is a morphism, i.e. that the naturality condition (9) holds. Indeed hf ;

i∈I ϕ i D = i∈I hf ; ϕ i D ⊆ i∈I ϕ i C ; h f = ( i∈I ϕ i C ); h f.

Weak labelled transition systems

Consider an LTS with silent τ labels. Closing wrt to rules (2), considering τ as the monoid identity and forming the traces yields a relational presheaf. This is technically somewhat similar to the approaches advocated in [START_REF] Ribeiro | Harnessing Theories for Tool Support in Software (TTSS '07)[END_REF] and [START_REF] Fiore | Weak bisimulation and open maps[END_REF]. We shall now make this construction precise and characterise it with a universal property.

Let A τ def = A + {τ }. There is a function on sets A τ → A * that sends each a ∈ A to itself (considered as a word of length one) and τ to . This extends to a morphism of monoids by freeness

u : A * τ → A * (10)
that yields a change-of-base functor u * : R * (A * ) → R * (A * τ ). In terms of LTSs, it is easy to see that u * acts by closing a transition system with actions in A * by the following rule, and on arrows (simulations) as identity.

P - → Q P τ -→ Q (11)
The left adjoint Σ u : R * (A * τ ) → R * (A * ) can be understood in this particular case as first closing an LTS wrt to rules (2) and then renaming τ to .

Lemma 12. There is a 2-adjunction

R * (A * τ ) Σu * * ⊥ R * (A * ) u * j j (12)
where Σ u can be understood on objects as closing an LTS wrt to the rules (2) and renaming τ to . On arrows Σ u acts as identity .

Proof. We define Σ u on objects as first forming the closure under (2) and then renaming τ to . On arrows Σ u is the identity. Now if h is an LTS on A * τ then it is easy to check that the identity relation on the statespace is a simulation from h to u * Σ u h. Also, if g is an LTS on A * then again the identity function is a simulation from Σ u u * g to g. These two families of simulations are natural transformations. The triangle equalities thus trivially hold.

The definition of Σ u gives us a concise way to capture weak simulation-a relation ϕ : h / / h , where h, h ∈ R * (A * τ ) is a weak simulation precisely when it is defines an arrow ϕ :

Σ u h / / Σ u h in R * (A * ).
Proposition 13. The category of (ordinary) labelled transition systems with label set A τ and weak simulations is the category with objects those of LT S(A τ ) (the full subcategory of R * (A * τ ) with objects ordinary functors) and morphisms h to h given by R * (A * )(Σ u (h), Σ u (h )).

Restricting to the subcategories with functional morphisms, u defined in [START_REF] Burstall | An algebraic description of programs with assertions, verification and simulation[END_REF] satisfies the weak factorisation lifting property and hence u * also has a right adjoint Π u : R(A * τ ) → R(A * ) [START_REF] Niefield | Change of base for relational variable sets[END_REF]Theorem 4.1]. In terms of LTS terminology, Π u maps an ordinary LTS L = (X, A τ , T ) to the following LTS with labels in A:

states: those x ∈ X for which x τ -→ x in L transitions: the non-τ transitions of L.

Π u (h) can thus be understood as the largest τ -reflexive sub-LTS, restricted to the non-τ actions. It is not difficult to verify that the Π u defined in this way is a right adjoint to u * .

Conclusions and future work

We have observed that several examples of labelled transition systems, especially when there is algebraic structure on labels, can be considered as relational presheaves. The morphisms between such LTSs are simulations and the resulting categories of LTSs have rich structure due to their mathematical status. As an example, we characterised weak closure as a left adjoint to a change-of-base functor.

There are several future directions. The theory of bisimulation needs to be developed: in the examples that we have examined bisimulations are those morphisms that remain morphisms when reversed via the underlying involution in Rel, it remains to be seen whether this view is fruitful in the wider, general picture. For example, it is of interest that functional bisimulations in our examples can be characterised as maps in R * (C), that is, those 1-cells which have a right adjoint in the 2-categorical sense.

There are several other settings in which there is an obvious monoidal structure on labels. One example is reversible transition systems where standard constructions [START_REF] Danos | Reversible communicating systems[END_REF][START_REF] Danos | General reversibility[END_REF] may be characterised as universal when viewed as relational presheaves.

Morphisms in R * (C), change-of-base functors and their adjoints give a general approach to defining simulations (amongst other equivalences), morphisms and canonical constructions in models where such notions have not been obvious; for example in the theory of reactive systems. Finally, Rel can be generalised to Span and other (bi)categories, yielding more general notions of labelled transition systems.

Proposition 6 .Proposition 7 .

 67 Now back to examples. Consider C to be a category with one object, i.e. a monoid (M, , ι). To give an LTS with a monoidal structure on labels (Example 3) is to give a relational presheaf, i.e. an object of R * (M ). Morphisms of R * (M ) are precisely the simulations between such LTSs.Any ordinary LTS (Example 1) can be considered a relational presheaf by taking C = A * and considering the LTS of traces. Not all relational presheaves in R * (A * ) are ordinary labelled transition systems in the sense of Example 1. For instance, in a general relational presheaf in R * (A * ) there can be transitions p -→ q for p = q and transitions p ab -→ p without an intermediate p such that p a -→ p and p b -→ p . Ordinary LTSs with labels in A form the full subcategory of R * (A * ) with objects the (ordinary) functors, which we will refer to as LTS(A). To give an ordinary LTS with label set A (Example 1) is to give a functor (A * ) op → Rel. Let LT S(A) denote the corresponding full subcategory of R * (A * ). The morphisms of LTS(A) are thus the simulations.

Lemma 11 .

 11 The local partial-orders of R * (C) are complete sup-lattices.

Although Hughes and Jacobs[START_REF] Hughes | Simulations in coalgebras[END_REF] have also studied simulation coalgebraically.

Jacobs, Hasuo and Sokolova have used coalgebras in Kleisli categories in order to consider trace semantics coalgebraically[START_REF] Hasuo | Generic trace semantics via coinduction[END_REF][START_REF] Jacobs | Trace semantics for coalgebras[END_REF].

Rosenthal [28] calls these generalized rp-morphisms.

These are Rosenthal's rp-morphisms.

More succinctly, R * (C) are quantaloids, see[START_REF] Rosenthal | The theory of Quantaloids[END_REF].

Acknowledgment. Thanks go to Bartek Klin for several useful discussions and to Tom Hirschowitz, Jürgen Koslowski and the anonymous referees for several important suggestions.