The Microcosm Principle and Compositionality of
GSOS-Based Component Calculi
Ichiro Hasuo⋆
University of Tokyo, Japan

Abstract. In the previous work by Jacobs, Sokolova and the author, synchronous
parallel composition of coalgebras—yielding a coalgebra—and parallel composition of behaviors—yielding a behavior, where behaviors are identified with statesof the final coalgebra—were observed to form an instance of the microcosm principle. The microcosm principle, a term by Baez and Dolan, refers to the general
phenomenon of nested algebraic structures such as a monoid in a monoidal category. Suitable organization of these two levels of parallel composition led to a
general compositionality theorem: the behavior of the composed system relies
only on the behaviors of its constituent parts. In the current paper this framework is extended so that it accommodates any process operator—not restricted
to parallel composition—whose meaning is specified by means of GSOS rules.
This generalizes Turi and Plotkin’s bialgebraic modeling of GSOS, by allowing
a process operator to act as a connector between components as coalgebras.

1 Introduction
1.1

Structural Operational Semantics and Its Bialgebraic Modeling

Structural operational semantics (SOS) [20] is a well-developed mathematical tool for
defining operational semantics of a programming language. It is based on SOS rules
from which transitions between program terms are derived. SOS has been notably successful for process calculi: simple programming languages for concurrent processes.
Various syntactic formats—syntactic restrictions on SOS rules—have been proposed toensure good properties of SOS (see [1] for a survey); the GSOS format [6] is one of themost common among them.
a
In SOS for process calculi, dynamic behaviors of processes—such as (a; b) k b →(0; b) k b—are derived by structural induction on the construction of process terms.
In categorical terms, dynamics of processes (the former) are modeled by a coalgebra
while the set of process terms forms an initial algebra that supports structural induction(the latter); see e.g. [15]. It is Turi and Plotkin’s seminal work [22] that combines these
two on a categorical level, resulting in a bialgebraic modeling of SOS.
⋆

Thanks are due to Marcelo Fiore, Masahito Hasegawa, Bart Jacobs, Paul-André Melliès,
Bartek Klin, John Power, Ana Sokolova and Sam Staton for helpful discussions. Helpful comments from the reviewers for the earlier versions of this paper are gratefully acknowledged.
Supported by PRESTO Promotion Program, Japan Science and Technology Agency.

