Paolo Baldan (1) -
Andrea Bracciali (2) -
Roberto Bruni (2)
(1) Dipartimento di Matematica Pura e Applicata, Università di Padova, Italia. (2) Dipartimento di Informatica, Università di Pisa, Italia.
Abstract:
We propose a general methodology for analysing the
behaviour of open systems modelled as coordinators, i.e., open terms
of suitable process calculi. A coordinator is understood as a process
with holes or place-holders where other coordinators and components
(i.e., closed terms) can be plugged in, thus influencing its
behaviour. The operational semantics of coordinators is given by means
of a symbolic transition system, where states are coordinators and
transitions are labelled by spatial/modal formulae expressing the
potential interaction that plugged components may
enable. Behavioural equivalences for coordinators, like strong and
weak bisimilarities, can be straightforwardly defined over such a
transition system. Differently from other approaches based on
universal closures, i.e., where two coordinators are considered
equivalent when all their closed instances are equivalent, our
semantics preserves the openness of the system during its evolution,
thus allowing dynamic instantiation to be accounted for in the
semantics. To further support the adequacy of the construction, we
show that our symbolic equivalences provide correct approximations of
their universally closed counterparts, coinciding with them over
closed components. For process calculi in suitable formats, we show
how tractable symbolic semantics can be defined constructively using
unification.