BRICS RS-96-2 Cheng & Nielsen: Open Maps, Behavioural Equivalences, and Congruences

BRICS

Basic Research in Computer Science

Open Maps, Behavioural Equivalences, and Congruences

Allan Cheng Mogens Nielsen

BRICS Report Series RS-96-2 ISSN 0909-0878 January 1996 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1996, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through WWW and anonymous FTP:

http://www.brics.dk/
ftp ftp.brics.dk (cd pub/BRICS)

Open Maps, Behavioural Equivalences, and Congruences^{⋆}

Allan Cheng and Mogens Nielsen

BRICS^{⋆⋆}, Department of Computer Science, Building 540, Ny Munkegade

University of Aarhus, Aarhus 8000 C, Denmark

                e-mail: {acheng,mn}@daimi.aau.dk

Abstract. Spans of open maps have been proposed by Joyal, Nielsen, and Winskel as a way of adjoining an abstract equivalence, P-bisimilarity, to a category of models of computation M, where P is an arbitrary subcategory of observations. Part of the motivation was to recast and generalise Milner’s well-known strong bisimulation in this categorical setting. An issue left open was the congruence properties of P-bisimilarity. We address the following fundamental question: given a category of models of computation M and a category of observations P, are there any conditions under which algebraic constructs viewed as functors preserve P-bisimilarity? We define the notion of functors being P-factorisable, show how this ensures that P-bisimilarity is a congruence with respect to such functors. Guided by the definition of P-factorisability we show how it is possible to parametrise proofs of functors being P-factorisable with respect to the category of observations P, i.e., with respect to a behavioural equivalence.

Keywords: Open maps, P-bisimilarity, P-factorisability, congruences, process algebra, category theory.

1 Introduction

Category theory has proven itself very useful in many fields of theoretical computer science. We mention just one example which is directly related to the work presented in the following sections. In [JNW93], Joyal, Nielsen, and Winskel have used category theory to propose an abstract way of capturing the notion of bisimulation, the so-called spans of open maps: first, a category of models of computations M is chosen, then a subcategory of observations P is chosen relative to which open maps are defined. Two models are P-bisimilar if there exists a span of open maps between them. In [CN95, NC95] the present authors give examples of application of the theory.

⋆ This work has been supported by The Danish Research Foundation, The Danish Research Academy, and BRICS. A short version of this paper will appear in the proceedings of CAAP ’96.

⋆⋆

Basic Research in Computer Science, Centre of the Danish National Research Foundation.

Winskel and Nielsen have presented operators of CCS-like process algebras using category-theoretic concepts such as products and co-products [WN95]. A natural question to ask is whether or not it is also possible to capture the following important aspect of process algebraic operators and bisimulation equivalences: when is P-bisimilarity a congruence with respect to some of these operators?

Based on the view that endofunctors on M may be seen as abstract operators we define a natural and general notion of a functor being P-factorisable. We then show that a P-factorisable functor must preserve P-bisimilarity. We observe an apparent similarity with the idea behind Milner’s proofs that CCS operators preserve strong bisimulation.

Common to much work on behavioural equivalences being congruences is that one chooses a specific (a) process term language, (b) class of models, and (c) behavioural equivalence. One then shows that specific operators—such as “parallel composition” and “nondeterministic choice”—preserve the proposed behavioural equivalence. Well-known examples are [Hen88, Mil89]. The behaviour of their process algebras is given by a structural operational semantics (SOS) [Plo81], in which the behaviour of a composite process term is given by the behaviour of its components.

In general, the term languages resemble each other, usually CCS-like, and hence the results differ from each other primarily with respect to the proposed equivalences. Based on this observation, one might look for general results.

One approach could be not to look at specific operators, but try to reason about a general set of operators. In [BIM88], Bloom, Istrail, and Meyer study a meta-theory for process algebras which are defined by SOS rule systems. They identify a rule format which ensures that any process language in so-called GSOS format has strong bisimulation as a congruence. It is worth noticing that they fix the notion of behavioural equivalence, strong bisimulation, and obtain general results by allowing the operators in the language to vary.

Based on the notion of P-factorisability, we choose an approach “orthogonal” to that of [BIM88]. The presentation of P-factorisability focusses, especially, on certain closure properties of the category P. Based on this observation, we show how one can parametrise the proofs of functors being P-factorisable with respect to the choice of the observation category P, i.e., the choice of a behavioural equivalence. Intuitively, we fix the operators, but allow the behavioural equivalence to vary. Then we identify conditions on P which ensure that the varying equivalences are congruences with respect to the operators. Hence, our results can be seen as “orthogonal” to that of Bloom, Istrail, and Meyer, in that we can parametrise with respect to the behavioural equivalences, as opposed to operators, [BIM88].

In the next section we recall Joyal, Nielsen, and Winskel’s theory of open maps. In Sec. 3 we present our notion of P-factorisability. Then, in Sec. 4 we apply our theory to a variant of Winskel and Nielsen’s labelled transition systems [WN95]. We consider the universal constructions from [WN95] and provide general “congruence” results parametrised by the category of observations P.

We then continue by examining the trickier recursion operator in Sec. 5. Finally we conclude and give suggestions for further research in Sec. 6.

2 Open Maps

In this section we briefly recall the basic definitions from [JNW93]. We present a slightly more general definition since it turns out more beneficial, more specifically for Theorem 30 and the discussion in Sect. 4.8.

Let U denote a category, the universe. A morphism m : X ⟶ Y in U should intuitively be thought of as a simulation of X in Y. Then, a subcategory of U which represents a model of computation has to be identified. We denote this category M. Also, within U, we choose a subcategory of “observation objects” and “observation extension” morphisms between these objects. We denote this category of observations by P. If nothing else is mentioned, we assume that U = M, corresponding to the definitions in [JNW93].

Given an observation (object) O in P and a model X in M, then O is said to be an observable behaviour of X if there exists a morphism p : O ⟶ X in M. We think of p as representing a “run” of O in X. We shall use O, O′, … to denote observations and T, T′, X, Y, … to denote objects from M. A morphism O ⟶^{q} O′ is implicitly assumed to belong to P.

Next, we identify morphisms m : X ⟶ Y in M which have the property that whenever an observable behaviour of X can be extended via f in Y then that extension can be matched by an extension of the observable behaviour in X.

Definition 1. Open Maps A morphism m : X ⟶ Y in M is said to be P-open (or just an open map) if whenever f : O_{1} ⟶ O_{2} in P, p : O_{1} ⟶ X, q : O_{2} ⟶ Y in M, and the diagram

[figure: O_{1}; f; p; X; m; O_{2}; q; Y]  (1)

commutes, i.e., m ∘ p = q ∘ f, there exists a morphism h : O_{2} ⟶ X in M (a mediating morphism) such that the two triangles in the diagram

[figure: O_{1}; f; p; X; m; O_{2}; h; q; Y]  (2)

commute, i.e., p = h ∘ f and q = m ∘ h. When no confusion is possible, we refer to P-open morphisms as open maps. □

The abstract definition of bisimilarity is as follows.

Definition 2. P-bisimilarity Two models X and Y in M are said to be P-bisimilar (in M), written X ∼_{P} Y, if there exists a span of open maps from a common object Z:

[figure: Z; m; m′; X; Y]  (3)

□

Remark. Notice that if M has pullbacks, it can be shown that ∼_{P} is an equivalence relation. The important observation is that pullbacks of open maps are themselves open maps. For more details, the reader is referred to [JNW93].

As a preliminary example of a category of models of computation M we present labelled transition systems.

Definition 3. A labelled transition system over Act is a tuple

(S, i, Act, ⟶) ,  (4)

where S is a set of states with initial state i, Act is a set of actions ranged over by α, β, …, and ⟶⊆ S × Act × S is the transition relation. For the sake of readability we introduce the following notation. Whenever (s_{0}, α_{1}, s_{1}),

(s_{1}, α_{2}, s_{2}), …, (s_{n−1}, α_{n}, s_{n}) ∈⟶ we denote this as s_{0} ⟶^{α_{1}} s_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} s_{n}

or s_{0} ⟶^{v} s_{n}, where v = α_{1}α_{2} ⋯ α_{n} ∈ Act^{∗}. Also, we assume that all states s ∈ S are reachable from i, i.e., there exists a v ∈ Act^{∗} such that i ⟶^{v} s. □

Let us briefly remind the reader of Park and Milner’s definition of strong bisimulation [Mil89].

