In: Lecture Notes in Computer Science, Vol. 711: MFCS'93. Springer-Verlag, 1993.
Abstract: 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.