Basic bialgebraic modeling In the simplest setting in [22], a bialgebra is a carrier X
equipped with both algebra and coalgebra`structures: ΣX → X → F X. Typically,
the functor Σ for the algebra part is Σ = σ∈Σ ( )arity(σ) : Sets → Sets, a functor
that represents a process algebra signature Σ; and the other functor is F = (Pω )A :Sets → Sets, a functor for coalgebraic modeling of labeled transition systems (LTSs).
Here Pω denotes the finite powerset functor, and A is the set of labels. The algebra andcoalgebra structures are further subject to a certain compatibility condition via a naturaltransformation ΣF ⇒ F Σ; this natural transformation is what represents SOS rules.
The following two are almost only examples of such bialgebras in the literature.
– The one induced by the initial algebra ΣI → I (or, slightly more generally, a freealgebra). Here I is the set of Σ-terms. The induced coalgebra I → F I is the transition structure between process terms, which is what is derived in the conventional
SOS framework [20].
– The one induced by the final coalgebra Z → F Z (or, slightly more generally,a cofree coalgebra). Here Z is the set of “behaviors”—specifically bisimilarity
classes of states of LTSs (see e.g. [11, §1.3]).1 Existence of the induced algebra
structure ΣZ → Z implies that the process operators are well-defined modulo
bisimilarity, that is, bisimilarity is a congruence. As laid out shortly in §1.2, thisinduced algebraic structure is what is generalized in the current paper.
Bialgebraic modeling of GSOS rules It turns out, however, that only a very limited classof SOS rules can be represented by a natural transformation of the form ΣF ⇒ F Σ.
Therefore in [22] a couple of extensions of the above basic scheme are proposed; themost notable among which is for the GSOS format. It is such that: a natural transformation representing GSOS rules is of the form ΣF• ⇒ F Σ ∗ . Here Σ ∗ is thefree monad over Σ, with Σ ∗ X being the set of Σ-terms that can contain elementsof X as variables. The functor F• is the cofree copointed functor over F , concretely:F• X = X × F X. In [22] it is shown that any GSOS specification—a set of SOS rules
compliant with the GSOS format—can be represented by a natural transformation of
the form ΣF• ⇒ F Σ ∗ and vice versa. See [16] for an introduction to the development.
The idea of bialgebraic modeling of SOS has been further pursued by many authors.
See [16] and the references therein.
1.2

Parallel Composition of Coalgebras and the Microcosm Principle

In bialgebraic modeling, it is the elements of the carrier of a bialgebra that are combinedusing process operators. As described above, typical examples of such are: process
terms (combined syntactically); and “behaviors,” i.e. bisimilarity classes of LTS states(combined thanks to ‘bisimilarity is a congruence’).
However, the rise of component calculi as a foundation of component-based systemdesign (see e.g. [4, 7]) poses a new challenge. In component-based design it is existing
systems that are to be composed; and this lies out of the realm of bialgebraic modeling. Specifically, ‘existing systems’ do not always mean ‘process terms’: one may be
1“Bisimilarity” here is more precisely behavioral equivalence; they coincide for functors F thatweakly preserve pullbacks (see e.g. [15]). This is the case with F = (Pω )A .

given two LTSs S1 and S2 that are generated from two process terms written in two
different process calculi. ‘Existing systems’ do not necessarily mean their ‘behaviors’
either: given two LTSs S1 and S2 , calculating their full behaviors is usually expensive.
Therefore it is nice to be able to combine LTSs as they are—much like a product of two
automata (e.g. in [4]), where one takes the product of two state spaces.
This idea of combining LTSs as they are, using a process operator whose meaning is specified by SOS rules, has been in the literature implicitly or explicitly (e.g.
in [5, 8]). However this idea is often regarded as a “cosmetic” extension to SOS and its
mathematical/categorical foundation has not been systematically pursued.
In our previous work [14] we formalized combination of LTSs as: a functor k :Coalg(F )×Coalg(F ) → Coalg(F ) arising from a natural transformation syncX,Y :F X × F Y → F (X × Y ). If F = (Pω )A this allows us to model synchronous parallel composition of LTSs (but hardly any other operator). There the carrier of the LTS
cd(X → F X) k (Y → F Y ) is X × Y . The natural transformation sync specifies a“synchronization mechanism,” which represents a very limited class of SOS rules.
The operation k for composing LTSs yields a canonical opFk
FZ
eration k for composing “behaviors” like the one in the bial- F (Z × Z)kζζζkgebraic modeling (§1.1). Namely, behaviors are identified with
Z
×
Z
∼
Z
=
k
elements of the final coalgebra ζ : Z →F Z and k is inducedby the coinduction diagram on the right.
Furthermore in [14], the two composition operators
k : Coalg(F ) × Coalg(F ) −→ Coalg(F )andk : Z × Z −→ Z

with the latter being a coalgebra morphism k: ζ k ζ → ζ, are identified as an instanceof so-called the microcosm principle. It is a term coined in [2], referring to the phenomenon that: a category C and its object X ∈ C have the “same” algebraic structures,with X’s inner algebraic structure depending on C’s outer one. A prototypical example
is a monoid object X in a monoidal category C: they both have a multiplication operator (m : X ⊗ X → X and ⊗ : C × C → C); and the definition of m uses ⊗ in it. In [14]we formalized what the microcosm principle means—especially what is meant by the“same” algebraic structures on different levels C and X ∈ C—using Lawvere theories.
As an application we proved a compositionality result:kd)
beh(ckcd
X ×YZ
for any coalgebras X → F X and Y → F Y we have the
top diagram on the right commute, where maps like beh(c) beh(c)×beh(d) k
Z ×Z
are by coinduction (the bottom diagram). This reads: the beF beh(c)havior of the composed system c k d can be computed fromFX
FZ
the behaviors of c and d, using k. In particular—denotingcζ′′bisimilarity by ∼—we have that c ∼ c and d ∼ d implies
X beh(c) Z
c k d ∼ c′ k d′ , with regards to an appropriate choice ofinitial states.

1.3

Microcosm Interpretation of Full GSOS Rules

The state of art in [14] roughly correcomposing bothcomposing behaviors
sponds to the basic bialgebraic modLTSs & behaviors
eling in §1.1 where an SOS specifica- sync. k[22], ΣF ⇒ F Σ[14]tion is represented by a natural trans- full GSOS [22], ΣF• ⇒ F Σ ∗current workformation ΣF ⇒ F Σ (see the table).
The current work extends [14] by accommodating any process operator whose meaningis specified by GSOS rules. Some GSOS rules are shown below; we assume that the setof labels is N ∪ N ∪ {τ }, consisting of names, conames and the internal action.
aaaay → y′x → x′ y → y ′x → x′(kL)(kR)(kS YNC)aaτx k y → x′ k y
x k y → x k y′
x k y → x′ k y ′ax → x′(;L)
ax; y → x′ ; yabx 6→ (∀a ∈ A) y → y ′bx; y → y ′

a

(;R)

x → x′(!)
a!x → x′ k!x

a

a→0

(AT)

a

x → x′(( )∗ )x → x′ ; x∗
∗ a

We use these rules for constructing a new LTS from given LTSs. This means:ax → x′ in S
(kS YNC) is read asτ

x k y → x′ k y ′ay → y ′ in T
(kS YNC)(1)

in S k Twith an additional class of variables (S and T ) that tells in which LTS each transition takes place. The variables x, y here designate states of LTSs—unlike in the usual
reading where they designate process terms. Different variables can designate states of
distinct LTSs: in (1), x and x′ are states of S, while y and y ′ are of T .
1.4

A Technical Challenge: State Spaces

Think of the new reading of the rules (;R) and (!). The challenge is: what is the state
space of the sequential composition S; T ? We can start with X × Y —where X and Y
are the state spaces of S and T , respectively—denoting its element by x; y. According
to the rule (;R), however, a state x; y can “evolve” into y ′ , which is no longer in X × Y .
So the answer seems` to be X × Y + Y . But how about the replication !S ? One would
think of X + = 1≤n X n or X ω ; both seem plausible.
In this paper we introduce a uniform, syntactic and modular way of constructing
such a state space, so that it is compatible with the given set R of GSOS rules. We shallcall it an R-state space. The construction is syntactic in the sense that an R-state spaceconsists of rather simple sets like X1 × · · · × Xm , summed up over all the relevant
algebraic terms (Def. 2.10). The construction is modular because the R-state space for
a composed term t can be calculated using the state spaces for t’s subterms as building
blocks ((4) later). Such modularity is an essential property of an “algebra.”
As a technical tool in this construction we introduce the notion of term lineage
graph (TLG). A TLG is roughly a graph between two terms (thought of as parse trees)that keeps track of evolution of terms (like x; y 7→ y ′ in (; R) above).
Organization of the paper In §2, after fixing notations for GSOS rules we describe
the construction of R-state spaces. In §3 we present a GSOS specification as a natural

transformation: this generalizes ΣF• ⇒ F Σ ∗ in [22] (for composing different LTSs)
as well as syncX,Y : F X × F Y → F (X × Y ) in [14] (for the full GSOS format).
This results in the two interpretations of process operators in §4, acting on LTSs andon behaviors. We prove a compositionality result, and show that our framework indeed
generalizes the GSOS fragment of [22]. In §5 we conclude and discuss related work.

2 State Space Compatible with GSOS rules
2.1

GSOS specification

