Modeling a Service and Session Calculus with Hierarchical Graph Transformation

Abstract

Graph transformation techniques have been applied successfully to the
modelling of process calculi, for example for equipping them with a
truly concurrent semantics. Recently, there has been an increasing
interest towards hierarchical structures both at the level of
graph-based models, in order to represent explicitly the interplay
between linking and containment (like in Milner's bigraphs), and at
the level of process calculi, in order to deal with several logical
notions of scoping (ambients, sessions and transactions, among
others). In this paper we show how to encode a sophisticated calculus
of services and nested sessions by exploiting a suitable flavour of
hierarchical graphs. For the encoding of the processes of this
calculus we benefit from a recently proposed algebra of graphs with
nesting.