J. Fanchon, N. Rivière, B. Pradin-Chézalviel, R.
Valette
LAAS-CNRS,
F-31077 Toulouse Cedex 4, France
Présenté à :
MSR 2003, Modélisation des sytèmes réactifs,
Metz, 6-8 octobre 2003, p.261-276, Editions Lavoisier,
ISBN 2-7462-0778-8
L'équivalence entre accessibilité dans les réseaux de Petri et prouvabilité de certains séquents de logique linéaire a été montrée de différentes manières. Notre travail présenté ici raffine ce résultat, d'une part parce qu'il prend en compte les spécificités de la traduction que nous avons utilisée dans nos travaux antérieurs et d'autre part parce qu'il étudie les relations entre l'ordre d'application des règles dans la preuve des séquents et les process finis associés au même problème d'accessibilité. Nous prouvons qu'à partir d'un arbre de preuve canonique, nous pouvons construire un process fini équivalent et que réciproquement, pour chaque process fini, un arbre de preuve canonique peut être construit. Une contribution de cet article est de montrer que l'efficacité du calcul des séquents en logique linéaire dans le fragment multiplicatif mis en oeuvre ici peut être utilisée afin de déterminer les process finis d'un réseau de Petri quelconque.
Process, Réseau de Petri, Logique linéaire, Ordres partiels, Arbres de preuves
Equivalence between reachability in Petri nets and provability of certain sequent of Linear logic has been proven in various ways. Our contribution refines this result in two ways. It considers the specific translation introduced in our previous work and it studies the relationships between the order of the rule application in the sequent proof and the finite processes associated with the same reachability problem. We prove that from a canonical proof tree, an ``équivalent'' finite process can be derived and reciprocally that for each finite process, an``equivalent'' canonical proof tree can be constructed. One of the contributions of this paper is that the effectiveness of linear logic sequent calculus in the multiplicative fragment used here can be used for determining the finite processes of any Petri net.
Process, Petri net, Linear logic, Proof trees, Partial orders