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