Abstract

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 ! , and forms of quantification. This logic is shown sound and complete with respect to atomic nets , 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