We first fix a signature Σ of a process calculus. For each n ∈ N it determines the set
Σn of n-ary operators.
Definition 2.1 (GSOS) A GSOS rule R (as in [22]) over a signature Σ is a syntactic
expression of the following form.
aa∈A,j∈[1,Nia ]{xi → yia,j }i∈[1,m]bi{xi 6→ }b∈Bi∈[1,m]e(2)

σ(x1 , . . . , xm ) → t
Here A is a fixed set of labels; xi , yia,j are distinct variables; Nia is a natural numberthat is 0 for almost every i and a; Bi is a (possibly infinite) subset of A; σ is an m-ary
operator in Σ; and t is a Σ-term where only xi and yia,j occur as variables. For a GSOS
rule R like (2), the operator σ on the left in the conclusion shall be denoted by σR ; theterm t on the right is denoted by tR .
A GSOS specification is a pair (Σ, R) of a signature Σ and an image-finite set R
of GSOS rules over Σ. Here image-finiteness means that there are only finitely manyrules in R, once σ ∈ Σ and c ∈ A are fixed.
Our another reading of (2)—in the sense of (1)—is as follows, deriving a transition
in a new LTS σ(S1 , . . . , Sm ).
aa∈A,j∈[1,Nia ]{xi → yia,j in Si }i∈[1,m]eσ(x1 , . . . , xm ) → tbi{xi 6→ in Si }b∈Bi∈[1,m]in σ(S1 , . . . , Sm )Here S1 , . . . , Sm are a new class of variables that designate LTSs; variables xi and yia,jwith a subscript i therefore designate states of Si .
We will need a careful inspection of the structure of Σ-terms. We fix some notations.
Notation 2.2 We assume that a Σ-term t always comes with an explicit context ofvariables: x1 , . . . , xm ⊢ t. Any occurrence of a variable in t must be that of x1 , x2 , . . .
or xm ; each variable xi can have multiple or no occurrences in t. For example, we
distinguish two terms x1 ⊢ x1 k x1 and x1 , x2 ⊢ x1 k x1 because of different contexts.
In the sequel, however, we suppress the context of a Σ-term when it is obvious.

Definition 2.3 (it , |t| and tℓ ) Given a Σ-term x1 , . . . , xm ⊢ t, the number of occurrences of variables in t is denoted by |t|. Note that this is not necessarily the same as m.
Then the term t induces an “indexing” function it : [1, |t|] → [1, m] such that: the i-th
occurrence of variables (counted from left to right) in t is that of xit (i) .
The term obtained from t, by replacing all the occurrences of variables by those of
distinct variables x1 , . . . , x|t| from left to right, is denoted by tℓ . This is the linear term
induced by t. An easy consequence is: t = tℓ [xit (1) /x1 , . . . , xit (|t|) /x|t| ].
For example, let t be the term x1 , x2 ⊢ x2 k (x1 k!x1 ). Then |t| = 3, it : 1 7→
2, 2 7→ 1, 3 7→ 1. The term tℓ is x1 , x2 , x3 ⊢ x1 k (x2 k!x3 ).
2.2

Requirements on State Spaces

Shortly we will introduce the notion of term lineage graph (TLG). Since it is technicallyrather involved, we shall first lay out what we aim to achieve using TLGs.
We construct state spaces for LTSs like S1 k S2 , S1 ; S2 , !S, etc., deriving fromgiven GSOS rules. Let x1 , . . . , xm ⊢ t be a Σ-term and X1 , . . . , Xm be sets, with
the idea that Xi is the state space of the LTS Si . We shall define an R-state space
LtM(X1 , . . . , Xm ). The following requirements are essential to to base the frameworkin [14] on it; these will be exploited in the technical development later in §3.
~ should accommodate initial states that are there
Requirements 2.4 1. The set LtM(X)prior to any evolution—such as x1 k x2 in S1 k S2 or !x in !S (see §1.4). The setof such initial states are given by|t|(X1 , . . . , Xm ) := Xit (1) × · · · × Xit (|t|) ,(3)~ need not be the same as X1 ×
where it and |t| are from Def. 2.3. Note that |t|(X)· · · × Xm . Our definition (3) implies, for example, that we allow x1 k x′1 (withx1 , x′1 ∈ X1 and x1 6= x′1 ) as an initial state in an LTS S1 k S1 .
~ should also accommodate those states which would arise through2. The set LtM(X)“evolution” specified by GSOS rules (see §1.4).
3. Functoriality: the operation LtM extends to a functor Setsm → Sets.
4. Modularity: the operation L M—applied to a term t and yielding a functor LtM :Setsm → Sets—is compatible with substitution of terms. That is,~ . . . , Ltn M(X)~.
(4)
L t[ti /xi ] M (X1 , . . . , Xm ) ∼= LtM Lt1 M(X),
2.3

Term Lineage Graph (TLG)

First we note that a Σ-term t can be identified with its parse tree. Its leaves
are variables and 0-ary operators; and its internal nodes are operators withpositive arities with a suitable branching degree. For example the term
x1 k!x1 is understood as on the right.

k
x1

!
x1

Definition 2.5 (Term lineage graph) Let s, t be Σ-terms. We require them to be in thesame variable context (Notation 2.2): x1 , . . . , xm ⊢ s, t. A term lineage graph (TLG)
ρ from s to t, denoted by ρ : s ⇒ t, is an unlabeled directed graph (like in (5)) whose
nodes are nodes of s and t (seen as parse trees), such that:– any edge is from a node in the domain term s to a node in the codomain term t;– each node in s has exactly one outgoing edge;– the edges are monotone: assume that the origin of one edge is a descendant (in theparse tree s) of the origin of another edge. Then the target of the former is also adescendant of (or the same as) that of the latter;– an edge from an operator symbol σ goes into a (not necessarily the same) operator
symbol;– an edge from a variable xi in s goes into the same variable xi in t.
A TLG is sometimes denoted by x1 , . . . , xm ⊢ ρ : s ⇒ t, making its context explicit.
Definition 2.6 (The TLG ρR ) Let R be a GSOS rule of the form (2). It induces a TLG
ρR defined as follows. Its type is ρR : tR [xi /yia,j ] ⇒ σR (x1 , . . . , xm ). Concretely– each node in the domain term tR [xi /yia,j ] that is labeled with an operator symbol
is tied to the root node (labeled with σR ) of the codomain term σR (x1 , . . . , xm );– each node in the domain term that is labeled with a variable xi is tied to the uniqueoccurrence of the same variable xi in the codomain σR (x1 , . . . , xm ).
Intuitively, the substitution yia,j 7→ xi in the domain term tR [xi /yia,j ] forces every
occurrence of a state of Si to be denoted by xi .
Here are some examples of TLGs induced by GSOS rules. The solid lines represent
the order in each parse tree; the dotted lines are the edges of the TLGs.
ρ(( )∗ )

