Copyright Information
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other
copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying
this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without
the explicit permission of the copyright holder.
Sensoria Bibliography Site Open bisimulation for the concurrent constraint pi-calculus
Maria Grazia Buscemi, Ugo Montanari
abstract:
The concurrent constraint pi-calculus (cc-pi-calculus) has been
introduced as a model for concluding Service Level Agreements. The
cc-pi calculus combines the synchronous communication paradigm of
process calculi with the constraint handling mechanism of concurrent
constraint programming. While in the original presentation of the
calculus a reduction semantics has been proposed, in this work we
investigate the abstract semantics of cc-pi processes. First, we
define a labelled transition system of the calculus and a notion of
open bisimilarity a'la pi-calculus that is proved to be a
congruence. Next, we give a symbolic characterisation of
bisimulation and we prove that the two semantics coincide.
Essentially, two processes are open bisimilar if they have the same
stores of constraints - this can be statically checked - and if
their moves can be mutually simulated. A key idea of the symbolic
transition system is to have `contextual' labels, i.e. labels
specifying that a process can evolve only in presence of certain
constraints. Finally, we show that the polyadic Explicit Fusions
calculus introduced by Gardner and Wischik can be translated into
monadic cc-pi and that such a transition preserves open
bisimilarity. The mapping exploits fusions and tuple unifications
as constraints.
