*For the most recent entries see the
Petri Nets Newsletter.*

## Linear Logic on Petri Nets.

Engberg, U.;
Winskel, G.
In:
de Bakker, J.W.; de Roever, W.-P.; Rozenberg, G.: *Lecture Notes in Computer Science, Vol. 803; A Decade of Concurrency*, pages 176-229.
Springer-Verlag,
June 1993.

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. This logic
is shown sound and complete with respect to atomic nets (this 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.

Keywords:
Linear logic; Petri nets.

*Do you need a refined search? Try our search engine
which allows complex field-based queries.*
*Back to the Petri Nets Bibliography*