Linear Logic on Petri Nets
Uffe H. Engberg and Glynn Winskel February 1994 |

## 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
Available as |

Last modified: 2003-06-08 by webmaster.