SPA syntax is based on the following elements:
a set of *input* actions, a
set of *output*
actions, a set of *visible*
actions, ranged over by , and the usual function such
that and ;two sets and of high and low level
actions such that , , and where ; a set of actions
( is the internal, invisible action), ranged over by
; a set *K* of constants, ranged over by *Z* .
The syntax of SPA *agents* is defined as follows:
where and is such that .Moreover, for every constant *Z* there must be the corresponding
definition: . The meaning of , , *E*+*E* ,
*E*|*E* , , *E*[*f*] and
is as for CCS [Mil89].
Intuitively, is the empty
process, which
cannot do any action; can do an action and then behaves
like *E* ; can alternatively choose to behave like
or ; is the parallel composition of and ,where the executions of the two systems are interleaved, possibly
synchronized on complementary input/output actions, producing an
internal . can execute all the actions *E* is able to do, provided
that they do not belong to ; *E* / *L*
turns all the actions in *L* into internal 's;
if *E* can execute action , then *E*[*f*] performs
; finally, *Z* does what *E* does, when .

Let be the set of
SPA agents,
ranged over by *E* , *F* .
Let denote the *sort* of *E* , i.e., the set of
the (possibly executable) actions occurring syntactically in *E* .
The sets of high level agents and low level ones are defined as
and , respectively.
The operational semantics of SPA is given (as usual) associating to each
agent a particular state of the labelled transition system
where and, intuitively,
means that agent *E* can
execute moving to *E*' (see [FG95,FG] for more details).

In the following the expression is a shorthand for ,where denotes a (possibly empty) sequence of labelled transitions. We also extend the `' notation to sequences of actions; with means that such that . For the empty sequence we have that stands for .

We recall here the definition of trace equivalence

**Definition 2.1**

A trace of a process *E*
is a sequence of actions that *E* can execute. The set of
traces is defined as follows:
. *E* and *F* are *trace equivalent*
(notation ) if and only if *T*(*E*) = *T*(*F*) .