ρ(!)

=⇒

k
x1

x1

!
x1

=⇒

x2

=⇒

;

ρ(;R)

!

;
x1

x1

x2

( )∗

( )∗
x1

(5)

x1

Definition 2.7 (Operations on TLGs) – (Identity) For each Σ-term s, the identity
TLG ids : s ⇒ s is the one in which each node in the domain term is tied to thesame node of the codomain term.
– (Composition) Given two successive TLGs ρ : t ⇒ s and ρ′ : s ⇒ u, the composition ρ′ • ρ : t ⇒ u is obtained by composing two successive edges of ρ and ρ′ ,and then forgetting about the mediating term s.
– (Substitution) Let x1 , . . . , xn ⊢ ρ : t ⇒ t′ be a TLG. Assume further that we havea TLG x1 , . . . , xm ⊢ ρi : ti ⇒ t′i , for each i ∈ [1, n].2 We define the substitution
ρ[ρi /xi ], which is a TLG between substituted terms from t[ti /xi ] to t′ [t′i /xi ], asfollows. Pictorially:ρ
ρ

=⇒

x1

x2

t
t1

2
=⇒

t′1

t1

x1

x2

ρ

1
=⇒

t′

t

t2

x1
ρ[ρ1 /x1 ,ρ2 /x2 ]

=⇒

t2

t′2

t′
t′1

t′1

That is,2

Distinguish m and n. Note we have the same context for all of ρi .

t′2

• Each node in the (upper) t-part of the domain term t[ti /xi ] has the same outgoing edge as in ρ, into the t′ -part of the codomain term.
• As for a node in the (lower) ti -part of the domain term: basically the outgoingedge is the same as the corresponding one in ρi : ti ⇒ t′i . However, like t′1
in the above example, there can be multiple occurrences of t′i in the codomain
term; we must decide which occurrence the edge points to. There we use theinformation in ρ : t ⇒ t′ : we follow the edge in ρ that starts from the corresponding occurrence of a variable.
Let us now illustrate the operations on TLGs. Using three TLGs ρ(;R) : x2 ⇒ x1 ; x2 ,idx1 : x1 ⇒ x1 and idx∗1 : x∗1 ⇒ x∗1 , we can form the substitution ρ(;R) [idx1 /x1 , idx∗1 /x2 ]that is shown below on the left. The equality below asserts that, if we pre-compose
ρ(( )∗ ) to that substitution, then it is the same as the identity TLG.
ρ(;R) [idx1 /x1 ,idx∗ /x2 ]

( )∗

=⇒

x1

1

;

x1

ρ(( )∗ )

=⇒
∗

( )
x1

id ∗

( )∗
x1

=

( )∗
x1

x
=⇒

( )∗

(6)

x1

Finally, a given set R of GSOS rules determines a class of TLGs that are relevant to it.
Definition 2.8 (R-TLG) Let (Σ, R) be a GSOS specification (Def. 2.1). The class of
R-TLGs is a subclass of TLGs between Σ-terms, defined inductively as follows: 1) for
each GSOS rule R ∈ R, the induced TLG ρR (Def. 2.6) is an R-TLG; 2) the class of
R-TLGs is closed under identities, composition, and substitution (Def. 2.7).
2.4

R-State SpaceWe define an R-state space operator LtM. Let us fix a GSOS specification (Σ, R).
Definition 2.9 (Initial state space) Given a Σ-term x1 , . . . , xm ⊢ t, we define the initial state space functor |t| : Setsm → Sets by (3) in §2.2. Its functoriality is obvious.
We are overriding the notation |t| (cf. Def. 2.3); this will not cause any confusion.
Definition 2.10 (R-state space) Let t be a Σ-term. We define the R-state space functor LtM : Setsm → Sets by:a
LtM(X1 , . . . , Xm ) :=|s|(X1 , . . . , Xm ) | ρ : s ⇒ t, R-TLG

.

(7)

