Completeness Results for Linear Logic on Petri Nets

Completeness is shown for several versions of Girard’s linear logic with respect to Petri nets as the class of models. The strongest logic considered is intuitionistic linear logic, with ⊗, ⊸, &, ⊕ and the exponential! (“of course”), and forms of quantification. This logic is shown sound and complete with respect to atomic nets (these include nets in which every transition leads to a nonempty multiset of places). The logic is remarkably expressive, enabling descriptions of the kinds of properties one might wish to show of nets; in particular, negative properties, asserting the impossibility of an assertion, can also be expressed.