A semantic framework for open processes

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.