Petri Nets as Quantales

Carolyn Brown

Abstract: This paper brings together two areas of interest in linear logic. It is known that proof in linear logic corresponds to evolution of Petri nets in a precise way, and also that quantales are an algebraic model of linear logic. We here show how a Petri net can be used to generate a quantale whose structure reflects the behaviour of the net. Such a net-quantale can then be used to give a sound interpretation of the linear logic proof rules. This interpretation allows us to specify properties of nets. The sorts of properties we can specify may be possibilities, which are expressed using implication, or impossibilities (safety properties, in effect), which are expressed using negation. The quantale also gives rise to an equivalence on nets.


Previous | Index | Next