Completeness results for linear logic on Petri nets Original Research Article

Completeness is shown for several versions of Girardʹs linear logic with respect to Petri nets as the class of models. One logic considered is the ⊕-free fragment of intuitionistic linear logic without the exponential !. For this fragment Petri nets form a sound and complete model. 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), though only once we add extra axioms specific to the Petri-net model. 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. Unfortunately, with respect to this logic, whether an assertion is true of a finite net becomes undecidable.