An Efficient Algorithm for Aggregating PEPA Models.
AbstractPerformance Evaluation Process Algebra (PEPA) is a formal language for performance modeling based on process algebra. It has previously been shown that, by using the process algebra apparatus, compact performance models can be derived which retain the essential behavioral characteristics of the modeled system. However, no efficient algorithm for this derivation was given. In this paper, we present an efficient algorithm which recognizes and takes advantage of symmetries within the model and avoids unnecessary computation. The algorithm is illustrated by a multiprocessor example.
Introduction
In recent years several Markovian process algebras (MPAs) have been presented
in the literature. These include PEPA [1], MTIPP [2], and EMPA [3].
As with classical process algebras, these formalisms allow models of systems
to be constructed which are amenable to functional or behavioural analysis
by a variety of techniques. Additionally they allow timing information to
be captured in those models and so facilitate performance analysis via the
solution of a Continuous Time Markov Chain (CTMC).
Process algebras have several attractive features: a facility for high-level
definition, compositional structure and the existence of formally defined
equivalence relations which can be used to compare models. In the Markovian
context theoretical results have shown that it is possible to exploit
these equivalence relations at the level of the model description to generate
an aggregated CTMC in a compositional way [4]. This is of great practical
importance because, like all state-based modelling techniques, MPA models
suffer from the state space explosion problem. Although prototype tools
have been developed for model exploration [5, 6, 7], little work has been done
to exploit to the full the potential to use equivalence relations to achieve effective
aggregation and thus to put the theoretic results to practical use. In
this paper we describe an algorithm to carry out efficient aggregation and
its implementation in the PEPA Workbench.
Aggregation is a widely used and well-understood technique for reducing
the size of CTMC used in performance analysis. The state space of
the CTMC is partitioned into a number of classes, each of which is treated
as a single state in a new derived stochastic process. If the partition can
be shown to have a condition known as lumpability [8], this new stochastic
process will again be a CTMC and amenable to numerical solution of a
steady state probability distribution via linear algebra. In the MPA context
the partitioning is carried out using a formally defined equivalence relation
which establishes behavioural or observational equivalence between states
within a model. The equivalence relation which is generally discussed in
relation to aggregation is called strong equivalence (for PEPA), Markovian
bisimulation (for MTIPP) or extended Markovian bisimulation equivalence
(for EMPA). However there are some problems with applying this equivalence
relation/aggregation at the syntax level in a compositional way. These
are discussed in more detail in Section 5. In this paper we use a finer equivalence
relation, called isomorphism, which although it may result in coarser
aggregations has the advantage of being readily amenable to automatic generation
of equivalence classes at the syntax level. Thus the construction
of the complete state space can be avoided and the aggregated CTMC is
constructed directly.
The rest of the paper is structured as follows. In Section 2 we introduce
the PEPA language, its operational semantics, and aggregation via
isomorphism. The algorithm for the computation of a reduced state space
is discussed in Section 3, an example is presented in Section 4. Some cases
in which the algorithm cannot achieve the optimal theoretical partitioning
are discussed in Section 5. Section 6 presents some related approaches and,
finally, Section 7 concludes the paper presenting some possible future investigation

Performance Evaluation Process Algebra (PEPA) is an algebraic description
technique based on a classical process algebra and enhanced with stochastic
timing information. This extension results in models which may be used
to calculate performance measures as well as deduce functional properties
of the system. In this section we briefly introduce PEPA; more detailed
information can be found in [1].
Process algebras are mathematical theories which model concurrent systems
by their algebra and provide apparatus for reasoning about the structure
and behaviour of the model. In classical process algebras, e.g. Calculus
of Communicating Systems (CCS [9]), time is abstracted away-actions are
assumed to be instantaneous and only relative ordering is represented-
and choices are generally nondeterministic. If an exponentially distributed
random variable is used to specify the duration of each action the process
algebra may be used to represent a Markov process. This approach is taken
in PEPA and several of the other Markovian process algebras [2, 3].
The basic elements of PEPA are components and activities, corresponding
to states and transitions in the underlying CTMC. Each activity is
represented by two pieces of information: the label, or action type, which
identifies it, and the activity rate which is the parameter of the negative
exponential distribution determining its duration. Thus each action is represented
as a pair (ff; r). We assume that the set of possible action types, A,
includes a distinguished type, - . This type denotes internal, or "unknown"
activities and provides an important abstraction mechanism.
The process algebra notation for representing systems is wholly based
on the use of a formal language. The PEPA language provides a small set
of combinators. These allow language terms to be constructed defining the
behaviour of components, via the activities they undertake and the interactions
between them. The syntax may be formally introduced by means of
the following grammar:
where S denotes a sequential component and P denotes a model component
which executes in parallel. C stands for a constant which denotes either
a sequential or a model component, as defined by a defining equation. C S
stands for constants which denote sequential components. The component
combinators, together with their names and interpretations, are presented
informally below.
r):S The basic mechanism for describing the behaviour of
a system is to give a component a designated first action using the prefix
combinator, ". For example, the component (ff; r):S carries out activity
(ff; r), which has action type ff and an exponentially distributed duration
with parameter r, and it subsequently behaves as S. The set of all action
types is denoted by A. Sequences of actions can be combined to build up a
life cycle for a component. For example:
Comp
S The life cycle of a sequential component may be more
complex than any behaviour which can be expressed using the prefix combinator
alone. The choice combinator captures the possibility of competition
or selection between different possible activities. The component
represents a system which may behave either as S 1 or as S 2 . The activities of
both S 1 and S 2 are enabled. The first activity to complete distinguishes one
of them: the other is discarded. The system will then behave as the derivative
resulting from the evolution of the chosen component. For example,
the faulty component considered above may also be capable of completing
a task satisfactorily:
Comp
Constant, C As we have already seen, it is convenient to be able to assign
names to patterns of behaviour associated with components. Constants
provide a mechanism for doing this. They are components whose meaning
is given by a defining equation: e.g. C def
which gives the constant C the
behaviour of the component P .
Cooperation,
Most systems are comprised of several components
which interact. In PEPA direct interaction, or cooperation, between
components is represented by the combinator "  \Delta
". The set L, of visible
action types (L ' A n f-g), is significant because it determines those
activities on which the components are forced to synchronise. Thus the co-operation
combinator is in fact an indexed family of combinators, one for
each possible cooperation set L. When cooperation is not imposed, namely
for action types not in L, the components proceed independently and concurrently
with their enabled activities. However if a component enables an
activity whose action type is in the cooperation set it will not be able to
proceed with that activity until the other component also enables an activity
of that type. The two components then proceed together to complete the
shared activity. The rate of the shared activity may be altered to reflect the
work carried out by both components to complete the activity.
For example, the faulty component considered above may need to co-operate
with a resource in order to complete its task. This cooperation is
represented as follows:
System
ftaskg
Res
If the component also needs to cooperate with a repairman in order to be
repaired this could be written as:
System  \Delta
Repman
or, equivalently
ftaskg
Repman
In some cases, when an activity is known to be carried out in cooperation
with another component, a component may be passive with respect to that
activity, denoted (ff; ?). This means that the rate of the activity is left
unspecified and is determined upon cooperation, by the rate of the activity
in the other component. All passive actions must be synchronised in the
final model.
If the cooperation set is empty, the two components proceed indepen-
dently, with no shared activities. We use the compact notation, P k Q,
to represent this case. Thus, if two components compete for access to the
resource and the repairman we would represent the system as
ftaskg
Repman
Hiding, P=L The possibility to abstract away some aspects of a compo-
nent's behaviour is provided by the hiding operator ``/''. Here, the set L
of visible action types identifies those activities which are to be considered
internal or private to the component. These activities are not visible to an
external observer, nor are they accessible to other components for coopera-
tion. For example, in the system introduced above we may wish to ensure
that these components have exclusive access to the resource in order to complete
their task. Thus we hide the action type task, ensuring that even when
the system is embedded in an environment no other component can access
the task activity of the resource:
System
ftaskg
Res)=ftaskg
Once an activity is hidden it only appears as the unknown type - ; the rate
of the activity, however, remains unaffected.
The precedence of the combinators provides a default interpretation of
any expression. Hiding has highest precedence with prefix next, followed by
cooperation. Choice has the lowest precedence. Brackets may be used to
force an alternative parsing or simply to clarify meaning.
2.1 Operational semantics and the underlying CTMC
The model components capture the structure of the system in terms of its
static components. The dynamic behaviour of the system is represented
by the evolution of these components, either individually or in cooperation.
The form of this evolution is governed by a set of formal rules which give an
operational semantics of PEPA terms. The semantic rules, in the structured
operational style of Plotkin, are shown in Figure 1; the interested reader is
referred to [1] for full details.
The rules are read as follows: if the transition(s) above the inference
line can be inferred, then we can infer the transition below the line. For one
example, the two rules for choice show that the choice operator is symmetric
and preserves the potential behaviours of its two operands. For another, the
cooperation operator has a special case where the two cooperands do not
synchronise on any activities. The notation for this case is E k F . In this
case the three rules would simplify to the two which are shown below.
F
These rules capture the intuitive understanding that two components which
do not synchronise on any activities cannot influence each other's computational
state. In the case of components which do synchronise the rate of the
resulting activity will reflect the capacity of each component to carry out
activities of that type. For a component E and action type ff, this is termed
the apparent rate of ff in E, denoted r ff (E). It is the sum of the rates of the
activities enabled in E. The exact mechanism used to determine the
rate of the shared activity will be explained shortly.
As in classical process algebra, the semantics of each term in PEPA is
given via a labelled transition system; in this case a labelled multi-transition
system-the multiplicities of arcs are significant. In the transition system
a state corresponds to each syntactic term of the language, or derivative,
Choice
F
Cooperation
F
F
F
F
r ff (E)
r ff
Hiding
Constant
E)

