Verification of siphons and traps for algebraic petri nets

Abstract

Siphons and traps are structures which allow for some implications on the neCs behaviour and can be used in manual correctness proofs for concurrent systems. We introduce symbolic representations of siphons and traps which work quite well even in infmite cases and are still intuitively readable. The verification of symbolic siphons and traps is traced back to unification and structural induction on the terms. This approach is motivated by some additional considerations. For unification and other proposed structural reasoning mechanisms tool support is given by completeness proof tools studied in the theorem-proving community.