Completeness Results for Linear Logic on Petri Nets
Uffe Engberg, Glynn Winskel · DAIMI Report Series · 1993
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 $\otimes$, $-\!\circ$, \&, $\oplus$ 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.