Definition 4. Let T_{1} = (S_{1}, i_{1}, Act, ⟶_{1}) and T_{2} = (S_{2}, i_{2}, Act, ⟶_{2}). A strong bisimulation between T_{1} and T_{2} is a relation R ⊆ S_{1} × S_{2} such that

(i_{1}, i_{2}) ∈ R ,  (5)
((r, s) ∈ R ∧ r ⟶^{α}_{1} r′) ⇒ for some s′, (s ⟶^{α}_{2} s′ ∧ (r′, s′) ∈ R) , (6)
((r, s) ∈ R ∧ s ⟶^{α}_{2} s′) ⇒ for some r′, (r ⟶^{α}_{1} r′ ∧ (r′, s′) ∈ R) . (7)

T_{1} and T_{2} are said to be strongly bisimilar if there exists a strong bisimulation between them. □

Henceforth, whenever no confusion is possible we drop the indexing subscripts on the transition relations and write ⟶, instead.

By defining morphisms between labelled transition systems we can obtain a category of models of computation, TS_{Act}, labelled transition systems.

Definition 5. Let T_{1} = (S_{1}, i_{1}, Act, ⟶_{1}) and T_{2} = (S_{2}, i_{2}, Act, ⟶_{2}). A morphism m : T_{1} ⟶ T_{2} is a function m : S_{1} ⟶ S_{2} such that

m(i_{1}) = i_{2} ,  (8)
s ⟶^{α}_{1} s′ ⇒ m(s) ⟶^{α}_{2} m(s′) .  (9)
□

The intuition behind this specific choice of morphism is that an α-labelled transition in T_{1} must be simulated by an α-labelled transition in T_{2}. Composition of morphisms is defined as the usual composition of functions.

By varying the choice of P we can obtain different behavioural equivalences, corresponding to P-bisimilarity. E.g., if, as done in [JNW93], we choose P_{M} as the full subcategory of TS_{Act} whose objects are finite synchronisation trees with at most one maximal branch, i.e., labelled transition systems of the form

i ⟶^{α_{1}} s_{1} ⟶^{α_{2}} ⋯ ⟶^{α_{n}} s_{n} ,  (10)

where all states are distinct, we get:

Theorem 6. [JNW93] P_{M}-bisimilarity coincides with Park and Milner’s strong bisimulation.

By slightly restricting our choice of observation extension so that P_{H} is the subcategory of TS_{Act} whose objects (observations) are of the form (10), and whose morphisms are the identity morphisms and morphisms whose domains are observations having only one state (the empty word), we get:

Theorem 7. [NC95] P_{H}-bisimilarity coincides with Hoare trace equivalence.

In [NC95] other behavioural equivalences were considered, e.g., weak bisimulation and probabilistic bisimulation.

3 P-Factorisability

In this section we propose the notion of P-factorisability. We start by a motivating example and continue with some category theoretical preliminaries, which notationally eases the presentation of P-factorisability.

3.1 An Example

Consider M = TS_{Act} and P = P_{M} from Sec. 2 and the transition systems below, which we denote—left to right—T_{1}, …, T_{5}. The initial states are depicted as ⊙.

[figure: ⊙; α; ⊙; α; ⊙; γ; ⊙; α; γ; ·; α; β̄; ·; α; ⊙; α; γ; ·; α; β̄; ·; α; ·; β; β; ·; β; ·; β̄; ·; β; γ; β; ·; β; β̄; β; τ; τ; ·; β; β; ·; β; γ; ·; β; β̄; τ; ·; β; ·; ·; ·; ·; ·; γ; ·; β̄; ·; ·; γ; ·; β̄; ·; ·; γ; ·; β̄; ·]

T_{1} is strongly bisimilar (P-bisimilar) to T_{2}. In fact, there is an obvious open map k from T_{1} to T_{2}. Considering T_{3} to be fixed, we can define a functor ∥T_{3} : M ⟶ M, where ∥ acts as a CCS-like parallel composition. T_{4} = T_{1}∥T_{3} and T_{5} = T_{2}∥T_{3} serve as an informal illustration of ∥T_{3}, when applied to T_{1} and T_{2}, respectively. In much the same way as Milner [Mil89] shows that P ∼ P′ implies P ∥ Q ∼ P′ ∥ Q, we would like to conclude that if k : T_{1} ⟶ T_{2} is open, then so

is T_{1}∥T_{3} ⟶^{k∥T_{3}} T_{2}∥T_{3}. ^{3}

Recall that P-bisimilarity is based on open maps, which again are based on observations from P. E.g., we can observe O, the behaviour ⊙ ⟶^{α} · ⟶^{γ} ·, in T_{4} and—via k∥T_{3} : T_{4} ⟶ T_{5}—in T_{5}. Some of these transitions in T_{4}, here only the α transition, are due to transitions “from” T_{1}. Using k, we conclude that the α transition in O must also be observable in T_{2}. In fact, we have a commuting diagram as in (1) with X = T_{4}, Y = T_{5}, O_{1} = O_{2} = O, m = k∥T_{3}, and f = 1_{O}, and by the above we have extracted a second commuting diagram of the form

(1) with X = T_{1}, Y = T_{2}, O_{1} = O_{2} = O′ = ⊙ ⟶^{α} ·, and m = k.

The way we have “factored” O into O′ is consistent with ∥T_{3} in the following sense: there exists a commuting diagram of the form

3 In fact, just as Milner uses a bisimulation P ∼ P′ to exhibit a bisimulation P ∥ Q ∼ P′ ∥ Q, we will “factor” the observation ⊙ ⟶^{α} · ⟶^{γ} · into transitions from T_{3} and from T_{1} and T_{2}, respectively. This will guide us to the mediating morphism required in (2).

[figure: O; O′∥T_{3}; T_{1}∥T_{3}; O; O′∥T_{3}; T_{2}∥T_{3}]

In the next section, we formalise this by defining the notion of P-factorisability, and, as a consequence, we will be able to conclude that k∥T_{3} is an open map.

3.2 Categorical Preliminaries

Given a category C with objects C_{0} and morphisms (arrows) C_{1}, let Ĉ be the category whose objects are C_{1} and whose morphisms represent commuting diagrams, i.e., there is a morphism (h_{1}, h_{2}) from f to g if

[figure: ·; f; h_{1}; ·; g; ·; h_{2}; ·]  (11)

is a commuting diagram in C. Composition of morphisms is defined component-

wise. For notational convenience we may “hat” objects and morphisms from Ĉ, e.g., X̂ and m̂. When convenient, we will denote objects from Ĉ as morphisms from C, e.g., X̂ might be denoted f.

Notice that a functor F : C ⟶ D induces a functor F̂ : Ĉ ⟶ D̂, which sends an object X̂ to F (X̂) and a morphism m̂ = (m_{1}, m_{2}) to (F (m_{1}), F (m_{2})).

3.3 Factorising Observations

Definition 8. P-factorisability A functor F : M ⟶ M is said to be P-factorisable if whenever we have an

object Ô in P̂, an object X̂ in M̂, and a morphism Ô \underrightarrow{_{q}} F̂(X̂) in M̂, then

