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).
Type de document :
Rapport
[Research Report] RR-4288, INRIA. 2001
Liste complète des métadonnées

Littérature citée [29 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00072299
Contributeur : <>
Soumis le : mardi 23 mai 2006 - 20:20:28
Dernière modification le : vendredi 13 janvier 2017 - 14:21:11
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:02:49

Fichiers

Identifiants

  • HAL Id : inria-00072299, version 1
  • Mot de passe :

Citation

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

Partager

Métriques

Consultations de la notice

165

Téléchargements de fichiers

172