Figure

1: Operational semantics of PEPA
initial state

Figure

2: DG for the Multi-Component model (without hiding)
State Corresponding derivative
ftaskg
Repman
ftaskg
Repman
ftaskg
Repman
ftaskg
Repman
ftaskg
Repman
ftaskg
Repman
ftaskg
Repman
ftaskg
Repman

Table

1: States of the derivation graph of Figure 2
and an arc represents the activity which causes one derivative to evolve into
another. The complete set of reachable states is termed the derivative set of
a model and these form the nodes of the derivation graph (DG) formed by
applying the semantic rules exhaustively. For example, the derivation graph
for the system
ftaskg
Repman
is shown in Figure 2, assuming the following definitions:
Comp
Res
Repman
For simplicity, in the figure we have chosen to name the derivatives with
short names s the corresponding complete names are listed in

Table

1. Note that there is a pair of arcs in the derivation graph between
the initial state s 0 and its one-step derivative s 1 . These capture the fact
that there are two distinct derivations of the activity (task ; -) according to
whether the first or second component completes the task in cooperation
with the resource, even though the resulting derivative is the same in either
case.
The timing aspects of components' behaviour are not represented in the
states of the DG, but on each arc as the parameter of the negative exponential
distribution governing the duration of the corresponding activity. The
interpretation is as follows: when enabled an activity a = (ff; r) will delay
for a period sampled from the negative exponential distribution with parameter
r. If several activities are enabled concurrently, either in competition or
independently, we assume that a race condition exists between them. Thus
the activity whose delay before completion is the least will be the one to suc-
ceed. The evolution of the model will determine whether the other activities
have been aborted or simply interrupted by the state change. In either case
the memoryless property of the negative exponential distribution eliminates
the need to record the previous execution time.
When two components carry out an activity in cooperation the rate of the
shared activity will reflect the working capacity of the slower component. We
assume that each component has a fixed capacity for performing an activity
type ff, which cannot be enhanced by working in cooperation (it still must
carry out its own work), unless the component is passive with respect to
that activity type. This capacity is the apparent rate. The apparent rate
ae ae
ae
ae
r
r
ae
ae
r
r
ae ffl
ae

Figure