there exist an object Ô_{1} in P̂ and morphisms Ô \underrightarrow{_{q^{⋆}}} F̂(Ô_{1}) and Ô_{1} \underrightarrow{_{q^{#}}} X̂ in M̂ such that the diagram

[figure: Ô; _{q}; _{q^{⋆}}; F̂(Ô_{1}); _{F}(_{q^{#}}); F̂(X̂)]  (12)

commutes in M̂. □ Definition 9. A functor F : M ⟶ M is a P-operator if it is P-bisimilarity preserving, i.e., if A is P-bisimilar to B, then F (A) is P-bisimilar to F (B). □ Theorem 10. Any P-factorisable functor F : M ⟶ M is a P-operator. Proof. It is sufficient to show that F preserves open maps. Assume m : X ⟶ X′ is an open map and we are given a commuting diagram

[figure: O; f; q; F (X); F (m); O′; q′; F (X′)]

with q and q′ in M. This diagram is a morphism Ô \underrightarrow{_{q}} F̂(X̂) in M̂. By Pfactorisability there exist Ô_{1} in P̂ and morphisms Ô \underrightarrow{_{q^{⋆}}} F̂(Ô_{1}) and Ô_{1} \underrightarrow{_{q^{#}}} X̂ in M̂ such that (12) commutes. Denote Ô as f : O ⟶ O′, q̂ as (q, q′), Ô_{1} as m_{1} : O_{1} ⟶ O′_{1}, q̂^{⋆} as (q^{⋆}, q^{′⋆}), X̂ as m : X ⟶ X′, and q̂^{#} as (q^{#}, q^{′#}). Since Ô_{1} \underrightarrow{_{q^{#}}} X̂ represents a commuting diagram and m was open, there exists a morphism p : O′_{1} ⟶ X such that the diagram

[figure: O; f; q^{⋆}; F (O_{1}); F (m_{1}); F (q^{#}); F (X); F (m); O′; q^{′⋆}; F (O′_{1}); F (q^{′#}); F (p); F (X′)]

must commute (by (12)). But then

q = F (q^{#}) ∘ q^{⋆} , by (12)
= F (p) ∘ F (m_{1}) ∘ q_{⋆}
= (F (p) ∘ q^{′⋆}) ∘ f ,

and

q′ = F (q^{′#}) ∘ q^{′⋆} , by (12)
= F (m) ∘ (F (p) ∘ q^{′⋆}) .

We conclude that F (m) is open. Hence if X ⟵^{m} Z ⟶^{n} Y is a span of open maps, F (X) ⟵^{F (m)} F (Z) ⟶^{F (n)} F (Y) is a span of open maps.

4 Application, an Example

As an example of the application of the theory we consider the category TS of labelled transition systems^{4} from [WN95]. As it is shown there, process-language constructs can be interpreted as universal constructions in TS. In the following subsections, we show how our theory can be applied to the functors associated to these universal constructions.

4.1 The Category of Labelled Transition Systems

In this section we define the category TS inspired by [WN95].

Definition 11. The category TS has as objects (S, i, L, ⟶), labelled transition systems (lts) with labelling set L. We require that all states in S be reachable (from the initial state i). □

We shall use the abbreviation T_{j} for (S_{j}, i_{j}, L_{j}, ⟶_{j}). If clear from the context we will omit the subscript j. Also, all the following constructions do produce ltss in TS, i.e., all states are reachable.

For technical reasons we assume the existence of a special element ∗ which is not member of any labelling set. A partial function λ between two labelling sets L and L′ can then be represented as a total function from L∪{∗} to L′∪{∗} such that ∗ is mapped to ∗. If a ∈ L is mapped to ∗, we interpret this as meaning that λ is undefined on a. Overloading the symbol λ, we shall write this as λ : L ↪ L′. Given T = (S, i, L, ⟶), we define ⟶_{∗} to be the set ⟶ ∪{(s, ∗, s) | s ∈ S}. The transitions (s, ∗, s) are called idle transitions.

Definition 12. A morphism m : T_{0} ⟶ T_{1} is a pair f = (σ_{m}, λ_{m}), where σ_{m} : S_{0} ⟶ S_{1} and λ_{m} : L_{0} ↪ L_{1} are total functions such that

σ_{m}(i_{0}) = i_{1}  (13)
s ⟶^{a}_{0} s′ ⇒ σ_{m}(s) ⟶^{λ(a)}_{1∗} σ_{m}(s′)  (14)
□

The intuition is that initial states are preserved and transitions in T_{0} are simulated in T_{1}, except when λ_{m}(a) = ∗, in which case they represent inaction in T_{1}. Composition of morphisms is defined component-wise. This defines the category TS. We suppress the subscript m when no confusion is possible.

Let Set_{∗} denote the category whose objects are labelling sets L and whose morphisms are partial functions λ : L ↪ L′ between labelling sets.

4 This category is different from the one presented in Sec. 2; we use this category because it has universal constructions such as, e.g., products and co-products which correspond in an almost direct way to the well-known process algebraic constructions.

4.2 More Categorical Preliminaries, Fibred Category Theory

Let p : TS ⟶ Set_{∗} be the function which sends an lts to its labelling set and a morphism (σ, λ) : T_{0} ⟶ T_{1} to λ : L_{0} ⟶ L_{1}. A fibre over L, p^{−1}(L), is the subcategory of TS whose objects have labelling set L and whose morphisms f map to 1_{L}, the identity function on L, under p.

We will use the following notions from fibred category theory.

Definition 13. A morphism f : T ⟶ T′ in TS is said to be Cartesian with respect to p : TS ⟶ Set_{∗} if for any morphism g : T′′ ⟶ T′ in TS such that p(g) = p(f) there is a unique morphism h : T′′ ⟶ T such that p(h) = 1_{p(T)} and f ∘ h = g.

[figure: T′′; g; h; TS; p; T; f; T′; _{Set_{∗}}; p(T); p(f); p(T′)]

A Cartesian morphism f : T ⟶ T′ in TS is said to be a Cartesian lifting of

the morphism p(f) in Set_{∗} with respect to T′. □

It can be shown now that p is a fibration, i.e.,

– any morphism λ : L ⟶ L′ in Set_{∗} has a Cartesian lifting with respect to any T′ in TS such that p(T′) = L′.

– any composition of Cartesian morphisms is itself Cartesian.

Dually, we define a morphism to be co-Cartesian.

Definition 14. A morphism f : T ⟶ T′ in TS is said to be co-Cartesian with respect to p : TS ⟶ Set_{∗} if for any morphism g : T ⟶ T′′ in TS such that p(g) = p(f) there is a unique morphism h : T′ ⟶ T′′ such that p(h) = 1_{p(T′)} and h ∘ f = g.

[figure: T′′; TS; p; T; g; f; T′; h; _{Set_{∗}}; p(T); p(f); p(T′)]

A co-Cartesian morphism f : T ⟶ T′ in TS is said to be a co-Cartesian lifting

of the morphism p(f) in Set_{∗} with respect to T′. □

Similarly, it can be shown that p is a co-fibration, i.e., p^{op} : TS^{op} ⟶ Set_{∗}^{op} is a fibration.

In the following, let U be TS, let F be the union of all fibres over all labelling sets, and let M be the subcategory of F induced by all non-restarting ltss, i.e., there are no transitions into the initial state. The reason for staying within fibres is that one commonly insists on having labelled actions simulated by identically labelled actions. Notice that TS_{Act} from Sect. 2 can be viewed as the fibre p^{−1}(Act). Morphisms in M will always be of the form (σ, 1_{L}), for some labelling set L. In particular, all commuting diagrams of the form (1) in M will always belong to some fibre p^{−1}(L). It can also be shown that M has pullbacks, hence ∼_{P} is an equivalence relation [JNW93]. The reason we consider non-restarting ltss is technical. We will address this issue below.

We shall assume that the category P of observation is closed under renaming of states and closed under variation of labelling sets, i.e., if (S, i, L, ⟶) is an observation and L′ is any labelling set such that (S, i, L′, ⟶) is an lts, then it is also an observation.

To emphasise the use of the theory in Sect. 3, we will use the notation M and P.

4.3 Product

In this section, we consider the product construction, which has strong relations to, e.g., CCS’s parallel composition operator, see [WN95] and Sect. 4.8. In [WN95], it is shown how CCS’s parallel composition operator can be expressed using the product, renaming, and relabelling operators we present below.

Definition 15. Let T_{0} × T_{1} denote (S, i, L, ⟶), where

– S = S_{0} × S_{1}, with i = (i_{0}, i_{1}) and projections ρ_{0} : S ⟶ S_{0}, ρ_{1} : S ⟶ S_{1} ,

– L = L_{0} ×_{∗} L_{1} = (L_{0} × {∗}) ∪ ({∗} × L_{1}) ∪ (L_{0} × L_{1}), with projections π_{0} : L_{0} ×_{∗} L_{1} ↪ L_{0} and π_{1} : L_{0} ×_{∗} L_{1} ↪ L_{1}, and

– s ⟶^{a}_{∗} s′ ⇔ ρ_{0}(s) ⟶^{π_{0}(a)}_{0∗} ρ_{0}(s′) ∧ ρ_{1}(s) ⟶^{π_{1}(a)}_{1∗} ρ_{1}(s′) .

□

Let Π_{0} = (ρ_{0}, π_{0}) : T_{0} × T_{1} ⟶ T_{0} and Π_{1} = (ρ_{1}, π_{1}) : T_{0} × T_{1} ⟶ T_{1}. It can be shown that this construction is a product of T_{0} and T_{1} in the category TS.

The product construction allows the two components T_{0} and T_{1} to proceed independently of each as well as synchronising on any of their actions. This behaviour is far too generous compared to CCS’s parallel composition. However, by restricting away all action pairs from T_{0} × T_{1} that are not of the form (a, ∗), (∗, a), or (a, ā), corresponding to a move in the left component, right component, and a synchronisation on complementary actions, and relabelling (a, ∗), (∗, a), and (a, ā) to a,a, and τ, respectively, we obtain CCS’s parallel composition. Both restriction and relabelling can be handled in our setting.

For a fixed lts T_{0} the above construction induces an obvious functor T_{0} × : M ⟶ M. We continue by applying our theory to prove a general result for this functor. First we need a definition, which will help formalising the “factoring” of observations in a product object.

Definition 16. Let T = (S, i, L, ⟶) and let λ : L ↪ L′ represent a partial function between labelling sets. Let ≡ be the least equivalence relation on S such that if s ⟶^{a} s′ and λ(a) = ∗, then s ≡ s′. Let [s] denote the equivalence class of s under ≡. Define [T]_{λ} = (S′, i′, L′, ⟶ ′), where

– S′ = {[s] | s ∈ S} and i′ = [i],

– [s] ⟶^{b} ′[s′] ⇔ ∃v ∈ [s], v′ ∈ [s′], a ∈ L. v ⟶^{a} v′ ∧ λ(a) = b ≠ ∗ .

Let η_{(T,λ)} : T ⟶ [T]_{λ} be the pair (σ, λ), where σ(s) = [s]. □

A simple argument shows that σ is well-defined. If s ≡ s′, then there exists a “back and forth” path

[figure: ·; l_{1}; l_{2}; ·; l_{3}; ·; l_{n−2}; ·; l_{n−1}; l_{n}; ⋯; s; ·; ·; s′]

where l_{i} = ∗ or λ(l_{i}) = ∗, for 1 ≤ i ≤ n. We conclude that σ(s) = σ(s′).

Proposition 17. The morphism η_{(T,λ)} : T ⟶ [T]_{λ} is co-Cartesian with respect to p.

Proof. Assume f : T ⟶ T_{1} and p(f) = p(η_{(T,λ)}). Define (σ′, 1_{L′}) : [T]_{λ} ⟶ T_{1} by σ′([s]) = σ_{f}(s). By an argument similar to the above one can show that σ′ is well-defined. To see that (σ′, 1_{L′}) is a morphism first notice that σ′([i]) = σ_{f}(i) =

i_{1}. Next, assume [s] ⟶^{b} ′[s′], i.e., ∃v ∈ [s], v′ ∈ [s′], a ∈ L. v ⟶^{a} v′ ∧ λ(a) =

b ≠ ∗. Then σ_{f}(v) ⟶^{λ(a)}_{1∗} σ_{f}(v′), i.e., σ′([s]) ⟶^{b}_{1∗} σ′([s′]). It is easy to see that (σ′, 1_{L′}) is the uniquely determined morphism such that p((σ′, 1_{L′})) = 1_{p([T]_{λ})} and f = (σ′, 1_{L′}) ∘ η_{(T,λ)}.

Lemma 18. For a partial function λ : L ↪ L′ between labelling sets, there is a functor F_{λ} : p^{−1}(L) ⟶ p^{−1}(L′) which sends f = (σ, 1_{L}) : T_{0} ⟶ T_{1} to F_{λ}(f) = (γ, 1_{L′}) : [T_{0}]_{λ} ⟶ [T_{1}]_{λ} defined by γ([s]) = [σ(s)].

Proof. The proof is routine, hence omitted.

We can now show the following theorem.

Theorem 19. Let T_{0} belong to M and L_{0} = p(T_{0}). Let P be any subcategory of U such that whenever we have O ⟶^{f} O′ in P, where p(f) = 1_{L_{0}×_{∗}L} for some

L, then F_{π_{1}}(O) ⟶^{F_{π_{1}} (f)} F_{π_{1}}(O′) also belongs to P. Then T_{0} × : M ⟶ M is a P-operator.

Proof. By Theorem 10 it is sufficient to show that T_{0} × is P-factorisable. So assume T ⟶^{m} T′ belongs to M, p(T) = L, and we are given Ô \underrightarrow{_{q}} T̂_{0}×(T̂), i.e., a commuting diagram in M

[figure: O; f; q; T_{0} × T; T_{0}×m; O′; q′; T_{0} × T′]

Since M is the union of fibres we have p(f) = p(q) = p(q′) = p(T_{0} × m) = 1_{L_{0}×_{∗}L} for some set L. Let π_{1} : L_{0} ×_{∗} L ↪ L be the projection on the second component. By our assumptions F_{π_{1}}(O) ⟶^{F_{π_{1}} (f)} F_{π_{1}}(O′) is in P. Let O_{1} = F_{π_{1}}(O), O′_{1} = F_{π_{1}}(O′), q = (σ_{q}, 1_{L_{0}×_{∗}L}), and q′ = (σ_{q′}, 1_{L_{0}×_{∗}L}). Define

q^{#} = (σ, 1_{L}) : O_{1} ⟶ T , where σ([s]) = ρ_{1}(σ_{q}(s)), and

q^{′#} = (σ′, 1_{L}) : O′_{1} ⟶ T′ , where σ′([s′]) = ρ′_{1}(σ_{q′}(s′)) ρ_{1} and ρ′_{1} are the projections mentioned in Definition 15. Notice, e.g., that for any s_{1}, s_{2} ∈ [s] in O_{1} we have ρ_{1}(σ_{q}(s_{1})) = ρ_{1}(σ_{q}(s_{2})). Next, define

q^{⋆} = (γ, 1_{L_{0}×_{∗}L}) : O ⟶ T_{0} × O_{1} , where γ(s) = (ρ_{0}(σ_{q}(s)), [s]), and q^{′⋆} = (γ′, 1_{L_{0}×_{∗}L}) : O′ ⟶ T_{0} × O′_{1} , where γ′(s′) = (ρ′_{0}(σ_{q′}(s′)), [s′])

It can now be shown that both diagrams

[figure: O; f; q^{⋆}; T_{0} × O_{1}; 1_{T_{0}} ×F_{π_{1}} (f); O_{1}; F_{π_{1}} (f); q^{#}; T; m; O′; q^{′⋆}; T_{0} × O′_{1}; O′_{1}; q^{′#}; T′]

exist in M and commute, i.e., we have morphisms Ô \underrightarrow{_{q^{⋆}}} T̂_{0}×(Ô_{1}) and Ô_{1} \underrightarrow{_{q^{#}}} T̂ in M̂. It can also be shown that q = q^{#} ∘ q^{⋆} and q′ = q^{′#} ∘ q^{′⋆}. Hence we have a commuting diagram of the form (12). Hence T_{0} × is P-factorisable.

4.4 Co-Product In this section, we consider the co-product construction, which has strong relations to, e.g., CCS’s nondeterministic choice operator, see [WN95] and Sect. 4.8. Definition 20. Let T_{0} + T_{1} denote (S, i, L, ⟶), where – S = (S_{0} × {i_{1}}) ∪ ({i_{0}} × S_{1}), with i = (i_{0}, i_{1}) and injections in_{0} : S_{0} ⟶ S,

in_{1} : S_{1} ⟶ S ,

– L = L_{0} ∪_{∗} L_{1} = (L_{0} × {∗}) ∪ ({∗} × L_{1}), with injections j_{0} : L_{0} ⟶ L and j_{1} : L_{1} ⟶ L, and

– s ⟶^{a} s′ ⇔ ∃v ⟶^{b}_{0} v′. (in_{0}(v), j_{0}(b), in_{0}(v′)) = (s, a, s′) or

∃v ⟶^{b}_{1} v′. (in_{1}(v), j_{1}(b), in_{1}(v′)) = (s, a, s′)

□

Let I_{0} = (in_{0}, j_{0}) : T_{0} ⟶ T_{0} + T_{1} and I_{1} = (in_{1}, j_{1}) : T_{1} ⟶ T_{0} + T_{1}. It can be shown that this construction is a coproduct of T_{0} and T_{1} in the category TS.

As opposed to the product construction, the co-product construction resembles more a process algebraic choice, “+”, operator. If we consider non-restarting ltss, co-product can be shown to correspond to “+” in a formal sense [WN95].

Definition 21. Given T′ = (S′, i′, L′, ⟶ ′) and a partial function λ : L ↪ L′. Let T′_{↓λ} = (S, i, L, ⟶), where

– S = {s ∈ S′ | ∃a_{1}, …, a_{n} ∈ L, s_{1}, …, s_{n} ∈ S′.

i′ ⟶^{λ(a_{1})} ′s_{1} ⟶^{λ(a_{2})} ′ ⋯ ⟶^{λ(a_{n})} ′s_{n} ∧ s_{n} = s}

– i = i′

– s ⟶^{b} s′ ⇔ s ⟶^{λ(b)} ′_{∗}s′

□

Let η_{(T′,λ)} : T′_{↓λ} ⟶ T′ be the pair (in, λ), where in is the injection function.

Proposition 22. The morphism η_{(T′,λ)} : T′_{↓λ} ⟶ T′ is Cartesian with respect to p.

Lemma 23. For a partial function λ : L ↪ L′ between labelling sets, there is a functor F_{↓λ} : p^{−1}(L′) ⟶ p^{−1}(L) which sends f = (σ, 1_{L′}) : T_{0} ⟶ T_{1} to F_{↓λ} = (γ, 1_{L}) : T_{0↓λ} ⟶ T_{1↓λ} defined by γ(s) = σ(s).

Theorem 24. Let T_{0} belong to M and L_{0} = p(T_{0}). Assume P is a subcategory of M such that whenever we have O ⟶^{f} O′ in P with p(f) = 1_{L_{0}∪_{∗}L} for some

L, F_{↓λ}(O) ⟶^{F_{↓λ}(f)} F_{↓λ}(O′) also belongs to P, where λ : L ⟶ L_{0} ∪_{∗} L is the injection function. Then T_{0} + : M ⟶ M is a P-operator.

Proof. It is sufficient to show that T_{0} + is P-factorisable. So assume T ⟶^{m} T′

belongs to M, p(T) = L, and we are given Ô \underrightarrow{_{q}} T̂_{0}+(T̂), i.e., a commuting diagram in M

[figure: O; f; q; T_{0} + T; 1_{T_{0}} +m; O′; q′; T_{0} + T′]

Let p(f) = 1_{L_{0}∪_{∗}L}. Let λ : L ⟶ L_{0} ∪_{∗} L be the injection function sending

a ∈ L to (∗, a) ∈ L_{0} ∪_{∗} L. By our assumptions F_{↓λ}(O) ⟶^{F_{↓λ}(f)} F_{↓λ}(O′) is in P. Let O_{1} = F_{↓λ}(O), O′_{1} = F_{↓λ}(O′), q = (σ_{q}, 1_{L_{0}∪_{∗}L}), and q′ = (σ_{q′}, 1_{L_{0}∪_{∗}L}). Define

q^{#} = (σ, 1_{L}) : O_{1} ⟶ T , where σ(s) = t, where σ_{q}(s) = (r, t), and

q^{′#} = (σ′, 1_{L}) : O′_{1} ⟶ T′ , where σ′(s′) = t′, where σ_{q′}(s′) = (r′, t′)

Next, define

q^{⋆} = (γ, 1_{L_{0}∪_{∗}L}) : O ⟶ T_{0} + O_{1} , where γ(s) = (r, i_{1}) if σ_{q}(s) = (r, i), γ(s) = (i_{0}, t) if σ_{q}(s) = (i_{0}, t), and

q^{′⋆} = (γ′, 1_{L_{0}∪_{∗}L}) : O′ ⟶ T_{0}+O′_{1} , where γ′(s′) = (r′, i′_{1}) if σ_{q′}(s′) = (r′, i′), γ′(s′) = (i′_{0}, s′) if σ_{q′}(t′) = (i′_{0}, t′)

It can now be shown that both diagrams

[figure: O; f; q^{⋆}; T_{0} + O_{1}; 1_{T_{0}} +F_{↓λ}(f); O_{1}; F_{↓λ}(f); q^{#}; T; m; O′; q^{′⋆}; T_{0} + O′_{1}; O′_{1}; q^{′#}; T′]

exist in M and commute, i.e., we have morphisms Ô \underrightarrow{_{q^{⋆}}} T̂_{0}+(Ô_{1}) and Ô_{1} \underrightarrow{_{q^{#}}} T̂

in M̂. It can also be shown that q = q^{#} ∘ q^{⋆} and q′ = q^{′#} ∘ q^{′⋆}. Hence we have a commuting diagram of the form (12). Hence T_{0} + is P-factorisable.

4.5 Restriction

In this section, we consider relabelling.

Definition 25. Given T′ = (S′, i′, L′, ⟶′) and a labelling set L. Let F ↓: M ⟶ M denote the functor which sends T′ to T = (S, i, L, ⟶), where

– S = {s ∈ S′ | ∃a_{1}, …, a_{n} ∈ L ∩ L′, s_{1}, …, s_{n} ∈ S′.

i′ ⟶^{a_{1}} ′s_{1} ⟶^{a_{2}} ′ ⋯ ⟶^{a_{n}} ′s_{n} ∧ s_{n} = s}

– i = i′

– s ⟶^{a} s′ ⇔ s ⟶^{a} ′s′, a ∈ L

and which maps a morphism m = (σ′_{m}, 1_{L′}) : T′_{1} ⟶ T′_{2} to F ↓ (m) = (σ_{m}, 1_{L}) : F ↓ (T′_{1}) ⟶ F ↓ (T′_{2}), where σ_{m}(s) = σ′_{m}(s). □

We have the following perhaps surprising result.

Theorem 26. For any choice of P the functor F ↓L is a P-operator.

Proof. We show that F ↓L is a P-operator. Assume T ⟶^{m} T′ and we have

[figure: O; f; q; F ↓L(T); F↓L(m); O′; q′; F ↓L(T′)]

that commutes in M. Let p(T) = L′. By our assumptions we must have a

commuting diagram

[figure: O_{1}; m_{1}; q^{#}; T; m; O′_{1}; q^{′#}; T′]

where O = (S, i, L, ⟶), O′ = (S′, i′, L, ⟶), f = (σ_{f}, 1_{L}), O_{1} = (S, i, L′, ⟶),

O′_{1} = (S′, i′, L′, ⟶ ′), m_{1} = (σ_{f}, 1_{L′}), q = (σ_{q}, 1_{L}), q′ = (σ_{q′}, 1_{L}), q^{#} = (σ_{q}, 1_{L′}), and q^{′#} = (σ_{q′}, 1_{L′}). Notice F ↓ L(O_{1}) = O, F ↓ L(O′_{1}) = O′, and F ↓L(m_{1}) = f. It can easily be shown that we have a diagram in M̂ as required in (12) and that it commutes.

4.6 Relabelling

Relabelling, as presented in [WN95], is a bit tricky. We will need some auxiliary definitions and we will have to consider (relabelling) functors between fibres.

Definition 27. Let T = (S, i, L, ⟶) be an lts and λ : L ⟶ L′ be a total function between labelling sets. Define T {λ} to be the lts (S, i, L′, ⟶ ′), where

s ⟶^{a} ′s′ ⇔ ∃ b. s ⟶^{b} s′ ∧ λ(b) = a .

□

Proposition 28. If λ : L ⟶ L′ is a total function in Set_{∗}, then T ⟶^{f} T {λ}, where f = (1_{S}, λ) is co-Cartesian with respect to p.

Proof. The proof is routine, hence omitted.

Any total function λ : L ⟶ L′ induces a functor F {λ} : p^{−1}(L) ⟶ p^{−1}(L′). Notice that F {λ} is not an endofunctor on M. Instead, given λ : L ⟶ L′ we consider λ′ : L ∪ L′ ⟶ L ∪ L′ defined by λ′(a) = λ(a) if a ∈ L and λ′(a) = a otherwise. Now p^{−1}(L) and p^{−1}(L′) embed fully and faithfully in p^{−1}(L∪L′). We will therefore only consider total relabelling functions of the form λ : L ⟶ L.

Let p_{0} : TS ⟶ Set be the functor which sends T to S and (σ, λ) : T ⟶ T′ to σ.

Definition 29. Let F^{−1}{λ}(T) denote the subcategory of p^{−1}(L) whose objects are ltss T′ such that F {λ}(T′) = T and whose morphisms f map to 1_{p_{0}(T)} under p_{0}; objects in F^{−1}{λ}(T) have the same set of states as T.

An object T′ in F^{−1}{λ}(T) is minimal if the only morphisms in F^{−1}{λ}(T) with codomain T′ is the identity morphism on T′. □

Remark. Notice that if T′ is minimal in F^{−1}{λ}(T), then for any two transitions s ⟶^{a} s′ and s ⟶^{b} s′ in T′ we have a ≠ b implies λ(a) ≠ λ(b).

Theorem 30. Given a total relabelling function λ : L ⟶ L. Choose M = p^{−1}(L). Let P be a subcategory of U. Assume that for all O ⟶^{f} O′ in P, where f = (σ_{f}, 1_{L}) and F^{−1}{λ}(O) and F^{−1}{λ}(O′) are nonempty, (σ_{f}, 1_{L}) : O_{1} ⟶ O′_{1} belongs to P, whenever O_{1} and O′_{1} are minimal elements in F^{−1}{λ}(O) and F^{−1}{λ}(O′), respectively, and (σ_{f}, 1_{L}) : O_{1} ⟶ O′_{1} defines a morphism. Then F {λ} : M ⟶ M is a P-operator.

Proof. Choose M = p^{−1}(L). We show that F {λ} : M ⟶ M is a P-operator, where λ : L ⟶ L is a total relabelling function. Assume T ⟶^{m} T′ belongs to M and we have

[figure: O; f; q; F {λ}(T); F {λ}(m); O′; q′; F {λ}(T′)]

that commutes in M. Since O is simulated in F {λ}(T) we know that F^{−1}{λ}(O)

is nonempty. Similarly, F^{−1}{λ}(O′) is nonempty. Since O is simulated in F {λ}(T) and p(m) = 1_{L}, there must exist a minimal O_{1} in F^{−1}{λ}(O) and a minimal O′_{1} in F^{−1}{λ}(O′) such that g = (σ_{f}, 1_{L}) : O_{1} ⟶ O′_{1} is a well-defined morphism in P and such that

q^{#} = (σ_{q}, 1_{L}) : O_{1} ⟶ T , where q = (σ_{q}, 1_{L}) : O ⟶ F {λ}(T), and

q^{′#} = (σ_{q′}, 1_{L}) : O′_{1} ⟶ T′ , where q′ = (σ_{q′}, 1_{L}) : O′ ⟶ F {λ}(T′) are well-defined morphisms in M.

Next, define

q^{⋆} = (γ, 1_{L}) : O ⟶ F {λ}(O_{1}) , where γ(s) = s, and

q^{′⋆} = (γ′, 1_{L}) : O′ ⟶ F {λ}(O′_{1}) , where γ′(s′) = s′

It can now be shown that both diagrams

[figure: O; f; q^{⋆}; F {λ}(O_{1}); F {λ}(g); O_{1}; g; q^{#}; T; m; O′; q^{′⋆}; F {λ}(O′_{1}); O′_{1}; q^{′#}; T′]

exist in M and commute, i.e., we have morphisms Ô \underrightarrow{_{q^{⋆}}} F̂ \{λ\}(Ô_{1}) and Ô_{1} \underrightarrow{_{q^{#}}}

T̂ in M̂. It can also be shown that q = q^{#} ∘ q^{⋆} and q′ = q^{′#} ∘ q^{′⋆}. Hence we have a commuting diagram of the form (12). Hence F {λ} is P-factorisable.

Notice that M = p^{−1}(L) is no restriction in our case, since M “consists” of full subcategories of fibres: it is easy to see that a P-open morphism in p^{−1}(L) is also P-open in M.

4.7 Prefix

Definition 31. Given T = (S, i, L, ⟶) and a label α. Let α.T = (S′, i′, L ∪ {α}, ⟶ ′), where

– S′ = {{s} | s ∈ S} ∪ {∅}, i′ = ∅, and

– v ⟶^{b} ′v′ ⇔ (v = ∅ ∧ b = α ∧ v′ = {i}) or (v = {s} ∧ v′ = {s′} ∧ s ⟶^{b} s′) .

□

Any label α induces a functor α. : M ⟶ M which sends f = (σ, 1_{L}) : T ⟶ T′ to (σ′, 1_{L∪{α}}) : α.T ⟶ α.T′, where σ′(∅) = ∅ and σ′({s}) = {σ(s)}.

Definition 32. Given T and a label α. Let α^{−1}(T) = (S′, i′, L, →′), where

– S′′ = {s ∈ S | ∃v ∈ L^{∗}. i ⟶^{α}⟶^{v} s}\{s | i ⟶^{α} s} ,

– S′ = {{s} | s ∈ S′′} ∪ {{s | i ⟶^{α} s}} ,

– i = {s | i ⟶^{α} s} , and

– r ⟶^{a} ′r′ ⇔ ∃s ∈ r, s′ ∈ r′. s ⟶^{a} s′ .

□

Any label α induces a functor α^{−1} : U ⟶ U which sends f = (σ, 1_{L}) : T ⟶ T′ to α^{−1}(f) = (σ′, 1_{L}) : T_{1} ⟶ T_{2}, where T_{1} = α^{−1}(T), T_{2} = α^{−1}(T′), σ′(i_{1}) = i_{2}, and σ′({s}) is the unique v ∈ S_{2} such that σ(s) ∈ v. Notice that α^{−1}(T) may not be non-restarting even though T is.

Theorem 33. Let P be a subcategory of U. Assume that whenever we have

O ⟶^{f} O′ in P, then α^{−1}(O) ⟶^{α^{−1}(f)} α^{−1}(O′) also belongs to P. Then α. is a P-operator.

Proof. We show that α. is a P-operator. Assume T ⟶^{m} T′ and we have

[figure: O; f; q; α.T; α.m; O′; q′; α.T′]

that commutes in M. Notice that since T and T′ are assumed to be non-

restarting, α^{−1}(O) and α^{−1}(O′) must also be non-restarting. Assume α ∈ L =

p(T). By our assumptions α^{−1}(O) ⟶^{α^{−1}(f)} α^{−1}(O′) is in P. Let O_{1} = α^{−1}(O) and O′_{1} = α^{−1}(O′). Define

q^{#} = (σ, 1_{L}) : O_{1} ⟶ T , given by σ(i_{1}) = i and σ({s}) = r, where σ_{q}(s) = {r} and q = (σ_{q}, 1_{L}) : O ⟶ α.T, and

q^{′#} = (σ′, 1_{L}) : O′_{1} ⟶ T′ , given by σ′(i′_{1}) = i′ and σ′({s′}) = r′, where σ_{q′}(s′) = {r′} and q′ = (σ_{q′}, 1_{L}) : O′ ⟶ α.T′

Next, define

q^{⋆} = (γ, 1_{L}) : O ⟶ α.O_{1} , where γ(i) = ∅,

γ(s) = {i_{1}} for s ∈ {s |, i ⟶^{α} s} in O, γ(s) = {{s}}, else, and

q^{′⋆} = (γ′, 1_{L}) : O′ ⟶ α.O′_{1} , where γ′(i′) = ∅,

γ′(s′) = {i′_{1}} for s′ ∈ {s′ |, i′ ⟶^{α} s′} in O′, γ′(s′) = {{s′}}, else.

It can now be shown that both diagrams

[figure: O; f; q^{⋆}; α.O_{1}; α.g; O_{1}; g; q^{#}; T; m; O′; q^{′⋆}; α.O′_{1}; O′_{1}; q^{′#}; T′]

exist in M and commute, i.e., we have morphisms Ô \underrightarrow{_{q^{⋆}}} α̂.(Ô_{1}) and Ô_{1} \underrightarrow{_{q^{#}}} T̂

in M̂. It can also be shown that q = q^{#} ∘ q^{⋆} and q′ = q^{′#} ∘ q^{′⋆}. Hence we have a commuting diagram of the form (12).

For the case where α ∉ p(T) the same reasoning can be used. First extend T and T′’s labelling sets to include α. The induced m_{α} : T ⟶ T′ in p^{−1}(L ∪ {α}) will be P-open if and only if m : T ⟶ T′ is due to our assumptions about P. Now notice that m_{α} and m are identical under α. . We conclude that α. is P-factorisable.

4.8 Putting it together

Let us consider Milner’s CCS-operators except recursion, which is handled in next section. Under the common assumption that only guarded sum is considered, it is shown in [WN95] how these CCS-operators can be expressed by the above constructions (functors). For each operator we have obtained a theorem for the corresponding functor which identifies conditions which guarantee that the functor is a P-operator. Or put differently, for each functor we have metatheorems providing conditions on P guaranteeing that ∼_{P} remains a congruence with respect to the functor (operator).

However, we would like to consider more than one functor at the time. Does there exist choices of P, such that P satisfies the conditions of all our theorems (including relabelling and prefixing) ?

Choosing P in M as the full subcategory induced by words (i.e., fibre-wise as done for P_{M} in Sec. 4.2), we can show that ∼_{P} also corresponds to Milner’s strong bisimulation. Moreover, it is easy to see that P satisfies all conditions of our theorems, i.e., ∼_{P} must be a congruence with respect to all the operators (functors). For example, let us just consider the conditions from Theorem 19. They state that when viewing the objects of P as finite strings, P in general has to be closed under the operation of taking a subsequence, and possibly renaming the labels. Furthermore, as an immediate consequence we conclude that ∼_{P} is a congruence with respect to the aforementioned CCS operators.

What about other choices of P? If—similarly to the choice of P_{H} in P_{M} in Sect. 2—we choose P as the subcategory of the previous choice of P obtained by only keeping identity morphisms and morphisms whose domains are observations having only one state (the empty word), then ∼_{P} corresponds to Hoare trace equivalence. This choice of P also trivially satisfies all conditions required by the theorems. Hence, Hoare trace equivalence is a congruence with respect to the presented constructions (and, again, the aforementioned CCS operators).

Choosing P as, e.g., the subcategory induced by trees will also satisfy all conditions required by the theorems. Hence ∼_{P}, which is a strictly finer equivalence than Milner’s strong bisimulation as hinted in [CN95], must also be a congruence with respect to the presented constructions.

5 Recursion

For recursion there is no simple way of defining a functor on M representing Milner’s recursion operator. The reason is that one needs some notion of process variables which are to be bound by the recursion operator. Some kind of process term language is necessary, as can be seen both in Milner’s work [Mil89] and Winskel and Nielsen’s [WN95]. However, without introducing a process algebraic term language it is possible to capture a recursion-like operator in a “faithful” way. The restriction is intuitively that free process variable cannot occur under the scope of a parallel composition operator. Such restrictions have been considered by Taubner [Tau89].

First, identify a set of variables Var and extend the objects (S, i, L, ⟶) of M with a partial function l from S to Var. Also, we now allow restarting ltss. ^{5} Furthermore, whenever l is defined on a state s, there can be no outgoing transitions from s and morphisms are now required to respect the labelling function l.

5 The only implication of this assumption is, that co-product will have to be handled in a way similar to recursion. We could also have considered a recursion operator which “unfolded” the transition systems, and hence stayed within the non-restarting ltss.

We define F_{X} : M ⟶ M, which intuitively “binds X”, on objects as follows. Given T = (S, i, L, ⟶, l), then F_{X}(T) = (S′, i′, ⟶ ′, L, l′), where

S′ = {i}, i′ = i, ⟶ ′ = ∅, and l′ is totally undefined, when l(i) = X, (15)

S′ = {s ∈ S | l(s) ≠ X}, i′ = i, l′ equals l on S′, when l(i) ≠ X, where (16)

s ⟶^{a} ′s′ if s ⟶^{a} s′ ∧ l(s′) ≠ X  (17)

or

∃ s′′. s ⟶^{a} s′′ ∧ l(s′′) = X ∧ s′ = i

Given a morphism f : T_{1} ⟶ T_{2}. F_{X}(f) : F_{X}(T_{1}) ⟶ F_{X}(T_{2}) is defined to map s ∈ S′_{1} to f(s) if l_{2}(f(s)) ≠ X, and i′_{2} otherwise.

Intuitively, F_{X} simply redirects all transitions going into X-labelled states to the initial state. For example:

[figure: i; α; ⟶^{σ}; i′; α; α; ⟼; i; α; ⟶^{F_{X}(σ)}; i′; α; X; X; F_{X} binding X]

F_{X} has the following desirable property:

Lemma 34. For any X ∈ Var, F_{X} is a functor.

Proof. The proof is routine, hence omitted.

As a special case, let us consider P as the subcategory of M corresponding to (10) except that final states may now be labelled with variables from Var.

Theorem 35. For any X ∈ Var, F_{X} is a P-operator.

Proof. The first observation is that (12) is not going to hold. This is due to the fact that an observation of F_{X}(T) can correspond to many observations of T. However, we can apply the theory from Definition 12 on each of these observations individually. So assume T ⟶^{m} T′ belongs to M and that

[figure: O; f; q; F_{X}(T); F_{X}(m); O′; q′; F_{X}(T′)]

is a commuting diagram in M. Let us denote f = (σ_{f}, 1_{L}) and use a similar

notation for q, q′, and m. Let O be denoted as

s_{0} ⟶^{a_{1}} s_{1} ⟶^{a_{2}} ⋯ ⟶^{a_{n}} s_{n}

and O′ as

s′_{0} ⟶^{a_{1}} s′_{1} ⟶^{a_{2}} ⋯ ⟶^{a_{n}} s′_{n} ⟶^{a_{n+1}} ⋯ ⟶^{a_{n+m}} s′_{n+m} .

Let 1 ≤ j_{1} < ⋯ < j_{r} ≤ n be all indexes such that the is no a_{j_{k}} transition from σ_{q}(s_{j_{k}−1}) to σ_{q}(s_{j_{k}}) in T, where r ≥ 0. This means that for 1 ≤ k ≤ r there exists a transition σ_{q}(s_{j_{k}−1}) ⟶^{a_{j_{k}}} r_{k} in T such that r_{k} is labelled X.

Let j_{0} = 0 and let U_{1}, …, U_{r} be observations in P, where for 1 ≤ k ≤ r, U_{k} is given by

(j_{k−1}, σ_{q}(s_{j_{k−1}})) ⟶^{a_{j_{k−1}}} ⋯ ⟶^{a_{j_{k}−1}} (j_{k} − 1, σ_{q}(s_{j_{k}−1})) ⟶^{a_{j_{k}}} (j_{k}, r_{k})

with final state labelled by X (labelling set L, and initial state (j_{k−1}, σ_{q}(s_{j_{k−1}}))). We refer to this procedure as splitting.

For 1 ≤ k ≤ r, let U′_{k} be the observation

(j_{k−1}, σ_{f}(σ_{q}(s_{j_{k−1}}))) ⟶^{a_{j_{k−1}}} ⋯ ⟶^{a_{j_{k}−1}} (j_{k} − 1, σ_{f}(σ_{q}(s_{j_{k}−1})) ⟶^{a_{j_{k}}} (j_{k}, σ_{f}(r_{k}))

with labelling set L. Again, the final state is labelled by X. Notice that if r > 0, then σ_{q′}(s′_{j_{r}}) = i′ in T′.

If there exists no n < k ≤ n + m such that there is no a_{k} transition from σ′_{q}(s′_{k−1}) to σ′_{q}(s′_{k}) in T′, then choose r′ = 0 and U_{r+r′+1} as

(j_{r}, σ_{q}(s_{j_{r}})) ⟶^{a_{jr +1}} ⋯ ⟶^{a_{n}} (n, σ_{q}(s_{n}))

where all states are unlabelled, and U′_{r+r′+1} as

(j_{r}, σ_{q′}(s′_{j_{r}})) ⟶^{a_{jr +1}} ⋯ ⟶^{a_{n+m}} (n + m, σ_{q′}(s′_{n+m}))

Else, split

s′_{j_{r}} ⟶^{a_{jr +1}} ⋯ ⟶^{a_{n+m}} s′_{n+m}

obtaining indexes n ≤ j_{r+1} < ⋯ < j_{r+r′} ≤ n+m, where r′ > 0, and observations U′_{j_{r+1}}, …, U′_{j_{r+r′}} with final states labelled with X. Let j_{r+r′+1} = n+m. Let U_{r+1} be the observation

(j_{r}, σ_{q}(s_{j_{r}})) ⟶^{a_{jr +1}} ⋯ ⟶^{a_{n}} (n, σ_{q}(s_{n}))

with all states unlabelled. For r + 1 < k ≤ r + r′ + 1 let U_{k} be the observation consisting of a single unlabelled state (j_{k}, i). Let U′_{r+r′+1} be the observation

(j_{r+r′}, σ_{q′}(s′_{j_{r+r′}})) ⟶^{a_{j_{r+r′} +1}} ⋯ ⟶^{a_{n+m}} (n + m, σ_{q′}(s′_{n+m}))

with all states unlabelled.

For 1 ≤ k ≤ r + r′ + 1 let V_{k} and V′_{k} denote the unlabelled versions of U_{k} and U′_{k}, respectively.

Note that for 1 ≤ k ≤ r + r′ + 1 there exist – a uniquely determined morphism f_{k} : V_{k} ⟶ V′_{k},

– an obvious morphism q_{k} : V_{k} ⟶ F_{X}(T), sending a state (p, s) to s,

– an obvious morphism q′_{k} : V′_{k} ⟶ F_{X}(T′),

– a uniquely determined morphism m_{k} : U_{k} ⟶ U′_{k},

– an obvious morphism q_{(k,#)} : U_{k} ⟶ T, sending a state (p, s) to s,

– an obvious morphism q′_{(k,#)} : U′_{k} ⟶ T′,

– an obvious morphism q_{(k,⋆)} : V_{k} ⟶ F_{X}(U_{k}), sending a state (p, s) to s, and – an obvious morphism q′_{(k,⋆)} : V′_{k} ⟶ F_{X}(U′_{k}) .

Now for 1 ≤ k ≤ r + r′ + 1

[figure: V_{k}; f_{k}; q_{k}; F_{X}(T); F_{X}(m); V′_{k}; q′_{k}; F_{X}(T′)]

commutes. Also, it can be shown that the two diagrams

[figure: V_{k}; f_{k}; q_{(k,⋆)}; F_{X}(U_{k}); F_{X}(m_{k}); U_{k}; m_{k}; q_{(k,#)}; T; m; V′_{k}; q′_{(k,⋆)}; F_{X}(U′_{k}); U′_{k}; q′_{(k,#)}; T′]

commute. Denoting these diagrams as morphisms in M̂ we can show that the

diagram

[figure: V̂_{k}; _{q_{k}}; _{q^{⋆}}; F̂_{X}(Û_{k}); _{F_{X}}(_{q_{(k,#)}}); F̂_{X}(T̂)]

commutes. From the proof of Theorem 10 it follows that there exists morphisms h_{k} : V′_{k} ⟶ F_{X}(T), 1 ≤ k ≤ r+r′+1, such that q_{k} = h_{k}∘f_{k} and q′_{k} = F_{X}(m)∘h_{k}. From these morphisms one can then obtain a morphism h = (σ_{h}, 1_{L}) : O′ ⟶ F_{X}(T) such that q = h∘f and q′ = F_{X}(m)∘h. To see this, let σ_{h} be the function that maps s′_{j} to σ_{h_{k}}((j, s′_{j})), when j_{k−1} < j ≤ j_{k}, and to i, when j = 0. It can now be shown that h indeed satisfies the claimed equalities.

6 Conclusion

We have examined Joyal, Nielsen, and Winskel’s notion of behavioural equivalence, P-bisimilarity [JNW93], with respect to congruence properties. Inspired by [WN95], we observed that endofunctors on M can be viewed as abstract operators. Staying within the categorical setting, we then identified simple ^{6} and natural conditions, which ensure that such endofunctors preserve open maps, i.e., that P-bisimilarity is a congruence with respect to the functors. We formalised this as P-factorisability. The main varying parameters were M, P, and the functors.

We then continued by giving a concrete application by fixing M. For a set of endofunctors, we obtained meta-theorems stating conditions on P, which guaranteed that P-bisimilarity would be a congruence with respect the functors.

As for future research, there are many possibilities. Returning to the discussion in the introduction, one could try to merge the two “orthogonal” approaches we mentioned, e.g., try to identify a way of presenting functors by SOS-like rule systems such that one could state conditions about both the rule systems and P, which would guarantee congruence of P-bisimilarity with respect to all functors, whose defining rule systems obeyed a special format.

Another possibility is to continue to work as in Sect. 4—other functors may be considered. However, as shown in [NC95], other choices of M make it possible to capture other interesting behavioural equivalences: weak bisimulation or “true concurrency” equivalences. One could look for similar meta-theorems for such choices of M.

Winskel and Cattani are developing presheaves over categories of observations as models for concurrency [CW96]. For presheaves there are general results on open maps, including the axioms for open maps of Joyal and Moerdijk [JM94], which make light work of showing the bisimulation of presheaves is a congruence for CCS-like languages. Their work exploits universal properties to show preservation of open maps. A condition superficially like P-factorisability is important in transferring such congruence properties from presheaves to other models like transition systems and event structures.

References

[BIM88] Bard Bloom, Sorin Istrail, and Albert R. Meyer. Bisimulation Can’t be Traced. In Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, pages 229–239, 1988.

[CN95] Allan Cheng and Mogens Nielsen. Open maps (at) work. Research Series RS-95-23, BRICS, Department of Computer Science, University of Aarhus, April 1995. 33 pp.

[CW96] G-L. Cattani and G. Winskel. Presheaf models for concurrency. Technical report, BRICS, 1996. To appear.

6 We find it a virtue, that the definition of P-factorisability—just as the definition of open maps—doesn’t require more than a modest knowledge of category theory.

[Hen88] Matthew Hennessy. Algebraic Theory of Processes. MIT Press series in the foundations of computing, 1988.

[JM94] A. Joyal and I. Moerdijk. A completeness theorem for open maps. Annals of Pure and Applied Logic, 70:51–86, 1994.

[JNW93] André Joyal, Mogens Nielsen, and Glynn Winskel. Bisimulation and open maps. In Proc. LICS’93, Eighth Annual Symposium on Logic in Computer Science, pages 418–427, 1993.

[Mil89] Robin Milner. Communication and Concurrency. Prentice Hall International Series In Computer Science, C. A. R. Hoare series editor, 1989.

[NC95] Mogens Nielsen and Allan Cheng. Observe behaviour categorically. In Proc. FST&TCS 15, Fifteenth Conference on the Foundations of Software Technology & Theoretical Computer Science, pages 263–278. Springer-Verlag (LNCS 1026), Bangalore, India, December 1995.

[Plo81] Gordon D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN–19, Computer Science Department, Aarhus University, September 1981.

[Tau89] D. Taubner. Finite Representations of CCS and TCSP Programs by Automata and Petri Nets. Springer-Verlag (LNCS 369), 1989.

[WN95] Glynn Winskel and Mogens Nielsen. Models for Concurrency, volume 4, chapter 1, pages 1–148. Oxford University Press, 1995. eds. S. Abramsky, D. M. Gabbay, and T. S. E. Gabbay.

This article was processed using the L^{A}TEX macro package with LLNCS style

Recent Publications in the BRICS Report Series

RS-96-2 Allan Cheng and Mogens Nielsen. Open Maps, Behavioural Equivalences, and Congruences. January 1996. 25 pp. A short version of this paper is to appear in the proceedings of CAAP ’96.

RS-96-1 Gerth St�lting Brodal and Thore Husfeldt. A Communication Complexity Proof that Symmetric Functions have Logarithmic Depth. January 1996. 3 pp.

RS-95-60 J�rgen H. Andersen, Carsten H. Kristensen, and Arne Skou. Speci�cation and Automated Veri�cation of Real-Time Behaviour � A Case Study. December 1995. 24 pp. Appears in 3rd IFAC/IFIP workshop on Algoritms and Architectures for Real-Time Control, AARTC ’95 Proceedings, 1995, pages 613�628.

RS-95-59 Luca Aceto and Anna Ing� olfsd� ottir. On the Finitary Bisimulation. November 1995. 29 pp.

RS-95-58 Nils Klarlund, Madhavan Mukund, and Milind Sohoni. Determinizing Asynchronous Automata on In�nite Inputs. November 1995. 32 pp. Appears in Thiagarajan, editor, Foundations of Software Technology and Theoretical Computer Science: 15th Conference, FCT&TCS ’95 Proceedings, LNCS 1026, 1995, pages 456�471.

RS-95-57 Jaap van Oosten. Topological Aspects of Traces. November 1995. 16 pp. To appear in Application and Theory of Petri Nets: 17th International Conference, ICATPN ’96 Proceedings, LNCS, 1996.

RS-95-56 Luca Aceto, Wan J. Fokkink, Rob J. van Glabbeek, and Anna Ing� olfsd� ottir. Axiomatizing Pre�x Iteration with Silent Steps. November 1995. 25 pp. Appears in Bjerner, Larsson and Nordstr� om, editors, 7th Nordic Workshop on Programming Theory, NWPT ’7 Proceedings, 1995. To appear in Information and Computation.

RS-95-55 Mogens Nielsen and Kim Sunesen. Behavioural Equivalence for In�nite Systems - Partially Decidable! November 1995. Full version of paper to appear in Proceedings of the 17th International Conference on Application and Theory of Petri Nets, 1996.