  Given that the sequent calculus for linear logic uses multisets of formulas, proof search can directly encode multiset rewriting. Since many computations can naturally be seen as multiset rewriting, it has been possible to make numerous connections between linear logic and Petri nets  (Gunter &amp; Gehlot 1989),  process calculi  (Andreoli &amp; Pareschi 1991,  Kobayashi et al. 1999,  Miller 1996),  and security protocols  (Cervesato et al. 1999,  Miller 2003).