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.


Previous | Index | Next