3: CTMC underlying the Multi-Component model
of ff in a cooperation P  \Delta
fffg
Q will be the minimum of r ff (P ) and r ff (Q).
The rate of any particular shared activity will be the apparent rate of the
shared activity weighted by the conditional probability of the contributing
activities in the cooperating components. The interested reader is referred
to [1] for more details.
The DG is the basis of the underlying CTMC which is used to derive
performance measures from a PEPA model. The graph is systematically
reduced to a form where it can be treated as the state transition diagram of
the underlying CTMC. Each derivative is then a state in the CTMC. The
transition rate between two derivatives P and P 0 in the DG is the rate at
which the system changes from behaving as component P to behaving as P 0 .
It is denoted by q(P; P 0 ) and is the sum of the activity rates labelling arcs
connecting node P to node P 0 . For example, the state transition diagram
for the CTMC underlying the simple component model is shown in Figure 3.
Note the arc labelled with rate 2- between states X 0 and X 1 , representing
the derivatives ((Comp k Comp)  \Delta
ftaskg
Repman and ((Comp k
Comp)  \Delta
ftaskg
Repman respectively.
In order for the CTMC to be ergodic its DG must be strongly connected.
Some necessary conditions for ergodicity, at the syntactic level of a PEPA
model, have been defined [1]. These syntactic conditions are imposed by the
introduced earlier.
2.2 Aggregation in PEPA via isomorphism
Equivalence relations, and notions of equivalence generally, play an important
role in process algebras, and defining useful equivalence relations is an
essential part of language development. For PEPA various equivalence relations
have been defined. These include isomorphism, which captures the
intuitive notion of equivalence between language terms based on isomorphic
derivation graphs, and strong equivalence, a more sophisticated notion of
equivalence based on bisimulation.
equivalence relation defined over the state space of a model will induce
a partition on the state space. Aggregation is achieved by constructing
such a partition and forming the corresponding aggregated process. In the
aggregated process each partition of states in the original process forms one
state. If the original state space is fX then the aggregated
state space is some fX [0] ; X In
general, when a CTMC is aggregated the resulting stochastic process will
not have the Markov property. However if the partition can be shown to
satisfy the so-called lumpability condition, the property is preserved and the
aggregation is said to be exact.
When the model considered is derived from a process algebra such as
PEPA it is possible to establish useful algebraic properties of the equivalence
relation used. The most important of these is congruence. An equivalence
relation is a congruence with respect to the operators of the language if
substituting an equivalent component within a model expression gives rise
to an equivalent model; e.g. if P is equivalent to P 0 , then P  \Delta
Q is equivalent
to
Q. When a congruence is used as the basis for aggregation in
a compositional model, the aggregation may be carried out component by
component, avoiding the construction of the complete state space because
the aggregated component will be equivalent to the original. Nevertheless
this approach is applied at the semantic level of the model and necessitates
the expansion and subsequent partitioning of relevant state spaces. More-
over, the reduced model produced in this way may not be as compact as
would be achieved by aggregating the complete model directly, making a
further application of the aggregation procedure necessary, in this case to
the model consisting of the aggregated components.
Both isomorphism and strong equivalence are congruence relations that
can be used as the basis for exact aggregation of PEPA models, based on
lumpability [4]. In either case the relation is used to partition the state
space (possibly compositionally), and so the underlying CTMC, and each
such equivalence class forms one state in the aggregated state space. In the
algorithm which we are presenting here we use the isomorphism relation:
the use of strong equivalence for the same purpose is discussed in Section 5.
The use of the isomorphism relation may seem surprising since the more
powerful bisimulation-style equivalence relations are one of the attractive
features of process algebras and are often cited as one of the benefits of
these formal languages. In contrast, isomorphism has received little attention
in the literature. In part, this is because in classical process algebra
the objective is to use an equivalence relation to determine when two agents
or system descriptions exhibit the same behaviour. In stochastic process
algebra greater emphasis is placed on using equivalence relations to partition
the derivation graph of the model in order to produce an aggregation
resulting in a smaller underlying Markov process. It has been shown that
PEPA's strong equivalence relation is a powerful tool for aggregation in this
style, always resulting in a lumpably equivalent Markov process [1]. How-
ever, we believe that in many instances isomorphism can also be useful for
this purpose. Since it is a more discriminating notion of equivalence it may
give a finer partition and thus less aggregation than strong equivalence. On
the other hand, as we will show, it may be detected at the syntactic level
of the system description without the recourse to the semantic level which
is necessary to detect strong equivalence in general. Thus a reduced derivation
graph is generated without the need to construct the original derivation
graph.
In the following section we present the algorithm which exploits isomor-
phism, while in Section 6 we discuss its relation to other work on automated
aggregation.
3 Algorithm
The algorithm for computing the reduced derivation graph of a PEPA model
begins by pre-processing a model which has been supplied by the modeller.
The purpose of this pre-processing is to re-express the model in a more
convenient form for the production of the aggregated derivation graph. The
aggregated derivation graph has at its nodes, equivalence classes of PEPA
terms, rather than single syntactic expressions. During the pre-processing
step the PEPA syntax is systematically replaced and the model expression is
converted into a vector form, which is then minimised and converted into its
canonical form. Every distinct PEPA expression maps to a distinct vector
form, but equivalent (isomorphic) expressions will have the same canonical
representation.
Once this pre-processing is complete, the generation of the reduced
derivation graph can begin. This process alternates between generating all
of the one-step derivatives of the present state and compacting these in order
to group together derivatives which have the same canonical representation.
The algorithm proceeds on the assumption that the model supplied is in
reduced named norm form. In the named form representation each derivative
of each sequential component is explicitly named. In the norm form the
model is expressed as a single model equation which consists of cooperations
of sequential components governed by hiding sets. In the reduced form all
cooperation and hiding sets have been reduced by removing any redundant
elements. If the supplied model is not in this form the necessary restructuring
is carried out before the algorithm is applied. The functions to achieve
this carry out routine checks on the validity of the model supplied and the
modifications that they make are completely transparent to the modeller.
We now proceed to describe these steps in more detail.
3.1 Restructuring the model
During the application of the algorithm it is convenient to have intermediate
derivatives in the model bound to identifiers. We generate these identifiers
as we decompose the defining equations for each sequential component. For
example, if the defining equation is
Comp
we introduce a name for the intermediate derivative by replacing this single
equation by the following pair of equations.
Comp
Once this has been done for each sequential component the model is said to
be in named form.
As described in Section 2, a PEPA model consists of a collection of
defining equations for sequential components and model components. One
of the model components is distinguished by being named as the initial
state of the model. The definition of this component may refer to other
model components, defined by other equations. We wish to eliminate uses
of model components from that definition, in order to reduce it to a normed
form in which the only identifiers used are those of sequential components.
We proceed by back-substituting the model component definitions into the
defining equation of the distinguished component. For example, the pair of
equations
Repman
System
ftaskg
Res
will become
ftaskg
Res  \Delta
Repman
We continue this process until it converges to a definition of a normed model
equation which consists only of cooperations of sequential components governed
by hiding sets.
If the cooperation or hiding sets in a model definition contain unnecessary
or redundant elements the equivalence classes formed by the algorithm
may not be optimal. Thus we can, in some circumstances, improve the
subsequent performance of the algorithm by removing redundant elements
from these sets before the algorithm is applied. Furthermore, the presence
of redundant elements in cooperation or hiding sets can be regarded as a
potential error on the part of the modeller; consequently the modeller is
warned of any reduction.
We have previously presented efficient algorithms for computing the sets
of activities (Act) which are performed by PEPA model components [10]
and we use these to reduce to the minimum the size of cooperation and
hiding sets in the following way.
This reduction is applied systematically throughout the normed model equa-
tion. This operation is bounded in complexity by the size of the static representation
of the input PEPA model and thus there is no hidden cost here of
a traversal of the state space which is generated by the dynamic exploration
of the model.
3.2 Pre-processing: vector form, minimisation, canonicalisa-
tion
The vector form of a model expression represents the model in the most
suitable form for our aggregation algorithm because it is amenable to efficient
calculation of its canonical form. Here we present the vector form as a
vector of sequential components with decorated brackets denoting the scope
of these sets. We use subscripted brackets to delimit a cooperation set and
superscripted angle brackets to delimit hiding sets.
In the implementation these vectors are represented by linked lists which
provide for efficient manipulation when forming canonical representatives.
Re-ordering and re-arrangement of the representations of components in
the vector forms can then be achieved by safe, statically-checked pointer
manipulation, thereby avoiding the overhead of the repeated copying of data
values which would be incurred by the use of an array-based representation.
For a model expression, we define the vector
form inductively over the structure of the expression: let M;N be expressions
and C be a constant denoting a sequential component.
1. vf (M  \Delta
2. vf
3. vf
In the following we write P to denote a vector
As with the normed model equation, the vector form representation contains
within a single expression all of the information about the static structure
of the model. It records the name of the current derivative of each of
the sequential components in addition to the scope of the cooperation and
hiding sets which are in force. The vector form alone is not sufficient to allow
us to compute the derivation graph of the model: the defining equations
for the sequential components are also needed.
Because it is generated directly from the full model equation the vector
form may include some redundancies. Hence, we include a preprocessing step
which is carried out to reduce the vector form generated by a straightforward
translation of the model equation to the vector form which will be used for
the remainder of the state space exploration. This step consists of generating
the minimal representation of the vector form, which is minimal with respect
to the number of brackets needed to record the scope of the cooperation and
hiding sets. As we will see, reducing the number of brackets in the vector
form may have significant impact on the aggregation which can be achieved.
Thus we can perform the following simplifications:
Elimination of redundant cooperation brackets: this arises when we
have a component such as Q  \Delta
R). The vector form of this
component would be (Q; contiguous brackets have
the same decoration in this way the inner one can be eliminated. In
this example this results in (Q;
Elimination of redundant hiding brackets: this would arise whenever
hiding brackets are contiguous regardless of their decoration. For ex-
ample, if we had a component (P=L)=K its vector form would be
This would be reduced to K[L hP i.
From the minimal vector form we reduce the model representation to its
canonical form. We can choose an arbitrary ordering on component terms-
one suitable ordering is lexicographic ordering. We denote this ordering by
We denote the canonicalisation function by C. We insert a
component P into a vector P using I P P. The definitions of these functions
are shown in Definition 2. The definitions are not complex but we include
them here for completeness and in order to prevent there appearing to be
any hidden complexity in their definitions.
(Canonicalisation and insertion functions) We present
the definition of the canonicalisation function first and the definition of the
insertion function second. There are three cases in the definition of each of
these functions.
1.
2. C L hP
3.
1. I P ()
2. I P
3. I P
3.3 Generating the aggregated derivation graph
The previous pre-processing steps have been applied to the input PEPA
model to facilitate the subsequent application of the aggregation algorithm.
Before pre-processing the model was represented by a PEPA expression,
which represented an individual (initial) state and contained all the information
necessary for its dynamic evolution. After the pre-processing steps
have been performed, the expression is reduced to canonical, minimal vector
which retains only information about the state structure of the model
and represents an equivalence class of states. Thus this canonical vector form
is a reduced representation in two senses. Firstly, the information about the
dynamic behaviour, cooperation sets and hiding sets, which is common to
all states of the model, is factored out and stored separately. Secondly, each
canonical vector form may in fact represent a number of equivalent model
states which would have distinct vector forms.
Generating the reduced derivation graph now proceeds via the following
two steps which are carried out alternately until the state space has been
fully explored.
Derivation: Given the vector form the objective is to find all enabled activities
and record them in a list, paired with the vector form of the
corresponding derivative. This is done by recursing over the static
structure of the current derivative. At the lowest level the sequential
components are represented simply as a derivative name. At this point
the defining equations are used to find the activity, or set of activities,
which are enabled by the derivative. We can identify three cases:
Individual activities which are not within the scope of a hiding
operator are recorded directly with the resulting derivative.
Individual activities which are within the scope of a hiding operator
are recorded as - actions with the appropriate rate together
with the resulting derivative.
ffl Activities which are within the scope of a cooperation set are
compared with the enabled activities of the other components
within the cooperation. If there is no matching activity the individual
activity is discarded; otherwise, as above, the activity is
recorded together with the resulting vector form.
Reduction: Carrying out the derivation may have given rise to vector forms
which are not canonical. Moreover several of the (activity, vector form)
pairs may turn out to be identical once the vector form is put into
canonical form. In this case the multiplicity is recorded and only one
copy is kept.
These two steps have to be repeated until there are no elements left in the
set of unexplored derivative classes.
In the remainder of this section we present these steps more formally,
but first we introduce some notation for describing the formulation and
manipulation of vectors and vector forms.
ffl Given a vector P, we write (P to denote the sub-vector of
those elements of P which satisfy the predicate OE. When the vector
P is obvious from the context we shall omit it, writing as an
abbreviation.
ffl We write P[P
to denote the vector obtained from P by substituting
ffl When S is a sub-vector (S similarly, we write P[S :=
as an abbreviation for P[S 1 := S 0
Note that we
only use vector substitution between vectors with the same number of
elements.
The rules which govern the derivation step of the algorithm are shown
in

Figure

4. The rule for constant formally states that at the lowest level
defining equations are used to find the activity or activities which can be
inferred from a derivative name. The two rules for hiding correspond to
the first two cases identified above. The most complex rules are those for
cooperation, the third case above. We examine these in more detail.
The first rule states the condition under which a number of identical ac-
tivities, (ff; r), give rise to derivatives which have identical canonical forms.
For this to be the case the activity (ff; r) must be enabled by one or more
component P i of P. Moreover, for each such possible activity, the vector
form of the resulting derivative is always the same when canonicalised. Formally

where oe is an arbitrary element of the vector S 0 , say its first element S 0
1 .
Note that the equation
1 does not imply that P 0
i and S 0
are equal,
only that they are in the same equivalence class because they have equal
canonical forms. The vector S 0 is defined as the sub-vector consisting of
those derivatives which may potentially change via an (ff; r) activity.
Having now formed a vector S satisfying these conditions for the activity
(ff; r) we can compute the rate at which the component performs this activity
and evolves to the canonical representative of the derivatives as jSj \Delta r, since
the total rate into the equivalence class will be the sum of the rates of the
individual activities which may make the move.
In the case where only one of the elements of the vector performs an
activity ff the complication due to the consideration of multiplicities does
not arise and the rule simplifies to be equivalent to the following.
Constant
Hiding
\Gamma\Gamma\Gamma!
\Gamma\Gamma\Gamma!
Cooperation
\Gamma\Gamma\Gamma! C(PL [S := S 0 ])
\Gamma\Gamma\Gamma! C(PL [S := S 0 ])
Y
r ff

Figure

4: Operational semantics of vector form
The complexity in the second rule for cooperation is due to the need
to calculate the rate at which the sub-vector of components in cooperation
performs the activity. Here also there is a simpler case, where the vector is
of size two. This special case of the rule affords easier comparison with the
operational semantics of PEPA, as presented in Figure 1.
\Gamma\Gamma\Gamma!
The rate R of the activity which is performed in cooperation is computed
from the individual rates r 1 and r 2 as in the corresponding cooperation rule
in

Figure

1.
3.4 Implementation
The state space reduction algorithm has been added to the PEPA Workbench
[5], the modelling package which implements the PEPA language and
provides a variety of solution and analysis facilities for PEPA models.
The algorithm is presented in pseudo-code form in Figure 5. The driving
force of the algorithm is provided by the procedure vfderive which,
given a derivative of the model, finds its enabled transitions using the function
cderiv, and calls itself on the resulting derivative. The function cderiv
carries out the canonicalisation of the one-step derivatives which it has produced
using the function derivatives. This function has different cases depending
on the structure of the vector form being handled, each reflecting
the appropriate rule(s) in the semantics. For example, in the case of a choice
the list of possible derivatives consists of the list of derivatives of the second
component of the choice appended to the list of derivatives of the first. The
derivatives of a vector of cooperating components are computed by using
the function cooperations to derive transitions and the function disallow to
enforce that activities of types in a cooperation set are not carried out without
a partner. We make use of a function lookup to retrieve the definitions
of component identifiers from the environment. Finally, the function update
takes a set of elements and a procedure and returns a set in which each
element has been modified by the procedure.
The modification to the PEPA Workbench required the alteration of the
data structure which is used to represent PEPA models as an abstract syntax
tree within the Workbench. The representation of cooperations between
pairs of components was generalised to extend to lists of components. If
the PEPA model which is submitted for processing does not contain any
if not marked (P )
then begin
mark
for each ((ff; r); n; P 0 ) in cderiv(P ) do
output transition (P (ff;n\Deltar)
begin
while d 0 is not empty do
choose (a; P ) from d 0 ;
if (a; n; P ) in r for some n
then replace (a; n; P ) by (a;
else add (a;
remove (a; P ) from d 0 ;
return
switch P is
case unary cooperation *)
return update(d; proc (a;
case n-ary cooperation *)
return
case L hP i (* hiding *)
return filter(d; L);
case (ff; r):P (* prefix *)
return singleton((ff; r); P );
case P +Q (* choice *)
return
case const C (* constant *)
return derivatives(lookup(C));
begin
while d is not empty do
remove x from d;
add P (x) to
return
if d 1 or d 2 is empty
then return ;
else
begin
remove
) from d 1 ;
remove
) from d 2 ;
if a
then
else
return
begin
while d is not empty do
remove ((ff; r); P ) from d;
if ff in L
then add ((-; r); P ) to r
else add ((ff; r); P ) to r
return
begin
while d is not empty do
remove ((ff; r); P ) from d;
if ff not in L
then add ((ff; r); P ) to r
return

Figure

5: Pseudo-code for the algorithm
structure which can be exploited by the state space reduction algorithm
then this change is invisible to any user of the Workbench. However, if the
PEPA model does contain either repeated components or other structure
which can be exploited then the benefits become apparent to the user of the
Workbench in terms of reduced time to generate the CTMC representation
of the model and in terms of the matrix of smaller dimension required for
its storage, once the model gets above a certain size (see Table 3).
4 Example
In this section we show how the algorithm works on an example. We consider
a multiprocessor system with a shared memory, we derive the corresponding
PEPA model, and then the underlying derivation graphs, both ordinary and
aggregated. Some alternatives to our approach are discussed in Section 5,
introduced by means of small variants of the same example.
4.1 Multiprocessor system
Consider a multiprocessor system with a shared memory. Processes running
on this system have to compete for access to the common memory:
to gain access and to use the common memory they need also to acquire
the system bus which is released when access to the common memory is
for simplicity the bus will not be explicitly represented in the
following. Processes are mapped onto processors. The processors are not
explicitly represented but they determine the rate of activities in the associated
processes, i.e. all processes have the same functional behaviour, but
actions progress at different speeds depending on the processor on which
they are running, and the number of processes present on the processor. It
is the modeller's responsibility to select rates appropriately.
A protocol which is not completely fair, but simply prevents one processor
from monopolising the memory, might impose that after each access of a
processor to the memory, some other processor must gain access before the
first can access again. A process running on the ith processor is represented
as
In this case, in order to impose the protocol, the memory is modelled as
remembering which processor had access last. Access for this processor is
disabled.
Mem i
If there are n i processes running on the ith processor the system is modelled
by the following expression
Sys
Mem k
Note that in the cooperation set of this model expression, and throughout
the remainder of the paper, we write get i as a shorthand for get
We assume that the starting state of the system excludes access
of an arbitrary processor, number k. The vector form of the model Sys ,
derived applying the equations of Definition 1, has the following form:
We now show an example derivation of the state space of Sys , both ordinary
and aggregated. For simplicity we consider a smaller system Sys 0 in which we
have only two processors and only two replicas of the same process running
on each processor. The simplified system is thus specified as
Mem 1
We can expand the derivatives of the processes P i , for and of the
memory Mem 1 as follows:
Mem 1
Mem 2
Initial state s1 :
Figure

Ordinary derivation graph of Sys 0
Complete derivation graph. The complete derivation graph of Sys
computed using the PEPA Workbench [5] with the aggregation algorithm
switched off, has 96 states and 256 transitions. A portion of this graph is
shown in Figure 6. To make the drawing easier to understand we have chosen
to name the derivatives with short names s i or s
depending on whether
the state has been completely expanded (s i ) or not (s
its
one-step derivatives are also represented). The vector forms corresponding
to the derivatives are listed in Table 2: each row contains the name of the
state and the corresponding vector form. Moreover, it contains information
on whether the vector form is canonical or not, and the name of the state
which represents the corresponding canonical vector form.
Aggregated derivation graph. The aggregated derivation graph, computed
using the PEPA Workbench with the aggregation algorithm switched
on, has 42 states and 88 transitions. A portion of this graph is shown in

Figure

7 and can be compared with the one of Figure 6.
The PEPA model Sys 0 has been constructed according to the algorithm:
the sequential components defining the processes and the memory are composed
by means of the cooperation operator to obtain the model equation.
All the derivatives have been explicitly named and we can use the model
equation to generate the vector form of the model which does not have
redundant brackets, and therefore no elimination is required.
At this point the aggregated state space can be obtained by considering
canonical vector forms only, as shown in the graph of Figure 7 in which
only a subset of the states of Table 2, those corresponding to the canonical
vector forms, is explicitly outlined. The names of the nodes are again s i
or s
i and the integer numbers in round brackets close to them specify the
number of equivalent states they represent. These numbers can be computed
by considering the number of replicas of the same process in the model
equation and the numbers of equal derivatives in each vector form. As an
example, let us consider the state s 10 which corresponds to the vector form
. This state represents four equivalent derivatives.
This number can be computed by dividing the product of the factorial of
the numbers of the repeated instances of components by the product of the
factorial of the numbers of identical derivatives in the vector form.
State Vector Form Canonical? Representative
s
s
22
26 ((P 0
28 ((P 0
Table

2: States and vector forms for
s
s
22 (4)
s
s
s
26 (2)
s 6 (1)
s
s 11 (1)

Figure

7: Aggregated derivation graph of Sys 0
More generally the formula could be expressed as follows
, is the number of processes running on the
same processor and n i;j are the numbers of equal derivatives of P i , such
that
The multiplicities of the arcs are also represented and indicate the number
of arcs which have been folded together. The fact that a single arc
represents one or more activities of the same type is reflected in the rate of
the action that labels the arc itself. For instance, the model evolves from the
state s 1 to the states s 3 by executing an action think with a rate 2- 1 because
in s 1 , i.e.
Mem 1 , two activities (think are
concurrently enabled.
Notice that the aggregation we obtain corresponds to finding permutations
of the same components within brackets. This form of aggregation
is pictorially represented in Figure 7 by flattening equivalent nodes of the
derivation graph of Figure 6 onto the same plane.
4.2 Timings
We ran different configurations of the multiprocessor system on a Pentium
III machine with clock frequency of 500 MHz and 128 MBytes of mem-
ory. The times recorded in Table 3 take into account both CPU time and
the time necessary for file I/O.
If there is a single component P i running on each processor, no aggregation
is possible and the execution times of the basic and the modified
Workbench are almost the same. As soon as we add replicas of the same
process, the state space aggregation becomes apparent (compare the second
and the fifth columns in Table 3) as well as the reduction in the execution
times (compare the fourth and the seventh columns), particularly when the
size of the model grows.
Alternative aggregations
In this section we illustrate some cases in which our algorithm, or indeed
any syntactic approach, cannot achieve the optimal theoretical partitioning.
In particular we show how greater aggregation could be achieved in some
circumstances if strong equivalence was used to generate partitions instead
Processors Derivation graph Aggregated derivation graph
Processes States Trans. Time (sec.) States Trans. Time (sec.)
Processors Derivation graph Aggregated derivation graph
Processes States Trans. Time (sec.) States Trans. Time (sec.)

Table

3: Execution times of the basic and modified Workbench
of isomorphism. Note, however, that these cases rely on quite strong conditions
on apparently unrelated activity rates. It is not clear that such conditions
occur with sufficient frequency in real models to justify the additional
complexity needed to implement an approach based on strong equivalence.
The strong equivalence relation is a more sophisticated notion of equiv-
alence, in the bisimulation style, based on observed behaviour. In general,
in a process algebra, two terms are bisimilar if their externally observed behaviour
appears to be the same. Strong equivalence assumes that both the
action type and the apparent rate of each activity is observable. Informally,
two PEPA components are strongly equivalent if their total conditional transition
rates to strongly equivalent terms are the same for all action types.
The conditional transition rate from P to P 0 via an action type ff is
denoted by q(P; This is the sum of the activity rates labelling arcs
connecting the corresponding nodes in the DG which are also labelled by
the action type ff. The conditional transition rate is thus the rate at which
a system behaving as component P evolves to behaving as component P 0
as the result of completing an activity of type ff. If we consider a set of
possible derivatives S, the total conditional transition rate from P to S,
denoted q[P; S; ff], is equal to
The definition can thus be formally stated as follows.
denote the set of all language terms, or derivatives. An
equivalence relation over derivatives, R ' T \Theta T , is a strong equivalence if
whenever then for all ff 2 A and for all S 2 T =R,
We say that P and Q are strongly equivalent, written
for some strong equivalence R, i.e.
fR j R is a strong equivalence g
Two of the following examples demonstrate the use of strong equivalence
for aggregation. However, in the first example we show how the abstraction
operator may be used at a higher syntactic level in the model and
introduce symmetries between components which appear quite distinct in
their defining equations. These symmetries rely on the context in which the
components are placed, something not currently captured by our algorithm.
In [11], Ribaudo distinguishes two form of aggregation which can be
found using strong equivalence. Horizontal aggregation arises from the interleaving
of the activities of similarly behaved components. This aggregation
takes advantage of repeated instances of the same pattern of behaviour
within the overall model structure. The aggregation found using
our algorithm may be termed a horizontal aggregation. In contrast, vertical
aggregation arises when there are repeated patterns of behaviour within a
single component. In the second example presented below, a variant of the
multiprocessor model is considered in which a horizontal aggregation can
be found using strong equivalence although isomorphism would regard the
components as distinct. Finally we give an example where a vertical aggregation
is possible with strong equivalence but not with isomorphism, and
consequently not with our syntactic approach.
5.1 Aggregation via abstraction
The facility to hide or abstract action types within a PEPA model is designed
to give the modeller the freedom to construct components in detail to ensure
that their behaviour is accurately represented but to subsequently restrict
the visible action types to only those relevant to the current modelling study.
For example, in the model of the multiprocessor presented in the previous
section, the modeller may choose to hide all the get i actions. In terms of
capturing the correct behaviour of the protocol it was important that these
action types were distinguished; but in terms of the complete model they
may all be regarded as internal - actions.
Hiding all of these activities introduces strong symmetries into the model
in terms of its functional behaviour. If, moreover, we find that the processes
which are running on different processors share the same timing characteris-
tics, i.e. - then the symmetries are apparent
in all aspects of the model's behaviour. Only one process can access the
memory at any time-and for the subsequent memory access its host processor
is excluded-but the processes on all other processors behave equiv-
alently. This means that we need only consider two classes of processors,
those excluded and those eligible for access, regardless of their placement on
processors. Once the get i activities are all hidden it is no longer possible to
identify from these process which type of process is operating.
For example, consider the multiprocessor with three processors, and two
processes running on the first, one on the second and two on the third. Then
if we regard the system immediately after the process P 2 has completed an
access to the memory and when one other process is waiting for access,
the behaviour of the system is isomorphic regardless of whether the waiting
process is on processor 1 or processor 3, i.e. all the following states are
isomorphic:
Mem
Mem
Mem
Mem
Although these states are equivalent by isomorphism our algorithm would
not place them within a single partition but into two: one consisting of
the first two states and one consisting of the second pair. This is because
the processes operating on different processors have distinct names and distinct
actions get i -this is necessary to ensure the correct functioning of the
protocol-and the syntactic form of minimisation that we use cannot recognise
that in some contexts P 1 and P 3 will behave equivalently.
This could be regarded as a penalty for the richness of the language. For
example, the analogous situation does not arise in Petri net-based models
because there is no notion of abstraction or hiding.
5.2 Horizontal aggregation via strong equivalence
Isomorphism is a strict structural equivalence: there must be a one-to-one
relationship between both derivatives and activities. The observation-based
strong equivalence is not so strict. Although corresponding derivatives must
be capable of the same action types at the same apparent rates, how these
are implemented as activities in the derivatives may differ as the following
example demonstrates.
Suppose that on processor 1 two different types of process may be run-
ning. The first is identical to the process P 1 discussed in Section 4.1. The
second has a similar pattern of behaviour but has two alternative local computations
between accesses to the common memory. The process -
below.
If the rates of the think activities are such that -
strongly equivalent to P 1 although the two are clearly not isomorphic. Thus
if we consider the system
Mem 2
our algorithm will distinguish the derivatives (P 00
Mem 0and (P 0
Mem 0
2 whereas a partitioning based on strong
equivalence would consider them to be equivalent. In this case the state
space aggregated by our algorithm will have 64 states whereas aggregation
based on strong equivalence would result in 42 states.
5.3 Vertical aggregation via strong equivalence
We can identify a second source of aggregation which can be achieved by
strong equivalence but which is not captured by our algorithm: so-called vertical
aggregation. Here we illustrate the vertical aggregation case by means
of another variant of the multiprocessor example. We consider a process
which, after the use of the memory, can detect an error. If this is the case
it does not return directly to the initial state; instead, it must complete a
recovery action and repeat the access to the memory. For this new process
the expansion of derivatives could be as follows:
where p is the probability that an error occurs. The derivation graph of
such a process P i is shown in Figure 8(a). Now we suppose that the action
(a) (b)

Figure

8: Derivation graphs of P i
types think and recover are hidden and become internal to the component.
Moreover, we assume that - . If this is the case the derivatives P i
and P 0000
are strongly equivalent, and we can aggregate them to form the
macro-state [P i ]. Similarly, we combine the arcs labelled (rel
and (rel ; p \Theta r) into a single arc labelled (rel ; r) connecting P 000

Figure

8(b)).
this form of aggregation relies on the information about the operational
behaviour of the component represented in the derivation graph.
It cannot be detected by the purely syntactic means used in our algorithm.
Approaches based on bisimulation style equivalences, such as strong equiv-
alence, work at the semantic rather than the syntactic level. Thus they are
not, in general, comparable to our approach.
6 Related work
The exploitation of symmetries to achieve aggregation of performance models
is a well-explored topic. Several automated approaches have been described
in the literature. In this section we give a brief account of some
of the work that has appeared in the context of stochastic Petri nets and
stochastic process algebras, and explain how that work relates to our own.
In each case the objective is to generate a partitioning of the original CTMC
which satisfies the condition of lumpability.
The closest approach to our own is the work on a class of stochastic
coloured Petri nets called Stochastic Well-formed Nets (SWN) [12]. Stochastic
Petri nets (SPN) [13] have been extensively used for the functional analysis
and performance evaluation of distributed systems. Their modelling
primitives consist of places and (timed) transitions, representing system
states and system events respectively. Just as in PEPA, in order to analytically
solve a SPN model, the associated stochastic process must be derived
by computing the set of reachable states (markings). Moreover, just as in
PEPA, for realistic systems the computation of the state space can often
lead to models whose size makes them intractable.
In order to tackle this problem SWN allow the construction of a parametric
representation of a system. This is achieved by folding similar subnets
and by adding a colour structure to distinguish tokens that, after the folding,
belong to the same place. The nets are restricted in terms of the possible
colour domains for places and transitions and in terms of the possible colour
functions. These restrictions allow symmetric structures within the model
to be exploited for solution purposes. In particular, these structures are
automatically detected and the reduced state space is constructed without
recourse to the complete state space. The reduction is obtained through the
concept of symbolic marking [12].
Informally, a symbolic marking corresponds to an equivalence class of
ordinary markings sharing the same characteristics. Unlike our approach,
there is no formal equivalence relation defined to underpin the partitioning.
In fact, the ordinary markings in the same equivalence class enable the same
set of transitions, whose firings lead to new ordinary states which are still
equivalent, i.e. belong to the same symbolic marking.
Starting from a symbolic representation of the initial marking a symbolic
reachability graph is constructed via a symbolic firing rule. Each symbolic
marking is represented in a minimal, canonical form. Note that unlike our
algorithm in which minimisation is carried out only in the preprocessing, in
the SWN case minimisation has to be repeated after each symbolic derivation
step. The symbolic reachability graph is used to generate a reduced CTMC
and it has been proved [14] that it is lumpably equivalent to the original
CTMC. Thus the same performance estimates can computed with a lower
computational cost.
Another Petri net-based approach has been developed in the context
of Stochastic Activity Networks (SAN) [15]. This formalism incorporates
features of both SPNs and queueing models and makes use of compositional
operators, similar to those found in process algebras. The primitives of the
formalism are places, activities (equivalent to Petri nets transitions), which
may be guarded by input gates, representing enabling rules, and output
gates representing completion rules. Once submodels have been constructed
representing the components of the system they may be combined using
the replication and join operations. The replication operator captures the
case of a system containing two or more identical subsystems. The join
operator combines SAN submodels of different types. Use of these operators
makes symmetries within the model explicit and so facilitates a compact
representation of the state space.
The structure of a composed SAN is represented by a directed tree with
different types of nodes. Leaf nodes capture the distinct SAN submodels,
i.e. the basic elements to which the construction operators apply. Internal
nodes with one child are replication nodes, their child being the submodel
to be replicated. Internal nodes with two or more children are join nodes,
the children representing the submodels to be joined together.
From this tree a state representation is automatically extracted that
is minimal in the sense that states which differ only by a permutation of
repeated components are grouped together into a single combined state.
Each such state is represented by recording, for each replication node, the
number of replicated SANs in each possible submodel marking, and for each
join node, a vector of the markings of each joined submodel. In addition
each state maintains information about the desired performance variable [15]
but this is outside the scope of this paper. There are clear parallels between
this state representation and our vector form discussed in Section 3.2.
The other work on aggregation of stochastic process algebra models is
developed almost entirely at the semantic level. In this approach well known
graph partitioning algorithms are used to reduce the labelled transition system
underlying the process algebra model [16, 4]. In [17] a more syntactic
approach is taken but this is on an ad hoc basis without a corresponding
tool implementation. Equational laws derived from Markovian bisimulation,
which is equivalent to strong equivalence, are used to obtain state space reduction
of a MTIPP model. This is achieved by term rewriting based on
judicious application of the laws. However, although good results can be
obtained on particular models, no set of term rewriting rules which can be
used for aggregation purposes have been found.
In some approaches good results have been obtained by modifying and
restricting the combinators of the language to make symmetries more explicit
and disallowing difficult cases. For example, in [18] a symmetric parallel
composition operator, denoted fn!PgS is used to capture the case of n-ary
parallel composition of identical replicas, all synchronising on actions
in S. This operator provides a means of expressing a number of replicated
copies of a process but it cannot express synchronisation of repeated copies
over different synchronisation sets. The operational semantics of the new
operator is consistent with the usual parallel composition but a reduced
state space is produced. This can be regarded as the SPA equivalent of the
SAN approach outlined above. States which differ only by a permutation of
replicated submodels are treated as equivalent.
Earlier work on MTIPP took a similar approach in terms of altering the
combinators of the language. In [19] a replication operator, here denoted
S P has the same informal semantics as fn!PgS above. Hiding and the usual
general parallel composition operator are removed from the language. The
distinction of this approach is that a denotational matrix semantics is given
rather than the more usual operational semantics. Using this approach the
infinitesimal generator matrix of the CTMC is constructed directly. Moreover
Rettelbach and Siegle show that the transition matrix resulting from
the semantics are minimal with respect to Markov chain lumpability (i.e.
the matrices do not have subsets of equivalent states).
The disadvantages of both these approaches are that they require the
modeller to adhere to a new set of combinators and this form of cooperation
does not allow different synchronisation sets amongst replicas of the same
component. The techniques do not appear to have been automated. In
contrast our algorithm works transparently with the PEPA language taking
advantage of whatever symmetries are present in the model submitted to
the PEPA Workbench by the user.
7 Conclusions and further work
We have shown how the existence of isomorphisms between terms in the
derivation graph of a stochastic process algebra model can be exploited to
aggregate the state space of the model. Our algorithm for this collapses the
derivation graph at each model state and does not require a costly computation
of bisimulation equivalence between components of the model. We have
found it to be applicable in situations where the full derivation graph is too
large even to be generated [20]. Further, we believe that many of the models
which occur in practice would contain symmetries of the types which can be
exploited by isomorphism. However, against these advantages our algorithm
cannot be guaranteed to achieve the maximum possible aggregation for all
models.
Generating an aggregated derivation graph will allow speedier computation
of the steady state probability distribution of the CTMC which corresponds
to a PEPA model. We have not discussed in this paper the influence
of aggregation on the interpretation of this probability distribution in terms
of the given PEPA model. When examining the steady state distribution in
order to determine performance factors such as throughput and utilisation
the PEPA modeller must now select sets of model states of interest via the
description of canonical representatives in the state space. This is an added
reason for choosing to aggregate with isomorphism instead of with bisimulation
because the formation of a canonical representative of an isomorphism
class is simpler. However, the full investigation of this issue remains as
further work.
Our work has been influenced by earlier work on SWN [21]. However,
we stress that significant adjustments to the approach have been necessary
for the development of the algorithm for SPA: it is not a straightforward
translation of results. Nevertheless we feel that there is considerable benefit
to be gained from studying the relationship between formalisms with the
objective of importing ideas, and when appropriate, techniques from one to
the other.

Acknowledgements

This collaboration took place within project "Rom/889/94/9: An enhanced
tool-set for performance engineers" funded by The British Council and
MURST. Stephen Gilmore is supported by the 'Distributed Commit Pro-
tocols' grant from the EPSRC and by Esprit Working group FIREworks.
Jane Hillston is supported by the ESPRC 'COMPA' grant.
The authors would like to thank the anonymous referees for helpful comments
on an earlier version of this paper and to thank Graham Clark for
implementation work on the PEPA Workbench.



--R

A Compositional Approach to Performance Modelling.
Stochastic process algebras.
A Tutorial on EMPA: A Theory of Concurrent Processes with Nondeterminism
Compositional Markovian modelling using a process alge- bra
The PEPA Workbench: A tool to support a process algebra based approach to performance modelling.

Compositional performance modelling with TIPPTool.
Finite Markov Chains.

From SPA models to programs.
On the aggregation techniques in stochastic Petri nets and stochastic process algebras.
Stochastic Well-Formed coloured nets for symmetric modelling applications
Performance analysis using stochastic Petri nets.
Stochastic Well-Formed coloured nets and multiprocessor modelling applications
Reduced Base Model Construction Methods for Stochastic Activity Networks.
Compositional nets and compositional aggregation.
Stochastic Process Algebras as a Tool for Performance and Dependability Modelling.
Exploiting Symmetries in Stochastic Process Algebras.
Compositional Minimal Semantics for the Stochastic Process Algebra TIPP.
Investigating an On-Line Auction System using PEPA
On Well-Formed coloured nets and their symbolic reachability graph
--TR

--CTR
Stephen Gilmore , Jane Hillston , Leila Kloul , Marina Ribaudo, PEPA nets: a structured performance modelling formalism, Performance Evaluation, v.54 n.2, p.79-104, 1 October
Marco Bernardo , Nadia Busi , Marina Ribaudo, Integrating TwoTowers and GreatSPN through a compact net semantics, Performance Evaluation, v.50 n.2-3, p.153-187, November 2002
Salem Derisavi , Peter Kemper , William H. Sanders , Tod Courtney, The Mbius state-level abstract functional interface, Performance Evaluation, v.54 n.2, p.105-128, 1 October
Daniel D. Deavours , Graham Clark , Tod Courtney , David Daly , Salem Derisavi , Jay M. Doyle , William H. Sanders , Patrick G. Webster, The Mbius Framework and Its Implementation, IEEE Transactions on Software Engineering, v.28 n.10, p.956-969, October 2002
David M. Nicol , William H. Sanders , Kishor S. Trivedi, Model-Based Evaluation: From Dependability to Security, IEEE Transactions on Dependable and Secure Computing, v.1 n.1, p.48-65, January 2004
stochastic process algebras;performance modeling;performance evaluation tools;model aggregation