Abstract FR:

En logique classique, la formalisation du fonctionnement des reseaux de petri (rdp) se heurte a la perennite de la verite. En logique modale, elle impose la construction prealable du graphe des marquages accessibles. A contrario, la logique lineaire (ll) fondee par girard permet de formaliser directement par des sequents prouvables purement propositionnels les relations d'accessibilite dans les rdp : toute transition apparait comme une implication lineaire disponible ad libitum entre les propositions traduisant ses marquages d'entree et de sortie. Pour approfondir cette formalisation, nous definissons comme primitives en ll les notions de ressource, d'action et de consommabilite/productibilite, analogues mais distinctes de celles de proposition, de deduction et de verite/faussete en logique classique. Nous developpons une interpretation concrete pour tous les connecteurs lineaires en coherence avec leurs proprietes syntaxiques. Nous presentons le connecteur <<<>par<>>> comme un operateur de cumul disjoint d'exemplaires de ressources (dual du connecteur <<<>fois<>>> de cumul conjoint) et la negation lineaire <<<>nil<>>> comme un inverseur du sens du temps. Cette concretisation montre les limites des formalisations existantes des rdp en ll ; nous les generalisons en traduisant chaque transition par une implication lineaire ordinaire, traitee comme une ressource perissable, dont tout exemplaire consomme correspond a une occurrence de franchissement. Ainsi, nous apportons une expression logique aux aspects primordiaux du fonctionnement des rdp : nous demontrons qu'une relation d'accessibilite par sequence de transitions equivaut a un sequent prouvable et que l'equation fondamentale est l'expression algebrique d'un corollaire du critere d'equilibrage en ll. Grace a la combinatoire de tous les connecteurs lineaires, notre approche ouvre des perspectives d'analyse de relations complexes d'accessibilite comme celles de reprise apres defaillance dans un systeme industriel.