## Relating Petri Nets to Formulae of Linear Logic

**Carolyn Brown**
*Abstract:* This paper investigates a connection between
linear logic and Petri nets. From the basis that the \otimes
operator applies to two events which may occur concurrently and
independently, while linear implication reflects causal dependency
between events, we build up a correspondence between Petri nets and
certain formula of linear logic. We consider the fragment of linear
logic *L1* comprising \otimes, -o, \wedge and !, and show that
whenever a formula *F_{N}* represents a Petri net N, then
*F_{N}* \vdash *G* iff *G* represents *N'*, a
possible future state of the net N (Theorem 7.1).

In addition, we show that if *F_{N}* represents N in a
canonical way then whenever *F_{N}* \vdash *G*, there
exists a canonical derivation of *F_{N}* \vdash *F'_{N}*,
where *F'_{N}* is the canonical formula representing the net
N' (the net represented by *G*) and *F_{N'}* \cong
*G*. The significant property of such a canonical derivation
is that it only introduces implication between formulae which
represent groups of places which are causally dependent on one
another in the net.

*ECS-LFCS-89-87*

Previous |

Index |

Next