HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Petri Nets Step Transitions and Proofs in Partially Commutative Linear Logic

Christian Retoré 1
1 S4 - System synthesis and supervision, scenarios
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : We encode the execution of Petri nets in Partially Commutative Linear Logic, an intuitionistic logic introduced by Ph. de Groote which contains both commutative and non commutative connectives. We are thus able to faithfully represent the concurrent firing of Petri nets as long as it can be depicted by a series-parallel order. This coding is inspired from the description of context-free languages by Lambek grammars. This report is an extended version (with complete proofs) of an article to appear in the proceedings of the Logic Colloquium 1999 (Utrecht).
Document type :
Complete list of metadata

Cited literature [29 references]  Display  Hide  Download

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 8:20:28 PM
Last modification on : Friday, February 4, 2022 - 3:16:12 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:02:49 PM


  • HAL Id : inria-00072299, version 1


Christian Retoré. Petri Nets Step Transitions and Proofs in Partially Commutative Linear Logic. [Research Report] RR-4288, INRIA. 2001. ⟨inria-00072299⟩



Record views


Files downloads