Protocol specification using P-graphs, a technique based on coloured Petri Nets

P-Graphs combine inhibitor Petri nets and abstract data types within the same algebraic framework. They are useful for the specification of concrete concurrent systems and in particular communication protocols. The inhibitor has been included to allow compact descriptions of systems by promoting the economy of data types. They are also necessary for the purging of resources; a common activity when modelling protocols or their services. This paper introduces P-Graphs with the aid of some simple examples. It also shows how to map P-Graphs to P-nets, which are Coloured Petri Nets (CP-nets) extended with place capacities and inhibitors. This is important for the analysis of P-Graph specifications, as P-nets can be transformed to CP-nets in almost all practical situations. Thus the analysis techniques of CP-nets can then be applied. Useful notation for capacities are introduced and their semantics defined in terms of the P-Graph. A notation for purging places of their tokens is also introduced, involving the superimposition of the inhibitor and normal arc. Two case studies, the Demon game and the M-Access Service of the Cambridge Fast Ring, are included to illustrate the use of the P-Graph and the extended notation for protocol specification.