`

Here |s| is the initial state space functor (Def. 2.9); the sum
is taken over all the
R-TLGs ρ with a codomain term t. We have one summand for each ρ, not for each s.
Let us now calculate some R-state spaces. We take as R the set of rules presented
in §1.3; we take the corresponding signature Σ = {k, !, ; , ( )∗ } ∪ {a | a ∈ A}.
For a rule R ∈ R whose principal operator is k—namely (kL), (kR) and (kS YNC)—
the induced TLG ρR coincides with the identity (Def. 2.7). It follows that any R-TLG ofthe form · ⇒ x1 k x2 is the identity TLG. Hence by (7) we have Lx1 k x2 M(X1 , X2 ) =|x1 k x2 |(X1 , X2 ) = X1 × X2 .
For the operator ; , an R-TLG whose codomain term is x1 , x2 ⊢ x1 ; x2 is either the identity or ρ(;R) (see (5)). Hence Lx1 ; x2 M(X1 , X2 ) = |x1 ; x2 |(X1 , X2 ) +|x2 |(X1 , X2 ) = X1 × X2 + X2 . Here the term x2 inside the expression |x2 | is x1 , x2 ⊢
x2 , to be precise about its context.
Regarding ! , we have countably many R-TLGs
idx kx [ρ(!) /x2 ]
ρ(!)
1
2
=⇒
=⇒
whose codomain is !x1 :kk!
id : !x1 ⇒ !x1 ,ρ(!) : x1 k!x1 ⇒ !x1 ,ρ(!) • (idx1 kx2 [ρ(!) /x2 ]) :

x1

x1

k
x1

x1 k (x1 k!x1 ) ⇒ !x1 , etc.

!
x1

!

x1

x1

The third one is depicted above. Therefore we have:aa
L !x1 M(X1 ) =X1i+1 = X1+ .
x1 k (· · · k (x1 k!x1 ) · · · ) (X1 ) =
{z
}
|
i≥0

i

i≥0

Regarding ( )∗ , from the equality (6) it follows that the situation is similar to! above. Namely, we have one R-TLG for each of the following types: x∗1 ⇒ x∗1 ,x1 ; x∗1 ⇒ x∗1 , x1 ; (x1 ; x∗1 ) ⇒ x∗1 , etc. Hence we have Lx∗1 M(X1 ) = X1+ .
We now verify that Requirements 2.4 are indeed fulfilled. The item 3 is obvious.
The proof is in [12, Appendix A].
~ → LtM(X).
~ This
Proposition 2.11 1. There is a canonical embedding (νt )X~ : |t|(X)mextends to a natural transformation νt : |t| ⇒ LtM : Sets → Sets.
~ → LtM(X).
~
2. Given an R-TLG ρ : s ⇒ t, it induces a canonical map LρMX~ : LsM(X)It also extends to a natural transformation LρM : LsM ⇒ LtM.
4. The operation L M is compatible with substitution: for Σ-terms x1 , . . . , xn ⊢ t andx1 , . . . , xm ⊢ ti for each i ∈ [1, n], we have a canonical isomorphism (4).
⊓⊔Using the embedding (νt )X~ in Prop. 2.11.1, we can also embed the set X1 × · · · × Xmin the R-state space LtM(X1 , . . . , Xm ). This is by the following θX1 ,...,Xm :θX~ :=X1 × · · · × Xm(ψt )X1 ,...,Xm−→(νt ) ~

~ −→X LtM(X)~Xit (1) × · · · × Xit (|t|) = |t|(X)



, (8)

where (ψt )X~ is a function such that (x1 , . . . , xm ) 7→ (xit (1) , . . . , xit (|t|) ) (cf. Def. 2.3).
It rearranges arguments x1 , . . . , xm according to the occurrences of variables in t.
Remark 2.12 Our choice of state spaces (Def. 2.10) is in fact one out of a spectrum.
The smallest extreme in the spectrum is obtained by: singling out the “reachable” partof our R-state space and then quotienting it out by the bisimilarity. Although this yields
a smaller state space, calculating such is expensive. Moreover it does not satisfy Requirements 2.4.4, breaking modularity/algebraicity of the whole framework.
The biggest extreme is to take, as the state space LtM(X1 , . . . , Xm ), the whole setof Σ-terms with all states xi ∈ Xi as variables. This satisfies Requirements 2.4 so we
could develop the theory on top of it. However, we claim it to be our finding that wecan trim down this big state space into the one in Def. 2.10. In particular, our refined
definition yields L k M(X1 , X2 ) = X1 × X2 which matches with intuition as well as withthe usual definitions of product of automata in e.g. [4].
In-between is the “Kleene-style” composition of automata. The classic result on
regular language and DFA/NFA has recently seen its vast generalization in coalgebraic
terms; see e.g. [21]. In this approach the Kleene star ( )∗ preserves finiteness of state
spaces, whereas our approach yields the state space X ∗ that is inevitably infinite. However the definition of Kleene-style composition calls for different ingenuity for each
operator; it is not clear if that can be done uniformly for any operation defined in GSOS.
We further note that our choice goes well with first-order representation of LTSs.
(Variants of) the latter are now widely used (e.g. CARML in [3]) because it enables
BDD-based representation and symbolic model checking [9]. In first-order representation, a state is represented by an assignment of values to variables such as [agent1 7→
critical, agent2 7→ noncritical]; hence a state space is the product of the value
domains for the variables. Combining such state spaces by means of products and coproducts (7) could be done in a programming language with advanced type constructors.

3 Categorical GSOS Specification
We introduced appropriate state spaces for S1 k S2 , S1 ; S2 , etc. in §2; we wish to derivetransition structures on those state spaces, making them LTSs. In concrete terms it is via
derivations using GSOS rules, with their reading like (1). In categorical terms, GSOS
rules are first translated into a natural transformation ξt (for each term t, this section);
which gives rise to transition structures (§4).
3.1

Copointed Functors and Copointed Coalgebras

We will need the following notion of copointedness—a technical but standard one in
the field (see e.g. [18, 22]). For the functor F = (Pω )A : Sets → Sets, we set afunctor F• : Sets → Sets by F• X := X × F X = X × (Pω X)A . We denote the firstprojection F• X(= X × F X) → X by εX .
An F• -coalgebra c : X → F• X is said to be copointed if theεX
FXX
diagram on the right commutes. Intuitively, the additional com- X ×cponent X in F• X = X × F X records the “original” state beforeX
a transition; indeed for a copointed F• -coalgebra c : X → X × (Pω X)A we haveac(x) = ( x, λa. {x′ | x → x′ } ). The next result is standard and easy; see [18].
Lemma 3.1 Let us denote the category of F -coalgebras by Coalg(F ); and the category of copointed F• -coalgebras by Coalg• (F• ). The two categories are isomorphic:
Coalg(F ) ∼= Coalg• (F• ). In particular, Coalg• (F• ) has a final object (a final copointed F• -coalgebra) that corresponds to a final object in Coalg(F ).
⊓⊔Due to this result, in the sequel we identify an LTS with a copointed coalgebra for thefunctor F• X = X × (Pω X)A . Bisimilarity in LTSs can then be captured by the final
copointed F• -coalgebra—which we denote by ζ• : Z → F• Z. Note that the coalgebraζ• has the same carrier set Z as the final F -coalgebra; this is also a standard fact.

3.2

GSOS Rules, Categorically

We shall translate a set R of GSOS rules into functions of the following type:(ξt )X~ : LtM( F• X1 , . . . , F• Xm ) −→ F• LtM(X1 , . . . , Xm ) ,(9)defined for each Σ-term x1 , . . . , xm ⊢ t and sets X1 , . . . , Xm . Here F = (Pω )A ,and m is the length of t’s context x1 , . . . , xm ⊢ t. These functions (ξt )X~ form a naturaltransformation ξt , defined for each term t. The difference from the natural transformation ΣF• X ⇒ F Σ ∗ X in [22] is that ours (ξt )X~ is required to be natural in multiple
sets X1 , . . . , Xm . This is because we deal with state spaces of multiple LTSs.
Towards the natural transformation ξt in (9) we proceed step by step: we first derive(1)(2) (3)from a GSOS rule R a natural transformation ξR , from which we derive ξR , ξσ , . . . ,finally reaching ξt of the desired form.
Step 1. Let R ∈ R be a GSOS rule in (2). It induces the following function(1)(ξR )X1 ,...,Xm :(1)`´(ξR ) ~
|σR | (F• X1 , · · · , F• Xm ) −→X F |tR [xi /yia,j ]| (X1 , . . . , Xm ) ,
(1)
“˛
” ”A
˛
`
´ (ξR
)~ “
Q
A
~
i.e.
−→X Pω ˛ tR [xi /yia,j ] ˛(X)i∈[1,m] Xi × (Pω Xi )
` (1)
´
by
(ξR )X~ (x1 , ϕ1 , . . . , xm , ϕm ) (e)ﬀ
˛a,ja,j ˛ ∀i. ∀b ∈ Bi . ϕi (b) = ∅, and= tR [xi /xi , yi /yi ] ˛.
∀i. ∀a. ∀j ∈ [1, Nia ]. ya,j
∈ ϕi (a).
iHere xi and ya,jdenote elements of Xi ; ϕi belongs to (Pω Xi )A ; and e ∈ A is a label.
i
Note that |σR |(F• X1 , · · · , F• Xm ) = F• X1 × · · · × F• Xm (Def. 2.9). The expressiona,ja,jtR [xi /xi , ya,ji /yi ] denotes the obvious element of the set | tR [xi /yi ] |(X1 , . . . , Xm ).
To be precise, the latter set is of the form Xk1 × · · · × Xk|tR | , with each component
Xkl coming from an occurrence of either xi or yia,j in tR . If Xkl is from xi then thea,ja,jthen it is ya,jl-th component of tR [xi /xi , ya,ji .
i /yi ] is xi ; if Xkl is from yi
Step 2. We exploit properties of L M (Prop. 2.11.1–2) to obtain the following two
successive functions. Here ρR is the R-TLG induced by the GSOS rule R (Def. 2.6).
a,j
a,j
~
~
(νt [x /ya,j ] )X
~ : | tR [xi /yi ] |(X) −→ L tR [xi /yi ] M(X) ,
R i
i
a,j
~
~
LρR M ~ : L tR [xi /y ] M(X) −→ LσR M(X) .
Xi

