===============================

Reactive Systems for Context Borrowing, Symbolic Execution and Web Service Binding

by Ugo Montanari
Dipartimento di Informatica
Università di Pisa

Joint work with Roberto Bruni, Gianluigi Ferrari, Fabio Gadducci,
Pawel Sobocinski and Emilio Tuosto

A systematic method for deriving bisimulation congruence from reduction rules has been proposed by Leifer and Milner, on turn inspired by Sewell. Also,the approach of observing contexts imposed on agents at each step has been proposed earlier by Montanari and Sassone, yielding the notion of dynamic bisimilarity. The basic idea of Leifer and Milner is to express "minimality"conditions for electing the context c among the (possibly infinite) ones that allow p to react. These conditions have been distilled by them in the notion of relative push-out (RPO) in a categories of reactive systems and made more general by Sassone, Sobocinski and Lack. The RPO construction is reminiscent of the unification process of logic programming, which in fact can be given an interactive semantics in much the same style. In the talk we present a short survey of the work by Leifer and Milner and Sassone, Sobocinski and Lack, and describe some recent developments which allow to see this approach under a larger viewpoint. The first contribution [1] observes contexts also for symbolic execution, suggesting applications to web service binding; the second [2] tackles the weak case by taking advantage of the tile model; and the third [3] uses cospan categories on adhesive categories, as suggested by Sassone, Sobocinski and Lack, for representing process calculi as graph transformation systems.

[1] Ferrari, G., Montanari, U. and Tuosto, E., Model Checking for Nominal Calculi, invited talk, in: Vladimiro Sassone, Ed., FOSSACS 2005, Springer LNCS 3441, 2005, pp. 1-24.

[2] Bruni, R., Gadducci, F., Montanari, U. and Sobocinski, P., Deriving Weak Bisimulation Congruences from Reduction Systems, in: Martin Abadi and Luca De Alfaro, Eds., CONCUR 2005, Springer LNCS, to appear.

[3] Gadducci, F. and Montanari, U., Observing Reductions in Nominal Calculi via a Graphical Encoding of Processes, in: Festschrift in Honor of Jan Willem Klop, Springer LNCS, to appear.