## Linear Logic and Petri Nets: Categories, Algebra and Proof

**Carolyn T Brown**
*Abstract:* This thesis explores three ways in which linear
logic may be used to define a specification language for Petri
nets, by giving precise correspondences, at different levels,
between linear logic and Petri nets.

Firstly, we define categories **NC** by analogy with de
Paiva's dialectica categories **GC**. The category **NSet**
has objects the elementary Petri nets and morphisms refinement
maps. We show that **GC** induces in **NC** sufficient
structure for **NC** to be a sound model of linear logic. We
demonstrate the computational significance of the net constructors
induced by the interpretation in **NSet** of the linear
connectives \otimes, \wedge, -- \circ, \oplus and (--)^{\perp}. Our
framework unifies several existing approaches to categories of
nets, and gives a model of full linear logic based on nets.

Secondly, we show that the possible evolutions of a net generate
a quantale. Quantales are algebraic models of linear logic.
Further, we show that certain restrictions on nets, including being
safe or bounded, arise as subquantales induced by suitable
conuclei. This approach allows us to give a sound semantics for
linear logic using sets of markings of a given net. Thus the
provability of certain assertions in linear logic corresponds to
properties of nets.

Thirdly, we define a semantics for a fragment of linear logic
*L*_{0} in terms of nets, by giving a partial function from
formulae of linear logic to nets. This semantics is complete and
sound where defined.

Further, we show that whenever a net N can evolve to a net N
\prime, there is a canonical proof in *L*_{0} that the formula
interpreted by N entails the formula interpreted by *N*
\prime. A canonical proof expresses the causal dependencies of a
net in a precise way, using the (Cut) rule. This approach allows us
to use the techniques of proof theory to study the evolution of
nets.

**Ph.D Thesis - Price £8.50**

*LFCS report ECS-LFCS-91-129 (also published as
CST-71-91)*

Previous |

Index |

Next