The functions are natural in X1 , . . . , Xm . We compose these arrows, apply the functor(1)
F , and then post-compose it to (ξR )X~ in Step 1. The outcome is a natural transforma
(2)tion (ξR )X1 ,...,Xm : |σR | (F• X1 , · · · , F• Xm ) −→ F LσR M (X1 , . . . , Xm ) .
(2)
Step 3. The natural transformation ξR has been defined for each rule R ∈ R;(3)
we shall take their “union” to define ξσ , now for each operator σ ∈ Σ. Specifically,for each operator σ ∈ Σ and e ∈ A, let Rσ,e denote the collection of those rulese
R ∈ R whose conclusion is of the form σ(x1 , . . . , xm ) → · . By the image finitenessassumption (Def. 2.1) the set Rσ,e is finite. We define a function`´(3)(ξσ )X~ : |σ| (F• X1 , · · · , F• Xm ) −→ F LσM (X1 , . . . , Xm )` (3)´by ξσ (x1 , ϕ1 , . . . , xm , ϕm ) (e)
` (2)
´
S
:= R∈Rσ,e ξR (x1 , ϕ1 , . . . , xm , ϕm ) (e) .

~Recall that F X = (Pω X)A and F• X = X × (Pω X)A ; the union is in Pω (LσM(X)).
(3)(4)
Step 4. We shall extend F in the codomain of ξσ to F• , so that we obtain (ξσ )X~ :
−−→
−−→
~
|σ|(F• X) → F• (LσM(X)).
What we need is a function of the type |σ|(F• X) →~ then we can tuple it with ξσ(3) and obtain ξσ(4) . Such a function is given by
LσM(X);)X−−→ |σ|(ε~X )~~ (ν−σ→~ .
|σ|(F• X ) −→ |σ|(X)
LσM(X)

Here εXi : F• Xi → Xi is the first projection (§3.1); νσ is from Prop. 2.11.1. We used
the functoriality of the operation |σ| (Def. 2.9).
−−→
(4)
(4)
~
We shall further extend this definition of ξσ to (ξt )X~ : |t|(F• X) → F• (LtM(X)),
now defined for each Σ-term t. This is by induction on the formation of Σ-terms.
−−→
If t is a variable xi (i.e. x1 , . . . , xm ⊢ xi ), we have |xi |(F• X) = F• Xi (Def. 2.9)
~ = Xi (Def. 2.10, the only R-TLG into xi is the identity). Hence theand Lxi M(X)(4)
function (ξxi )X~ we are defining is of the type F• Xi → F• Xi ; it is defined to be the(4)identity. If t is a composed term σ(s1 , . . . , sn ), we define (ξt )X~ by the composite:|σ(s1 , . . . , sn )|(F• X1 , . . . , F• Xm )
∼
=
´
` (4)
(4)
|σ| (ξs1 )X~~ , . . . , (ξsn )X(4)(ξσ )Ls1 M(X),...,Ls~~n M(X)
∼
=

