CSP, partial automata, and coalgebras.
The paper presents a first reconstruction of Hoare's theory of CSP in terms of partial automata and related coalgebras. We show that the concepts of processes in Hoare (Communicating Sequential Processes, Prentice-Hall, Englewood Cliffs, NJ, 1985) are strongly related to the concepts of states for special, namely, final partial automata. Moreover, we show how the deterministic and nondeterministic operations in Hoare (1985) can be interpreted in a compatible way by constructions on the semantical level of automata. Based on this, we are able to interpret finite process expressions as representing finite partial automata with designated initial states. In such a way we provide a new method for solving recursive process equations which is based on the concept of final automata. The coalgebraic reconstruction of CSP allows us to use coinduction as a new proof principle. To make evident the usefulness of this principle we prove some example laws from Hoare (1985).
Introduction
For people usually working on model theory or semantics of formal specifications
it becomes often very hard to approach the area of process calculi and
process algebras.
There are processes without any physical basis. There is no difference
between concepts as machine, process, agent, state, and system. There is syntax
without semantics. There is no difference between processes and process
expressions. And so on.
The paper is devoted to make some steps to overcome these difficulties.
In contrast to the area of process calculi we insist on the clear intuition that
there is an essential difference between the concepts system (machine, agent),
state, and process, respectively. A system has different states and processes
are devoted to describe the (observable) behavior of systems, where two states
can be observed to be different indeed by the fact that different processes start
in these states.
This paper will be published in
Electronic Notes in Theoretical Computer Science, Volume 19
URL: www.elsevier.nl/locate/entcs
r
The aim of the paper is to make evident that CSP can be interpreted as
a theory of processes for special (deterministic and nondeterministic) partial
automata. The theory that allows to bring CSP and automata into a common
perspective is the theory of coalgebras [6]. We show the coincidence between
the concepts of processes in [4] and the concepts of states in final automata
(coalgebras). Moreover, we analyse how far the constructions and operations
in [4] on the level of processes can be related to and justified by corresponding
compatible constructions on the level of arbitrary automata. This analysis
will put many of the informal arguments and intuitions of Hoare to a formal
semantical level.
We insist also on a clear distinction between the concept of process and the
concept of process expression. Traditionally, process expressions are used for
a (finite) syntactical representation of processes and the algebraic laws in [4]
tell which process expressions denote the same process. Process expressions,
however, can be also seen in a compatible way as syntactical representations
of (finite) automata with initial states. Compatibility means that the process
starting in the corresponding initial state coincides with the process represented
by the same process expression. This observation offers a new method
to solve recursive process equations: A recursive process equation describes
a finite automaton with an initial state and the image of this state with respect
to the unique homomorphism into the final automaton (with processes
as states) is the solution of the recursive equation. We draw attention to the
fact that there is no need to impose a cpo structure on processes to describe
the solution of recursive equations by means of fixed point constructions in
cpo's. Within the coalgebraic approach the fixed point construction can be
seen as being shifted to an external level and as made only once, namely, if we
describe the final automaton (coalgebra) as the result of a category theoretic
fixed point construction.
We hope that the integrated view to CSP, automata, and coalgebras developed
in this paper will be a step in achieving unifications of theories in
computing science as advocated by Hoare in [5]. Such an integrated view,
however, has also a value for its own: It becomes easier to explain and to teach
process calculi. By relating operations on the level of processes to constructions
on the level of automata the possible and adequate scope of applications
of CSP becomes more clear for "users". Finally, I believe that a satisfactory
formal treatment of a phenomenon in computing requires to consider it
from different viewpoints and to understand well the transitions between these
different viewpoints.
Since the paper tries to bridge two apart areas it is written mainly for
two kinds of readers. Reader familiar with coalgebraic reasoning as presented,
e.g., in [6], can read the paper as an introduction to and an explanation of
basic concepts and ideas of CSP. Technically, there will be nothing really new
concerning the theory of coalgebras. Reader familiar with CSP or other process
calculi should be also able to read the paper. To convince this kind of
r
reader of the practical relevance of category theoretic and coalgebraic reasoning
we analyse the category theoretic fixed point construction of final partial
automata in some detail. Besides this, the paper is self-contained in a way that
anybody interested in the theory of processes can read it with some benefit.
The paper is organized as follows. In section 2 we introduce the concept
of deterministic process according to [4] and try to make apparent the strong
relationship to the concept of deterministic partial automaton. Thereby, it
turns out that processes are related to the curried version of partial automata,
as studied in [10], thus a coalgebraic treatment of processes appears to be quite
natural.
Section 3 explores the insight in [10] that (partial) automata in its curried
version should be considered as special coalgebras. We show how the general
category theoretic fixed-point construction of final coalgebras applies to deterministic
partial automata and that these general construction provides a
reasonable model of deterministic processes which turns out to be isomorphic
to the mathematical model presented in [4].
Section 4 makes evident that Hoare defines the interaction of processes
in a coalgebraic manner. Moreover, we show that interaction of processes
corresponds on the semantical level to the synchronization of automata, i.e.,
the processes in an arbitrary synchronized automaton can be desribed by the
interaction of the processes of the single components.
In section 5 we discuss Hoare's treatment of branching and internal non-determinism
which is based on the idea of acceptance (refusal) sets. We show
that the concept of nondeterministic processes in CSP corresponds to the
concept of deterministic filter automata.
Section 6 provides a semantical interpretation of the nondeterministic operations
in [4] on the level of automata and describes the elimination of internal
actions in automata.
Finally, Hoare's treatment of divergence is analysed in section 8. We
show that this treatment is based on a mixture of coalgebraic and algebraic
techniques.
We close the paper with some conclusions and remarks for further work.
Deterministic processes and automata
Fortunately and in contrast to other presentations of processes [4] owns a
mathematically rigour which allows to start immediately a more semantically
oriented analysis of the proposed concept of process. Firstly, Hoare assumes
for any process P a fixed set A of events (actions) in which the process may
engage. A is called the alphabet of P and is also denoted by ffP . The process
with alphabet A which never actually engages in any of the events of A is
called
Secondly, Hoare provides a clean notation for processes. The process
which first engages in the event a 2 A = ffP and then behaves exactly as the
r
process P is denoted by
Omitting brackets is allowed by the convention that ! is right associative.
In such a way a simple vending machine V MA that succesfully serves two
customers with chocolate before breaking can be described by the following
process expression
where ffV chocg. The process which initially engages in either
of the distinct events a after one of these alternative
first events a i has occured, behaves exactly as the process P i is denoted by
where we assume ffP define A to be also the alphabet
of (a Note, that the process denoted by the
process expression (a long as the
are deterministic since the events a are required
to be distinct.
A machine V MB that serves either chocolate or toffee before breaking can
be described now by the process expression
where ffV tofg.
Thirdly, Hoare states that every deterministic process P with alphabet
A may be regarded as a function F with a domain B ' A, defining the set of
events in which the process P is initially prepared to engage; and for each a in
B, the deterministic process F (a) defines the future behavior of the process P
if the first event was a. This means that every deterministic process P 2 DPA
can be uniquely described by a partial function F : A !p DPA with domain
stands for the set of all deterministic processes with
alphabet A.
Globally considered, Hoare assumes, in such a way, the existence of a
bijective mapping
nextA
where [A !p DPA ] denotes the set of all partial functions from A into DPA .
STOPA , e.g., is the process uniquely determined by the condition dom(nextA
i.e., the deterministic process which at all times
can engage in any event of A, can be described uniquely by the conditions
dom(nextA (RUNA A.
Taking into account the idea of automaton we see immediately that the set
of all deterministic processes with alphabet A can be seen as the set of states
of an infinite deterministic partial automaton without output. Traditionally
[1], a deterministic partial automaton without output is defined to be a triple
d) with I a set of input symbols, S a set of states, and d : S \Theta I !p S
r
a partial state transition function. It is well-known, however, that for any such
partial function there is an equivalent curried version, i.e., a total function
dom(-(d)(s)). In such a way an
automaton M can be described equivalently using the curried version of d by
the tripel (I; S; -(d)) as pointed out in [10].
That Hoare's concept of deterministic process can be really reflected by
a partial automaton (A; DPA ; nextA ) will be justified now by considering the
mathematical model of deterministic processes in [4]: A deterministic process
with alphabet A is defined to be any prefix closed subset P of A   , i.e., any
(non-empty) subset P 2 A   which satisfies the two conditions hi 2 P , and
denotes the empty trace (finite
sequence) and s-t the catenation of traces. The process STOPA is modeled
in this way by the set fhig and RUNA is given by A   itself. The domain of
nextA (P ) is denoted in [4] by P 0 and defined by dom(nextA (P
Pg. nextA (P )(a) for any a 2 P denoted in [4] by P (a)
and defined by nextA (P Pg.
From now on let DPA be the set of all prefix closed subsets of A   and the
partial automaton will be called the Hoare-model of
deterministic processes with alphabet A. Note, that nextA is bijective indeed
since we can assign to any partial function F : A !p DPA the prefix closed
set next \Gamma1
(a)g.
To make a clear distinction between processes and process expressions we
will use from now on identifiers instead of the (name of the) process
STOPA for building process expressions.
After realizing that the deterministic processes in CSP constitute special
partial automata it will be promising to take into consideration arbitrary partial
automata. The first observation will be that process expressions as, e.g.,
can be interpreted in two different ways.
Firstly, as suggested in [4], it can be interpreted as a "userfriendly" syntactic
notation of the prefix closed set V
of traces, i.e., as representing the element V MB of DPA .
Secondly, however, we can take vmb as a syntactic presentation of a finite
partial automaton
given by
3. This partial automaton can be
depicted as follows
coin '&%$/!''# 2
choctof
To make the translation of a process expression exp into a partial automaton
exp unambiguous we could use the subexpressions of exp to denote
the states of M exp as, e.g., (coin
instead of 3. Note, that this
approach forces us to identify the codomains of the two arrows starting from
(in contrast to the tree oriented pictorial presentation of processes in section
1.2 of [4]). Note, further, that this approach brings us more close to the
labelled transition systems used in [7] to reason about processes.
In the next section we will see that the Hoare-model HMA of deterministic
processes can be characterized by being a final object in the category of all
deterministic partial automata with alphabet (set of input symbols) A. This
means, that there exists for any deterministic partial automaton
mapping
s 2 S and a 2 A, where the left hand side of the equation is defined if, and
only if, the right hand side is defined.
[A !p S]
DPA
next A [A !p DPA
Note, that this condition is equivalent to the traditional condition for the
uncurried version of automata morphisms.
In our example to
fhig.
Both interpretations of a process expression are compatible because the
translation of a process expression exp into a deterministic partial automaton
exp points out implicitly an initial state in M exp , namely, the state that
corresponds to the whole expression exp, and this state will be maped by - Mexp
to the process P exp obtained by the "process interpretation" of the expression.
For our example we have, e.g., - Mvmb
Using prefixing and choice we can only build process expressions representing
finite deterministic processes. To be able to describe syntactically infinite
processes Hoare introduces recursion. Let X be an identifier (process vari-
able) and F (X) be a process expression build on X by prefixing and choice
using events from a fixed set A. The idea in [4] is that F (X) defines a map
DPA such that the recursive process equation can be
taken as the syntactic description of a deterministic process if there is exactly
one fixed point of [[F ]]. Hoare proves that this is the case as long as F (X)
is guarded, i.e., as long as there is at least one occurrence of ! in F (X). The
unique fixed point is denoted in [4] by the process expression
A machine VMC with alphabet A = fcoin; choc; tofg that either serves
chocolate or toffee in a loop can be described using the process expression vmb
above by the recursive equation where the corresponding unique
fixed point V MC 2 DPA is given by all traces from A   with coin at each odd
r
position and either choc or tof at each even position.
Fortunately the translation of process expressions into finite partial automata
with an initial state can be extended to recursion thus we obtain a new
method for solving recursive process equations: Let M F be the
finite partial automaton according to F (X) with the initial state s 0 2 S and
with s X 2 S the state that corresponds to the free variable X, i.e., for this state
we have especially dom(t(sX Than we obtain M -X
with initial state s 0 by glueing together s 0 and s
and define for all s 2 S 0 and all a 2 dom(t 0
Now the image of s 0 w.r.t. the unique automata morphism - M
can be taken as the deterministic process described by
the recursive equation
For our example we have arises by glueing
together the states 1 and 3 in Mvmb
ee
choc
yy
tof
and we have - M-X:A:vmb MC. If we consider as a further example the
process expression run
we obtain a "one-state" partial automaton M-X :A:run with - M-X:A:run
RUNA for the only state s 0 in M-X :A:run .
In the next section it will become, hopefully, evident that our method
provides for all process expressions build by identifiers, prefixing, choice, and
recursion the same results as the fixed point construction in [4].
Remark 2.1 That our method extends nicely to mutual recursion should be
obvious. But, as the fixed point construction in [4], our method works only for
guarded expressions. That is, for we have a one-state automaton
MX , i.e., we have s thus by construction M-X :A:X will have no states
at all. Analogously to [4] we will treat the meaning of -X:A:X when we
discuss nondeterministic operators in section 6.
Final coalgebras
For a -coalgebra is a pair (S; t) consisting of
a set S, the carrier of the coalgebra, and a mapping t
and consists of a mapping f which commutes with the
operations:
r
f
To apply this definition to deterministic partial automata we have only
to check that the assignment S 7! [A !p S] extends to a functor A! :
SET. For this we assign to any mapping f the mapping
It is easy to check that this defines in fact a functor A!
Now, the concepts "deterministic partial automata with alphabet A"and "A ! -
coalgebra" turn out to be obviously equivalent. The category of all A! -
coalgebras and all A!-homomorphisms will be denoted, therefore, by DAA .
Because the functor A! : SET ! SET is ! op -continuous [9], i.e., preserves
limits of ! op -chains, we can fortunately use the category theoretic
version of the least fixed point construction [11] to construct the final A! -
coalgebra: The limit (L; (- of an ! op -chain
in SET can be described canonically by all infinite sequences
such that a i 2 A i and f i (a . The mapping
projects to the i-th component a i thus we have -
for all i 2 N .

A 3
The carrier NFA of the intended final A! -coalgebra is given now according
to [9,11] by the limit (NFA ;
of the following
A 3
obtained by applying successively the functor A! to the unique mapping from
into the singleton set into the final object of
the category SET.
To see that NFA is strongly related to the set DPA of all prefix closed
subsets of A   we firstly consider the elements of A n
! (1), which can be refered to
as nested functions of depth less than or equal to n. For
has four functions as elements and by using the maps-to-
notation we get A! )g.
r
A pictorial representation could look as follows
coin
choc
coin
\Upsilon\Upsilon
choc

wich can be depicted by
coin
coin
choc
coin
coin
choc
@
@
@
@
@
@
@
choc
coin
\Upsilon\Upsilon
choc

Note, that we make a difference between fully undefined function
of type A 2
the fully undefined function of type
Note, further, that nested functions are different from synchronization trees
[7,13]. That is, a node in our pictures represents the graph below this node in
contrast to synchronization trees where a node represents the path from the
root of the tree to this node.
each function in A! to   thus A!
maps each g 2 [A !p [A !p 1]] to
a In general A n
(1) cuts the (possibly empty)
1)-th layer of a nested function where the information that a cutting has
taken place is announced by writing   at the corresponding node at depth
n. Moreover, all nodes ; (n+1)\Gammai at depth i ! n are changed to ; n\Gammai and, if
necessary, new sharings are introduced.
For our example we have A!
we have the following transformation
of nested functions
coin
coin
coin
choc
@
@
@
@
@
@
@
coin
\Upsilon\Upsilon
choc
coin
\Upsilon\Upsilon
choc

Remark 3.1 The elements of NFA are by construction infinite sequences
of nested functions with
That is, the elements of A n
! (1) do not correspond directly to
r
the elements of DPA . They represent finite approximations of processes. For
the prefix closed set P ng of bounded traces
corresponds uniquely to a nested function in A n
(1) where   at depth n in the
corresponding nested function indicates that we do not know if there exists a
trace in Pn(P -n) which extends the corresponding trace of length n in P -n
or if not.
In general we have a bijection between DPA and NFA since the prefix
closedness ensures that each P 2 DPA can be represented uniquely by the
sequence
1))-n for 0 - n. Further, any of those sequences corresponds uniquely to a
sequence where the equation P
corresponds to the requirement
represented by the sequence hfhig; fhig; of prefix closed sets and thus
by the sequence h
The
limit of the ! op -chain
A 3
A 4
Since there is only one mapping from A! (NFA
we have trivially A! (- 0 thus we obtain a further limit diagram for the
yy

A 3
A 4
The limit properties of both diagrams ensure the existence of a unique
mapping
(1)
and, moreover, it is ensured that this mapping is bijective, i.e., an isomorphism
in SET.
A i+2
The intended coalgebraic model of deterministic processes is now provided
by the A! -coalgebra
Remark 3.2 Note, that the category theoretic fixed point construction provides
a kind of "external" approximation of processes. That is, a process P
r
is identified with the sequence h ; of its finite approximations,
where the g i 's are not processes. Please bear in mind that an open branch
in g i is indicated by   and not by ;. This means, processes and their finite
approximations are kept apart.
There is no need for to force a cpo structure on the set of all processes to
be able to speak about finite approximations of infinite processes.
To convince the reader that the coalgebraic model and the Hoare-model
are isomorphic we have to analyse how the mapping uA
works. Let be given a sequence in NFA . The image of P
w.r.t. uA has to be a partial function uA thus we have firstly
to determine the domain of uA (P ). For this we have to bear in mind that all
partial functions g
have the same domain
because
with A i
(!) a total mapping for all i 2 N . That the domain of uA (P ) equals
this common domain of the components g i+1 of P is forced by equation 1,
which implies for all i 2 N
(2)
and thus dom(uA (P
Secondly, we have to define for any a 2 dom(uA (P )) a sequence uA (P
a
a
a
ensures g a
thus we obtain by the assumption P
(!)(g a
a
. That is, h ; g a
a
a
indeed an element of NFA and we
are done.
Since we have nextA (P for each prefix closed set
and each a 2 dom(nextA (P should become
evident, now, that the bijection between DPA and NFA outlined in remark
3.1 is compatible with nextA and uA as stated in
Theorem 3.3 The Hoare-model and the coalgebraic
model are isomorphic A! -coalgebras, i.e., there exists
a bijective mapping apprA : DPA ! NFA such that the following diagram
commutes
DPA
next A
appr A
The coalgebraic model final in the category of A! -
coalgebras by construction [9,11]. Since HMA is isomorphic to CMA we have
Corollary 3.4 are final A! -
coalgebras, i.e., final objects in the category DAA .
r
To justify the claim in section 2 that our new method of solving recursive
equations which is based on the finality of HMA or CMA , re-
spectively, is strongly related to the fixed point construction in [4], we have
to look more close to the proof of the finality of CMA .
be an arbitrary A! -coalgebra. What we
are interested in, is to determine the process that starts in a state s 2 S. That
is, we have to analyse step-by-step which states can be reached from s by which
transitions: The unfolding of the state transition function t
gives the following sequence of commutative diagrams
A!
A 3
A 3
where the left-most rectangle is commutative since there is only one mapping
from S into 1 and all other rectangles are stepwise images of the first one.
for any state s 2 S which states can be reached from
s in one step by which transition. A i
how
arbitrary sequences of transitions of length i, i.e., sequences not taking into
account the restrictions made by t, can be continued according to t in the next
step. Starting in a state s 2 S we obtain in such a way an infinite sequence
for all i 2 N , i.e., with t s
i represents all sequences of transitions in M of length atmost
starting in s. Moreover, t s
i tells which states are reached by sequences of
length exactly i. The states visited in between are forgotten in t s
For the following automaton M with alphabet
a
'&%$/!''# 2a
a
ff
a
xx
OO
and for the state 1 we could depict, e.g., the first four elements of unfoldM (1)
r
as follows
a
a
a
a b
a
@
@
@
@
@
@
@
a
~~
~ ~ ~ ~ ~ ~ ~ ~
Finally, we consider the abstraction of unfoldM (s) into a process. The
mapping all states to   thus A i
just forgets the information, which states are reached by sequences of length
i and keeps only the infomation that sequences of length i may be continued.
We obtain now for any s 2 S an infinite sequence
proc
The first four elements of proc M (1), e.g., are
a
\Upsilon\Upsilon
a
a
a
\Upsilon\Upsilon
a
@
@
@
@
@
@
@
a
~~

The commutativity of the above diagrams and the definition of t s
s
respectively, entail for all i 2 N
s
thus proc M (s) becomes indeed a process, i.e., an element of NFA . This means
that we have constructed by proc M (s) the process starting in state s 2 S.
Globally this provides a mapping proc M . That this mapping
constitutes a A!-homomorphism proc CMA and that this A! -
homomorphism is unique can be proved straightfowardly according to the
limit construction of NFA and the ! op -continuity of the functor A!
SET.
4 Interaction and concurrency
Firstly, Hoare describes the interaction of processes P and Q with the same
alphabet defines a process P k Q with ff(P k
which behaves like the system composed of P and Q interacting in lock-step
synchronization, i.e., any occurence of events requires simultaneous participation
of both the processes involved. To model this kind of interaction we have
to define a mapping k : NFA \Theta NFA ! NFA .
In the last section we have seen that is the final A! -
coalgebra, i.e., the final partial automaton with alphabet A. This offers a
canonical way to define mappings from an arbitrary set S into NFA [6]: We
have only to construct a A! -coalgebra
finality of CMA , there exists a unique A!-homomorphism proc
CMA . The substantial problem will be to design M in such a way that the
underlying mapping proc M becomes the intended one.
Following this coalgebraic heuristics it becomes immediately obvious that
we have to synchronize CMA with itself to obtain the appropriate A! -coalgebra:
Let
be the A! -coalgebra such that for any pair of processes
dom(synA
and such that for all a 2 dom(synA
The final A!-homomorphism proc SYN A : SYN A ! CMA due to section
3 makes the following diagram commutative
NFA \Theta NFA
syn A
proc SYN A
That is, for each pair (P; Q) 2 NFA \Theta NFA the equation
uA (proc SYN A
is required. For any event z 2 dom(synA (P; Q)) this means that
uA (proc SYN A
Using the notation in [4] the last condition turns into the equation (P k
thus it becomes apparent that the coalgebraic definition
of proc SYN A
is equivalent to the requirements stated in
law 4, page 67 in [4] for the interaction operator
Since proc SYN A
is uniquely defined by the above conditions we can be sure
that proc SYN A is indeed the intended interaction operator k .
Secondly, Hoare describes the concurrent interaction of processes P and
r
Q with different alphabets ffP 6= ffQ. Only events that are in both their alpha-
bets, i.e., in the intersection ffP " ffQ, are required to synchronize. However,
events in the alphabet of P but not in the alphabet of Q may occur independently
of Q whenever P engages in them. Similarly, Q may engage alone in
events which are in the alphabet of Q but not of P . In such a way the alphabet
of the process P k Q will be the union ffP [ ffQ of the alphabets of the
component processes. Note, that the use of overstrokes in [7] provides another
technique to fix which events in different sets of events have to synchronize.
Let be given now two alphabets A and B. The coalgebraic definition of the
intended mapping k : NFA \Theta NFB ! NFA[B can be extracted from law
7, page 71 in [4]. The synchronization of CMA and CMB provides a partial
automaton
with alphabet A[B as follows: For any pair of processes
we define
dom(syn A;B
and for any c 2 dom(syn A;B (P; Q)) we set
syn A;B
The final
provides the intended concurrent interaction operator
NFA[B . Note, that obviously SYN
The coalgebraic definition of the concurrent interaction operator suggests
a straightforward generalization of synchronization to arbitrary partial automata

Definition 4.1 For any partial automata M
and we define the corresponding synchronized
automaton
as follows: For each
and for any c 2 dom(synM 1
r
As an example we synchronize the vending machine VMC from section 2
with alphabet A = fcoin; choc; tofg and a customer CU with alphabet
fcoin; tof; bisg described by the recursive equation
paying a coin the customer decides between having a toffee
or a biscuit instead. The corresponding partial automata can be depicted by
coin '&%$/!''# 2
ee
choc
yy
tof
-OEAE-aeoe a
coin '&%$/!''# b
ee
bis
yy
tof
and the synchronization SYN VMC;CU of both automata is given by
a)
""
coin
(2; a)
choc
OO
bis
OO
bis
tof
choc
That is, after the customer was able to pay a coin he may decide for toffee
and the machine can deliver a toffee at the same time. If he decides for biscuit
the machine will serve up later on a chocolate. Or, even worth, the machine
may decide to give him a chocolate and he has to interpret this as his own
decision for biscuit to have a second chance to get a toffee.
Note, that by simply extending the alphabet of the customer to
fcoin; tof; bis; chocg we would obtain a synchronized automaton with a dead-
lock
a)
""
coin
(2; a)
OO
bis
OO
bis
tof
Now it turns out that the concurrent interaction of processes exactly describes
how the processes in a synchronized automaton SYNM 1 ;M 2 can be
reconstructed from the processes of the single automata M 1 and M 2 . That
is, synchronization of automata is compatible with interaction of processes as
stated in
Theorem 4.2 For any partial automata M
any pair of states
have that
given by the final (A[B)! -
homomorphism proc SYN A;B
suffices to show that the
r
mapping proc M 1
constitutes a
homomorphism proc M 1
NFA \Theta NFB
syn A;B
The required equality proc SYN M 1 ;M 2
is then
ensured by the uniqueness of final homomorphisms.
We have to show that for any pair (s the equality
\Theta proc M 2
holds. Since proc CMA is a A!-homomorphism we have for
and since proc CMB is a B!-homomorphism we have for s 2
According to the equations 4 and 5, the totality of the mappings proc M 1 ,
proc M 2 , and the definition of SYNM 1 ;M 2 and SYN A;B , respectively, we can
firstly show that the domain of both functions in equation 3 are equal:
dom(syn A;B (proc M 1
\Theta proc M 2
\Theta proc M 2 )
Secondly, we show the equality 3 for all c 2 dom(t 1
B. According to definition of syn A;B , the equality 4,
and the definition of synM 1 ;M 2 we obtain
\Theta proc M 2 )(c)
The other cases can be proved analogously. 2
According to theorem 4.2 we can extend in a compatible way our interpretation
rof process expressions as representations of finite automata to interac-
tion: For two process expressions exp 1 and exp 2 we define
where we can take due to theorem 4.2 as initial state of M exp 1
if
s i is the initial state of M exp i
2.
Remark 4.3 There is an essential problem to relate states in M exp 1
to
variables. The process expression (a seems to have a free
variable X. The idea, however, to take (s (a!X)k(b!X) as the state
corresponding to X does not work well especially with respect to recursion, i.e.,
with respect to the idea to substitute X successively by the whole expression
In general, we can not model substitutivity in a simple
way on the level of automata since X, (a
(b different automata.
For this paper we fix the problem by the following decision: Since interaction
is an essential parallel operator the symbol k builds a border between exp 1 and
impermeable for names. That is, we consider (a X) to be
equivalent to (a ! X)
Please note that Hoare
considers only examples where this problem does not arise, i.e., only examples
5 Nondeterminism in CSP
At first glance the nondeterministic processes in CSP have nothing to do with
the nondeterministic transition systems usually considered in the (coalgebraic)
literature [6]. That is, they are neither related to the power set construction
nor to the finite power set construction P f
If a nondeterministic system in the sense of CSP being in a certain state
can engage in an event then the state reached in the next step will be uniquely
determined by the event. Nondeterminism is restricted to the possibility to
decide locally in each state which events will be accepted or, alternatively,
refused for the next step. That is, even in case we can engage in an event it
may be that we can not carry out this event because it was decided before not
to accept this event for the next step.
At second glance, however, it is possible to relate this kind of systems
to real nondeterministic systems, namely, to image finite nondeterministic
automata [9].
The crucial observation is that the systems in CSP can be motivated along
two ideas: Firstly, by the old idea from Formal Language Theory to abstract
from nondeterminism by constructing out of a nondeterministic automaton N
with the set S of states a deterministic automaton P f N with the set P f (S) of
states. Secondly, by the idea to maintain in P f N the differences between the
original states in N as long as this difference can be expressed in the language
r
A of events.
We consider the following image finite nondeterministic automaton
a
a
a '&%$/!''# 6
Starting from state 1 we can reach by event a either the state 3 or the state
5. The difference between state 3 and state 5 which can be observed locally
in these states and which can be expressed in the language A is the difference
between bg. If we construct now the
corresponding power automaton P f N we can fix this difference by assigning
to the state f3; 5g in P f N the set ffb; cg; fa; bgg. In such a way we obtain out
of two different states 3 and 5 in N a single state f3; 5g in P f N but with two
different local states fb; cg and fa; bg. Following this idea the reachable part
of P f our example
would look as follows
ffagg fflffi flfi
a
a
R
R
R
R
R
R
R
R
R
R
R
R
R
R
R
R
R
R
c
l l l l l l l l l l l l l l l l l l
f;g
f;g fflffi flfi
Note, that the states 2 and 4 are not distinguishable by A since
Operationally considered we have to decide in state f3; 5g if we accept for
the next step either events from fa; bg or from fb; cg. If we decide for fa; bg
the event c can not occur in the next step, the event a, however, will bring
us to the singleton state f6g, and the event b will bring us to the compound
state f2; 4g since we can go in N by b from 3 to 2 and from 5 to 4. In
general we obtain by this variant of power construction systems with a kind
of nondeterministic local filters.
Remark 5.1 Hoare uses families of sets of refused events instead of families
of sets of accepted events to model this kind of nondeterminism. We
have decided for acceptance sets as in [3] because it eases argumentations in
operational terms. In contrast, Hoare argues mainly in observational terms.
Moreover, we will not introduce internal nondeterminism if we transform later
deterministic automata into filter automata. It can be checked, however, that
our descriptions of operations by means of acceptance sets, presented in the
next sections, are fully equivalent to the definitions of Hoare in [4].
To model the concept of nondeterministic processes used in CSP we have
to consider partial automata of the following structure
r
that will be called deterministic filter automata. For any state s 2 S we will
denote the first component of t(s) by acc(t(s)) and the second component,
in abuse of notation, also by t(s). This means that we are dealt with A f
coalgebras for the functor A f
[A !p S] for each set S and with A f
for each
mapping refers to the category of A f
-coalgebras and
A f
-homomorphisms.
The functor A f
! is also ! op -continuous [9] thus we can construct, analogously
to the case of deterministic automata, for each alphabet A a final
A f
The elements of FPA are again infinite sequences h ; where the
components g i are nested functions with an additional acceptance set, i.e.,
a subset of P(A), at each node. We will refer to the elements of FPA as
(deterministic) filter processes. CHAOSA 2 FPA , e.g., that is the most non-deterministic
process which at all times can engage in any event of A and at the
same time refuse any event of A, can be described uniquely by the conditions
CHAOSA for all a 2 A.
Remark 5.2 The set FPA includes all nondeterministic processes defined in
[4], but, also something more because we can not model coalgebraically the
saturation conditions in [4] (and [3]) for the acceptance (refusal) sets. We
guess that Hoare needs these conditions because he identifies divergence
with chaos and tries to treat divergence in a more algebraic manner (compare
section 7). This difference will be a point of further research.
Obviously, we can assign to any deterministic partial automaton
corresponding deterministic filter automaton
for all s 2 S. For a A!-homomorphisms the underlying mapping
provides also a A f
we have dom(A!
to the totality of f This means, we have an embedding functor
for each alphabet A. Note, that the corresponding embedding
according to [4] would take instead of the singleton family of acceptance
sets fdom(t(s))g the family of refusal sets. That is the resulting
filter automaton would own a proper internal nondeterminism which,
however, can never be observed from outside. Note, further that obviously
Besides the problem of "branching nondeterminism" discussed up to now
Hoare tries to treat within his framework also the problem of "internal non-
determinism", i.e., the problem that a system may carry out internal actions
r
which can not be observed from outside. To treat this problem he uses the
concept of acceptance (refusal) sets. We consider the following simple deterministic
filter automaton F
a
a
// f;g
f;g ffbgg ffag; fa; -gg ffa; bg; fbgg '&%$/!''# 6
// f;g
where - is assumed to be an internal action. Hoare insists on the intuition
that "we want these actions to occur automatically and instantaneously as
soon as they can" ([4], p. 111). That is, if we decide internally in state 1 to
accept fa; -g action - will occur instantaneously and we have to go on from
state 3 with a new decision for acceptance. Only in case we decide for fag,
we are allowed to stay at state 1 and to take the chance to reach state 2 via
action a.
Because the decision for fa; -g in 1 is equivalent to being in 3 and making
any decision there we can eliminate action - by identifying states 1 and 3 and
by taking the decions in 3 instead of the decision fa; -g in 1. In such a way we
can describe the observable behavior of F by the following nondeterministic
filter automaton
a
a
f;g
f;g ffbgg ffag; fa; bg; fbgg '&%$/!''# 6
// f;g
As long as there is no divergence in F , i.e. no infinite loop of internal actions,
the elimination of internal actions outlined above is fully compatible with
Hoare's treatment. In case of divergence, however, Hoare firstly identifies
all divergent states with CHAOSA and proceeds with the above elimination
(see section 7).
6 Nondeterministic operators
The realization of our program to interpret the operations in [4] as constructions
on the level of automata and thus to interpret every finite process expression
as representing a finite automata with an initial state such that the
process starting in this state equals the process represented by the same expression
according to [4], becomes a little bit complicated if we take into
account nondeterministic operators.
We can assign deterministic filter processes only to states of deterministic
filter automata. The constructions general choice [], interleaving jjj, and elimination
of internal actions, however, will introduce branching nondeterminism
thus we are obliged, firstly, to take into consideration nondeterministic filter
automata and to define our constructions for this kind of automata. Secondly,
r
we have to describe a transformation of nondeterministic filter automata into
deterministic filter automata to get the deterministic filter processes Hoare
is interested in. Note, that the identification of actions (not considered in [4])
would also introduce branching nondeterminism and could be treated naturally
within our approach.
On the other side, internal actions arise by concealment of actions and
also by the constructions nondeterministic or u and recursion -. To assign
observable deterministic processes to automata with internal actions we have
two possibilities. Firstly, we can eliminate internal actions on the level of
automata and than transform the resulting nondeterministic automata into
a deterministic one. In case of divergence we will not get, in this way, the
deterministic filter processes intended by Hoare. Secondly, we can carry out
the transformation into a deterministic automata first and than we have to
use a mixed coalgebraic and algebraic procedure, according to Hoare, to
eliminate internal actions in deterministic filter processes.
In the sequel we present our semantical interpretations of the nondeterministic
operators in [4] on the level of filter automata. There will be no space
to prove formally the correctness of our interpretations as we have done it for
interaction in theorem 4.2. We hope, however, the reader will be convinced
by the definitions, the informal argumentations, and the examples.
6.1 Nondeterministic filter automata
(Image finite) nondeterministic filter automata are automata of the structure
-coalgebras for the functor
for each set S and with Anf !
for each mapping f
given by P f The category
of Anf ! -coalgebras and Anf ! -homomorphisms will be denoted by NFAA .
Obviously, the embedding in
S allows to assign to any deterministic filter automaton
\Theta [A !p S]) a nondeterministic filter automaton
with t n Note, that this definition works smoothly
since we keep in F n the situations a =
This assignment is compatible with A f
-homomorphisms thus we obtain an
embedding for each alphabet A.
On the other side we can define on basis of the finite power set functor
nondeterministic filter automaton
deterministic filter automatn
r
as follows: For each M 2 P f (S) we define
dom(t
and for each a 2 dom(t p (M)) ' A we set
It can be easily checked that this construction is compatible with Anf ! -homo-
morphisms, i.e., that the finite power set functor
to a functor for each alphabet A. For examples of the
finite power set construction we refer to the next subsections.
6.2 General choice, interleaving, and interaction
The general choice operator [] corresponds on the semantical level to the glueing
of states in automata. Thereby any decision for acceptance in the glued
state is given by glueing decisions of the single states.
Definition 6.1 Let be given a nondeterministic filter automaton
and different states s 1 6= s 2 in S. Then the glueing of states s 1 and s 2 provides
an automaton
as follows: We set S for each
and for each a 2 dom(t
Note, that the case a 2 dom(t(s 1 ))"dom(t(s 2 branching
nondeterminisms and that the construction extends straightforwardly to any
equivalence on states.
On basis of this construction we can extend, now, the translation of process
expressions into automata with an initial state to the []-operator: We
consider two process expressions exp 1 and exp 2 with fX the set of
expressions have in common. Let s i
with
be the state in F exp i
corresponding to the variable X j . Please
bear in mind that a state which correspond to a free variable has always the
domain ; and the acceptance f;g. Then we introduce for the sequence of
r
glueings s 1
the abbreviation
denotes the disjoint union of automata. The expression exp 1 []exp 2
can be interpreted now by the finite nondeterministic filter automaton
with initial state (s 1 is the initial state of F exp i
2.
As example we consider the expressions exp
i.e., the following deterministic automata
and F exp 2
a
c
c
ffa; cgg ffbgg f;g ffb; cgg f;g
Then the nondeterministic automaton F exp 1 []exp 2
initial state (1; 4) and with (3; 5) the state corresponding to the free variable
X in expression exp 1 []exp 2 looks as follows
c
c
a
f;g
As outlined in the introduction of this section we have, firstly, to go to the
power automaton P f
with initial state f(s 1 secondly, to
apply the final A f
to in order to obtain the deterministic filter process represented by
the expression exp 1 []exp 2 according to [4]. For our example we obtain the
following (reachable part of) automaton P f
a b
c
ffbgg fflffi flfi
// f;g
As known from Formal Language Theory any trace t 2 A   of actions in
is also a trace of actions in P f
vive versa. The more
interesting point is that both automata are also equivalent with respect to
acceptance traces. That is, F exp 1 []exp 2
can carry out the sequence r 2
of acceptance decisions and actions if, and only if, P f
can. We draw attention to the point that the trace hci from (1; 4) to (3; 5)
can not be continued in F exp 1 []exp 2
since (3; 5) is a final state. To model this
breaking condition for traces we have to consider in P f
acceptance
r
traces thus we can decide in state f2; (3; 5)g for acceptance ; to break the
run. In general, an acceptance trace in a filter
automaton F can not be continued in state s if dom(t(s)) " acc
The intuition behind the interleaving operator jjj is to combine two systems
without any synchronization such that if both systems could engage in the
same action, the choice between them is nondeterministic.
Definition 6.2 For any nondeterministic filter automata F
we define the corresponding interleaved automaton
as follows: For each
and for each a 2 dom(int(s
We adapt example X1, p. 121 in [4] and consider the following (determin-
istic) filter automata F 1 and F 2 with initial states 1
a
a
ffbgg
The interleaving of F 1 and F 2 provides INT F 1 ;F 2 with initial state (1; 1)
a
a
a
a
OO
OO
ffbgg
and the power construction delivers the following part of P f (INT F 1 ;F 2
a
a
ffagg f;; fag; fbg; fa; bgg ffbgg
For process expressions exp 1 and exp 2 we can define now
r
with initial state (s 1 is the initial state of F exp i
2. The
discussion in remark 4.3 concerning free variables applies also to interleaving,
i.e., we decide that there are no free variables in exp 1 jjjexp 2 .
The interaction operator k does not introduce, in contrast to general choice
and interleaving, new branching nondeterminism. Definition 4.1 provides
in such a way for any deterministic filter automata F
corresponding synchronized filter automaton
if we define additionally for each
The definition of synchronization for nondeterministic filter automata is
straightforward.
6.3 Recursion and nondeterministic or
Concealment of actions forces us to give a full treatment of internal actions
anyway thus it will be not so problematic to model recursion - and nondeterministic
or u by the introduction of special internal actions.
Hoare insists on the intuition that the process expression -X:A:X represents
an infinite loop of internal actions, i.e., divergence. To cover this intuition
we have to model the -operator by the introduction of a new internal action
in an automaton and not by glueing of states, as we have done it in section 2
in the context of deterministic partial automata.
be the finite nondeterministic filter automaton according
to F (X) with alphabet A, with the initial state s 0 2 S, and with s X 2 S
the state that corresponds to the free variable X, i.e., for this state we have
especially dom(t(sX f;g. Than we obtain
with initial state s 0 by adding a new internal action to the alphabet and by
introducing a new internal action from s X to s
and t 0
g.
Since the only state in FX at the same time corresponds to X and is initial
in FX we obtain for F-X:A:X the following one-state automaton
back ffbackgg
Remark 6.3 To be correct we have to distinguish for an automaton F between
the alphabet A and the "interface", i.e., the set A obs ' A of its observable
ractions. In this sense it may be that back is already an internal (hidden)
action of F F (X) , i.e., we will have back 2 A int = A n A obs if there is already
an application of recursion - in F (X). Moreover we should observe that A in
stands for the set of observable actions.
The intuition behind the nondeterministic or u is to provide to the outside
of a system a nondeterministic alternative between two possible behaviors.
We can model this intuition by introducing an additional decision point with
two possible internal local decisions.
Definition 6.4 Let be given a nondeterministic filter automaton
and states s S. Then the introduction of an alternative between s 1 and
provides an automaton
us
as follows: We set S rightg and
For process expressions exp 1 and exp 2 we can define analogously to the
general choice operator the nondeterministic filter automaton
us 2
with initial state s 1 u s 2 if s i is the initial state of F exp i
2.
As example for nondeterministic or and recursion we consider the expression
X) from subsection 6.2. According to our definitions
we obtain for F-X:exp 1 uexp 2
c
a
right
yy
c
OO
back
ffbackgg ffleftg; frightgg
with initial state 1 u 4 and with the internal actions left, right, and back.
6.4 Elimination of internal actions
We describe now formally the stepwise elimination of internal actions in automata
as outlined in the introduction of this section.
For this we consider a finite nondeterministic filter automaton
with a fixed set A obs ' A of observable actions For any state s 2 S with
we can construct a new finite nondeterministic
filter automaton
r
by eliminating the internal actions starting in s as follows: We denote by
the set of all states in F
reachable from s by an internal action. We set S
and for each a 2 dom(t 0 (s 0 )) we set
Note, that in case dom(t(s)) n A just delete
in acc(t(s)) all acceptances that include internal actions.
If we apply stepwise the elimination of internal actions to a finite nondeterministic
filter automaton F with the set A obs ' A of observable actions
we will get finally due to the finitarity of F a finite nondeterministic filter
automaton
all thus we can consider F 0 to be an automaton with alphabet A obs .
For the example
in subsection 6.3 we will get after two steps
(in any order) the automaton F 0
c
a

c
ff
ffbgg
where m is the initial state and arises by merging the states 1, 4, 1 u 4, and
(3; 5) in F-X:exp 1 uexp 2
. Further, the power construction provides the following
part of P f
with initial state fmg
c
a

xx
a
c
ffbgg fflffi flfi
OO
Even for finite automata with divergence, i.e., with loops of internal ac-
tions, our procedure provides a reasonable result. The crucial point is that we
abstract from divergence by merging all states of a loop into one state and by
collecting all fully observable acceptances in the loop. In such a way we would
obtain for F-X:A:X (in two steps) the automaton
fg
i.e., an automaton representing the process STOPA . This is indeed not the
r
intuition of Hoare who wishes to interpret -X:A:X as representing chaotic
behavior.
7 Concealment
In the last section we describe, within our framework, Hoare's treatment of
internal actions and thus of divergence.
The problem is to assign to the states of a nondeterministic filter automaton
F with alphabet A and with the set A obs ' A of observable actions
deterministic filter processes with alphabet A obs . Firstly, we can use the power
construction to transform the nondeterministic filter automaton
F into a deterministic filter automaton P f (F) where the singleton
states in P f (F) correspond to the states in F . Secondly, we can assign to each
state in P f (F) a deterministic filter process with alphabet A using the (unique)
final A f
into the final
A f
-coalgebra FMA since the set FPA of deterministic filter processes on
A is the carrier of FMA . Finally, we need a mapping hide
to transform deterministic filter processes on A to deterministic filter processes
on A obs , i.e., processes with observable actions only. The definition of
will be the subject of this section.
Before going to technical details we draw attention to the following crucial
observations:
(i) Since the state transition function vA
the final A f
-coalgebra FMA is bijective we have as well a A f
A ) both with the
same carrier FPA [6,12].
(ii) The definition of hide : FPA ! FPA obs and thus the concept of "nonde-
terministic processes" in [4] is based on a complex mixture of coalgebraic
and algebraic techniques (see remark 5.2). This difference between the
fully coalgebraic concept of "deterministic processes" in [4] and the mixed
coalgebraic and algebraic concept of "nondeterministic processes" shows
itself also in the difference between the fixed point constructions in [4].
For "deterministic processes" the construction starts with the completely
undefined process STOPA and proceeds by extending definedness. In
contrast, the construction for "nondeterministic processes" starts with
the completely defined (and accepted) process CHAOSA and proceeds
by reducing definedness (and acceptance).
(iii) The mapping hide
will provide neither in the coalgebraic
nor in the algebraic sense any kind of homomorphism.
We are going now to define hide
. We start by considering
two A f
-subcoalgebras of FMA : Obviously, the set FPA obs of observable
processes constitutes a A f
-subcoalgebra of FMA . That is, FMA obs
r
can be seen as a A f
-subcoalgebra of FMA . Moreover, we can characterize
FMA obs by the equation FMA
acc(v A (p)) ' That is, FMA obs
is the greatest
A f
-subcoalgebra of FMA contained in the set LocA obs of locally observable
processes (see [9]).
In the same way we obtain the set DIVA obs
' FPA of all divergent pro-
cesses, i.e., processes with infinite traces of internal actions, as carrier of the
A f
is the greatest A f
-subcoalgebra of FMA
contained in the set LocA int
of processes with local internal actions.
If we turn, next, to the algebraic viewpoint we can observe that the A f
A ) is generated by the set FPA obs
[DIVA obs
, i.e., we
i. This means that FM \Gamma1
A is the smallest
A f
-algebra of FM \Gamma1
A containing FPA obs
[DIVA obs
. In such a way we can use
the common algebraic induction with the two basic cases FPA obs
and DIVA obs
to define things on FPA .
For the definition of hide
we need, further, an auxiliary
mapping that merges a finite set of observable
filter processes into a single observable filter process. Using the embedding
and the power construction
we obtain for the final
a further
thus the final
! -homomorphism from P f (N(FMA obs
to FMA obs
provides the intended mapping merge
Let be given, now, a set A of actions with a designated set A obs ' A of
observable actions. To define the mapping
we consider first the two basic cases. For observable processes we take obviously
the identity
and divergent processes have to be identified (according to Hoare) with
chaotic behavior
The induction step is based on the A f
That is, we can consider any process p 2 FPA n (FPA obs
) as the
result of applying the operation v \Gamma1
A to the argument (acc(v A (p)); vA (p)), and
the induction assumption will be that hide(v A (p)(a)) 2 FPA obs
is already
defined for all a 2 dom(vA (p)).
To define on this assumption hide(p) 2 FPA obs it will be enough to assign
to (acc(v A (p)); vA (p)) 2 P(P(A)) \Theta [A !p FPA ] a pair
r
since we can use the
A obs
A obs
to define
A obs
Note,that we will have according to this definition and the bijectivity of vA obs
Analogously to the elimination of internal actions described in section 6.4
we define (acc
as follows: We
denote by the set of all
processes in FPA reachable from p by an internal action, and we set
Note, that we get indeed acc p ' according to
the equations acc
(hide(q)), and the induction
assumption. For each a 2 dom(g p ) we set
in case a 2 (dom(vA
in case a 2 dom(vA
in case a 2 S
As example we consider the deterministic filter automaton F-X:exp 1 uexp 2
from section 6.3 with alphabet A = fa; b; c; lef t; right; backg and the set
of observable actions. The second and third component of
the process proc F -X:exp 1 uexp 2
(1 starting in state
can be depicted by
right
OEOE
right
a
\Upsilon\Upsilon
c
c
\Upsilon\Upsilon

and the second and third component of the corresponding observable process
r
are
a
c
a
OEOE
c
ffbgg fi
a
\Upsilon\Upsilon
c
ii
a
\Upsilon\Upsilon
c

Since there is no divergence in F-X:exp 1 uexp 2
this process coincides with the
process starting in the state fmg of the automaton P f
in section
6.4 that arises from F-X:exp 1 uexp 2
by, firstly, eliminating internal actions and
by, secondly, abstracting from nondeterminism using the power construction.
8 Conclusion and further work
We have shown that the concepts of processes in [4] are strongly related,
on the semantical level, to the concepts of deterministic partial automata,
deterministic filter automata, and nondeterministic filter automata. We were
able to give a compatible semantical interpretation of most of the operations
in [4] on the level of automata.
The algebraic laws in [4] turn now to statements concerning the compatibility
of constructions on different levels and in a next step we have to prove
these laws as we have done it for the statement in theorem 4.2 concerning the
compatibility of synchronization of automata and interaction of processes.
Based on the results and categorical concepts of this paper we should be
able to develop a more general theory of combining and structuring automata.
This would include, e.g., the straightforward interpretation of changes of symbols
by means of functors between categories of automata (analogously to
[13]). It would be also very interesting and necessary to relate the constructions
and results of this paper to similar constructions and results in the area
of behavioral [8] and hidden [2] algebraic specifications.
It will be also convenient to consider weaker concepts of homomorphisms
based on the obvious partial ordering on the sets [A !p S], [A !p P f (S)],
and P(P(A)), respectively. This would allow, e.g., to consider the synchronized
automaton SYNM 1 ;M 2 as a (relative) subautomaton of the product
automaton . Moreover, we will be able in such a way to extend
our considerations in [14] concerning traces and runs in deterministic partial
automata to filter automata.
Finally, it seems to be worth to extend the analysis of section 7 to other
process calculi. That is, to find out to what extend coalgebraic and algebraic
techniques are mixed there and how far they may be separated and combined
in a more structured way.
r



--R

Universal Theory of Automata.
A Hidden Agenda.
Algebraic Theory of Processes.
Communicating Sequential Processes.
Unification of Theories: A Challenge for Computing Science.
A tutorial on (co)algebras and (co)induction.
Communication and Concurrency.
Initial Computability
Universal coalgebra: a theory of systems.
Automata and coinduction (an exersice in coalgebra).
The category theoretic solution of recursive domain equations.
Functorial operational semantics and its denotational dual.
Models for concurrency.
A coalgebraic introduction to CSP.
--TR
Communicating sequential processes
Initial computability, algebraic specifications, and partial algebras
Algebraic theory of processes
Communication and concurrency
Models for concurrency
Unification of Theories
Automata and Coinduction (An Exercise in Coalgebra)
Universal coalgebra: a theory of systems

--CTR
Michele Boreale , Fabio Gadducci, Processes as formal power series: a coinductive approach to denotational semantics, Theoretical Computer Science, v.360 n.1, p.440-458, 21 August 2006
communicating sequential processes;partial automata;coalgebras;final automata