Verification of distributed algorithms with algebraic Petri Nets

Abstract

This paper demonstrates by help of an example how algebraic Petri nets can be used for modelling and verification of distributed algorithms. For lack of space we could only sketch the used proof techniques; still the proof should provide a flavour of our method. In essence the basic technique for deriving simple temporal properties is to verify the validity of some state formulas which are derived from the structure of the net and the verified formula: equations for place invariants, simple implications for siphons and traps, and some more complex implications for assertions. Though not completely explained here, even the pick up rule for leadsto properties can be reduced to checking the validity of some state formulas. For combining temporal formulas in order to verify more complex properties we mainly use standard rules: weakening of invariants, PSP-rule and proof graphs for liveness properties.

A formal presentation of this method is beyond the scope of this paper. A formal presentation of algebraic nets as used in this paper can be found in [3]; more information about the verification techniques and some more interesting examples can be found in [4, 8].

This work was supported by the DFG (Project ‘Distributed Algorithms’).