`
−−→
−−→ ´
|σ| |s1 |(F• X), . . . , |sn |(F• X)`´~~|σ| F• (Ls1 M(X)),. . . , F• (Lsn M(X))``´´~ . . . , Lsn M(X)~F• LσM Ls1 M(X),`´F• Lσ(s1 , . . . , sn )M(X1 , . . . , Xm ) .

Here the first isomorphism is a variant of (4), for | | instead of L M, which we readily(4)
obtain. The second one uses functoriality of |σ| applied to functions (ξsi )X~ ; the latterare available by the induction hypothesis. The third function is what we defined in thefirst half of the current Step 4; the last isomorphism is by Prop. 2.11.4.
Step 5. Finally we shall obtain the goal (9) of the current §3.2, by extending |t|−−→(4)~ By Def. 2.10
into LtM in the domain of the previous (ξt )X~ : |t|(F• X) → F• (LtM(X)).
of LtM, such an extension can be done through finding, for each R-TLG ρ : s ⇒ t, a−−→
~ The following composite does this job.
function of the type |s|(F• X) → F• (LtM(X)).
(ξs(4) ) ~~|s|(F• X1 , . . . , F• Xm ) −→X F• (LsM(X))

F• (LρMX~)−→~F• (LtM(X))

Here LρM is from Prop. 2.11.2. We take the cotuple of these functions (i.e. definition bycases) to obtain (ξt )X~ .

4 The Microcosm Interpretation of GSOS Rules
Let (Σ, R) be a GSOS specification. We shall define its microcosm interpretation. It
consists of, for each Σ-term x1 , . . . , xm ⊢ t,mthe outer interpretation JtK : Coalg• (F• )→ Coalg• (F• ) ; andthe inner interpretation [t] : Z m → Z .

Recall (§3.1) that we identify an LTS with c ∈ Coalg• (F• ). Hence the outer interpretation is a “process operator” t acting on LTSs. Therefore the two interpretations
combined constitute an instance of the microcosm principle; see §1.2.
Definition 4.1 Let (Σ, R) be a GSOS specification, and t be a Σ-term.
1. We define t’s outer interpretation JtK : (Coalg• (F• ))m → Coalg• (F• ) as follows, using functoriality of LtM. The function (ξt )X~ was introduced in §3.2 as “categorical GSOS rules.” Functoriality of thus defined JtK is easy.
F • Xm 
c1, . . . , cm
Xm
X1

 F • X1

JtK

7−→

`
´
F• LtM(X1 , . . . , Xm )(ξt )X1 ,...,Xm
LtM(F• X1 , . . . , F• Xm )LtM(c1 , . . . , cm )LtM(X1 , . . . , Xm )~The copointedness (§3.1) of the resulting F• -coalgebra is easy, too. It has LtM(X)—
the R-state space from §2—as a carrier.
2. We define t’s inner interpretation [t] : Z m → Z as follows. Once we have the outerinterpretation JtK, we can apply it to the m-tuple (ζ• , . . . , ζ• ) of the final copointed
coalgebra ζ• : Z → F• Z. Then the resulting coalgebra JtK(ζ~• ) induces a unique“behavior” map into the final one, as below. This behavior map is almost what we~ (from (8)) to it and obtain [t]. Thatwant; we pre-compose θZ,...,Z : Z m → LtM(Z)m~is, [t] := beh(JtK)(ζ• ) ◦ θZ~ : Z → Z.
~
F• (LtM(Z))

F• Z

JtK(ζ~• )~LtM(Z)

ζ•
beh(JtK(ζ~• ))

final

Z

Proposition 4.2 (Modularity) Assume Σ-terms t and ti are as in Prop. 2.11.4. The
operations J K and [ ] are compatible with substitution: given LTSs c1 , . . . , cm ∈Coalg• (F• ) and “behaviors” z1 , . . . , zm ∈ Z, we haveJ t[ti /xi ] K (c1 , . . . , cm ) ∼= JtK Jt1 K(~c), . . . , Jtn K(~c) ;[ t[ti /xi ] ] (z1 , . . . , zm ) = [t] [t1 ](~z), . . . , [tn ](~z) .
⊓⊔We present our main result on compositionality. It relates the outer and inner interpretations. The latter arose from the former via finality (Def. 4.1); the following result
follows straightforward from finality, too.
Theorem 4.3 (Compositionality) Given a Σ-term x1 , . . . , xm ⊢ t and LTSs c1 , . . . , cm
that belong to Coalg• (F• ), we have the following diagram commute.
X1 × · · · × Xm(θt )X1 ,...,Xm
LtM(X1 , . . . , Xm )beh(c1 ) × · · · × beh(cm )beh(JtK(c1 , . . . , cm ))Z × ··· × Z[t]ZHere (θt )X1 ,...,Xm is the “bookkeeping” function from (8); Z is the carrier of the final
coalgebra (§3.1). Putting it equationally: for any state xi ∈ Xi of each LTS we have
beh JtK(c1 , . . . , cm ) ( θt (x1 , . . . , xm ) ) = [t] beh(c1 )(x1 ), . . . , beh(cm )(xm ) .
That is: the behavior of a composed system JtK(~c) can be computed from the behaviorsbeh(ci ) of its constituent parts, using the inner operator [t].
⊓⊔Let ζ̂ : Σ ∗ Z → Z be the (Eilenberg-Moore) Σ ∗ -algebra on Z induced by a GSOS
specification (Σ, R), due to [22, Cor. 7.2]. Here Σ ∗ is the free monad induced by thesignature Σ. The following result—claiming that our framework is indeed an extensionof (the GSOS fragment of) [22]—holds because our ξt in §3, when suitably restricted,
coincides with the categorical GSOS in [22].
Theorem 4.4 Let x1 , . . . , xm ⊢ t be a Σ-term; let κt be the correΣ∗Z
sponding coprojection Z m ֒→ Σ ∗ Z. For these, the diagram on the κtright commutes.
⊓
⊔ Zm

