Linear Logic on Petri Nets

Uffe Henrik Engberg, Glynn Winskel

    Research output: Book/anthology/reportReportResearch

    9 Citations (Scopus)

    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.\bibpar 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 $\otimes$, $-\!\raise+.3ex\hbox {\boldmath$\scriptscriptstyle\circ$}$, $\vphantom{\oplus}\raisebox{-1.15pt}{\rm\&}$, $\oplus$ and the exponential ${!}$ (``of course''), and forms of quantification. This logic is shown sound and complete with respect to {\em 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.
    Original languageEnglish
    Place of publicationUniversity of Aarhus
    PublisherBRICS
    EditionRS-94-3 in Report Series
    Number of pages54
    Publication statusPublished - 1994

    Fingerprint

    Dive into the research topics of 'Linear Logic on Petri Nets'. Together they form a unique fingerprint.

    Cite this