Modelling and verifying mobile systems using p-graphs

Abstract

This paper introduces the p-graphs, a graphical model of mobile interactions that tries to accommodate the expressivity of the p-calculus and the intuitiveness of place-transition nets. Graph rewriting techniques are used to describe the operational semantics of p-graphs.The bijective encoding/decoding of p-graphs allows to mix transparently graphical and term-based proof techniques, which leads to a dual characterization of bisimilarity. The main originality of this characterization is the synchronous interpretation it provides: each graph/term being attached to a clock evolving at the rate of interactions with the environment.This gives new opportunities for the design of efficient verification algorithms for mobile systems. © Springer-Verlag Berlin Heidelberg 2009.