ζ̂

Z

[t]

5 Conclusions and Future Work
We have extended our previous work [14] so that any process operator specified by
GSOS rules can now be interpreted as a component connector that combines LTSs as
components. This outer interpretation gives rise to a canonical inner interpretation thatcoincides with what is derived by the bialgebraic modeling of SOS [22].
Our framework is categorical, hence comes with great potential generality. This
includes application to systems other than LTS—like bialgebraic modeling applied toweighted systems [17]—which we wish to pursue. In particular we believe our genericconstruction of R-state spaces will carry over.
Regular languages and automata seem to be the first computer science example ofthe microcosm principle. Our current framework fails to include it. One difficulty is:
the outer operators (specified in GSOS-like rules) are naturally defined on NFAs, while
the inner operators is on regular languages that form the final DFA. Use of coalgebraic
techniques such as trace semantics [13] is being investigated.
The notion of TLG and operations on them (§2) indicates strong relevance of rewriting logic [19] and the theory of generalized operads/combinatorial species/clones recently pursued by many authors, including [10]. We are especially interested in thelatter, but not only because of TLGs. Roughly we can call their theory universal algebra in varying contexts. Here a “context” can be a monoidal one (where variables
are not to be deleted, duplicated or swapped), a symmetric monoidal one (where swapping is allowed), a Cartesian one (where all three are allowed), and so on. In fact sucha context can be thought of as algebraic structure itself; hence the theory may be also
called universal (algebra in algebra). The microcosm principle then offers a degenerate
example of such, where we have the same structure on the two levels.

References
1. Aceto, L., Fokkink, W., Verhoef, C.: Structural operational semantics. In: Bergstra, J., Ponse,
A., Smolka, S. (eds.) Handbook of Process Algebra, pp. 197–292. Elsevier (2001)
2. Baez, J.C., Dolan, J.: Higher dimensional algebra III: n-categories and the algebra of
opetopes. Adv. Math 135, 145–206 (1998)
3. Baier, C., Blechmann, T., Klein, J., Klüppelholz, S.: A uniform framework for modeling andverifying components and connectors. In: Field, J., Vasconcelos, V.T. (eds.) COORDINATION. Lect. Notes Comp. Sci., vol. 5521, pp. 247–267. Springer (2009)
4. Baier, C., Sirjani, M., Arbab, F., Rutten, J.J.M.M.: Modeling component connectors in reo
by constraint automata. Science of Comput. Progr. 61(2), 75–113 (2006)
5. Bliudze, S., Krob, D.: Modelling of complex systems: Systems as dataflow machines. Fundam. Inform. 91(2), 251–274 (2009)
6. Bloom, B., Istrail, S., Meyer, A.R.: Bisimulation can’t be traced. Journ. ACM 42(1), 232–268(1995)
7. Bonsangue, M.M., Clarke, D., Silva, A.: Automata for context-dependent connectors. In:
Field, J., Vasconcelos, V.T. (eds.) COORDINATION. Lect. Notes Comp. Sci., vol. 5521, pp.
184–203. Springer (2009)
8. Bruni, R., Lanese, I., Montanari, U.: A basic algebra of stateless connectors. Theor. Comp.
Sci. 366(1–2), 98–120 (2006)
9. Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)
10. Curien, P.L.: Operads, clones, and distributive laws (2008), preprint, available online
11. Hasuo, I.: Tracing Anonymity with Coalgebras. Ph.D. thesis, Radboud Univ. Nijmegen(2008)
12. Hasuo, I.: The microcosm principle and compositionality of GSOS-based component calculi.
Extended version with proofs, available online (May 2011)13. Hasuo, I., Jacobs, B., Sokolova, A.: Generic trace semantics via coinduction. Logical Methods in Comp. Sci. 3(4:11) (2007)
14. Hasuo, I., Jacobs, B., Sokolova, A.: The microcosm principle and concurrency in coalgebra.
In: Foundations of Software Science and Computation Structures. Lect. Notes Comp. Sci.,
vol. 4962, pp. 246–260. Springer-Verlag (2008)
15. Jacobs, B.: Introduction to coalgebra. Towards mathematics of states and observations(2005), Draft of a book, www.cs.ru.nl/B.Jacobs/PAPERS
16. Klin, B.: Bialgebraic methods and modal logic in structural operational semantics. Inf. &Comp. 207(2), 237–257 (2009)
17. Klin, B.: Structural operational semantics for weighted transition systems. In: Palsberg, J.
(ed.) Semantics and Algebraic Specification: Essays Dedicated to Peter D. Mosses on the
Occasion of His 60th Birthday, Lect. Notes Comp. Sci., vol. 5700, pp. 121–139. SpringerVerlag (2009)
18. Lenisa, M., Power, J., Watanabe, H.: Category theory for operational semantics. Theor.
Comp. Sci. 327(1–2), 135–154 (2004)
19. Martı́-Oliet, N., Meseguer, J.: Rewriting logic: roadmap and bibliography. Theor. Comp. Sci.
285(2), 121–154 (2002)
20. Plotkin, G.D.: A structural approach to operational semantics (1981), report DAIMI FN-19,
Aarhus Univ.
21. Silva, A., Bonchi, F., Bonsangue, M.M., Rutten, J.J.M.M.: Quantitative kleene coalgebras.
Inf. & Comp. 209(5), 822–849 (2011)
22. Turi, D., Plotkin, G.: Towards a mathematical operational semantics. In: Logic in Computer
Science. pp. 280–291. IEEE, Computer Science Press (1997)