Title
A semantic framework for open processes
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 placeholders 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 labeled 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. Different 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.
Year
DOI
Venue
2007
10.1016/j.tcs.2007.09.004
Theor. Comput. Sci.
Keywords
DocType
Volume
suitable process calculus,closed component,semantic framework,open process,operational semantics,symbolic bisimulation,tractable symbolic semantics,symbolic equivalence,Unification,open systems,Symbolic bisimulation,open system,process calculus,closed term,symbolic transition system,Open systems,closed instance,unication.
Journal
389
Issue
ISSN
Citations 
3
Theoretical Computer Science
3
PageRank 
References 
Authors
0.39
37
3
Name
Order
Citations
PageRank
P. Baldan1514.13
A. Bracciali2533.76
Roberto Bruni3123880.58