Abstract:
This article shows how individual Petri nets form models of Girard's intuitionistic linear logic. It explores questions of expressiveness and completeness of linear logic with respect to this interpretation. An aim is to use Petri nets to give an understanding of linear logic and give some appraisal of the value of linear logic as a specification logic for Petri nets. This article might serve as a tutorial, providing one in-road into Girard's linear logic via Petri nets. With this in mind we have added several exercises and their solutions. We have made no attempt to be exhaustive in our treatment, dedicating our treatment to one semantics of intuitionistic linear logic.
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. A start is made on
decidability issues.
Available as PostScript, PDF, DVI.