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) .