Curry-Howard isomorphism has proved very fruitful as a methodological tool for exploiting the deep relationship among typed lambda calculus, intuitionistic logic and cartesian closed categories, A direct payoff of this has been the design of functional programming langages with powerful type systems, Limear logic is a logic of actions that seems weell suited for concurrent computation. In this paper, we establish a correspondence between Petri nets, linear logic and symmetic monoidal categories.