Formalisation en logique linéaire du fonctionnement des réseaux de Petri

In classical logic, the formalisation of the Petri net token game faces the invariance of truth. In modal logic, it requires first to construct the reachable marking graph. In contrast, Girard's linear logic allows us to use purely propositional provable sequents to directly formalise the reachability relations in a net: each transition appears as a linear implication available ad libitum between the propositions translating its input and output markings. To study thoroughly this formalisation, we define as primitives in linear logic the notions of resource, action and consummability/producibility, analogous but distinct from those of proposition, deduction and truth/falseness in classical logic. We establish a concrete interpretation of the linear connectives with respect to their syntactical properties. The connective "par" is presented as an operator of disjoint accumulation of resource items (dual of the connective ¿times¿ of joint accumulation) and the linear negation "nil" as a time inversion. This concrete view brings out the limits of the existing formalisation of the token game. We increase the expressive power of these formalisations by translating each transitions as an ordinary linear implication, being itself a perishable resource, whose consuming represents a transition occurrence in firing sequence. We give a logical expression to the essential features of the Petri net token game : we demonstrate that a reachability relation by firing sequence is equivalent to a provable sequent and that the fundamental equation is an algebraic expression of the balancing criterion of linear logic. By means of the combinatory of all linear connectives, our approach opens perspectives for analysing complex reachability relations, e. g. for recovering after crash in an industrial system.En logique classique, la formalisation du fonctionnement des réseaux de Petri (RdP) se heurte à la pérennité de la vérité. En logique modale, elle impose la construction préalable du graphe des marquages accessibles. A contrario, la logique linéaire (LL) fondée par Girard permet de formaliser directement par des séquents prouvables purement propositionnels les relations d'accessibilité dans les RdP : toute transition apparaît comme une implication linéaire disponible ad libitum entre les propositions traduisant ses marquages d'entrée et de sortie. Pour approfondir cette formalisation, nous définissons comme primitives en LL les notions de ressource, d'action et de consommabilité/productibilité, analogues mais distinctes de celles de proposition, de déduction et de vérité/fausseté en logique classique. Nous développons une interprétation concrète pour tous les connecteurs linéaires en cohérence avec leurs propriétés syntaxiques. Nous présentons le connecteur « par » comme un opérateur de cumul disjoint d'exemplaires de ressources (dual du connecteur « fois » de cumul conjoint) et la négation linéaire « nil » comme un inverseur du sens du temps. Cette concrétisation montre les limites des formalisations existantes des RdP en LL ; nous les généralisons en traduisant chaque transition par une implication linéaire ordinaire, traitée comme une ressource périssable, dont tout exemplaire consommé correspond à une occurrence de franchissement. Ainsi, nous apportons une expression logique aux aspects primordiaux du fonctionnement des RdP : nous démontrons qu'une relation d'accessibilité par séquence de transitions équivaut à un séquent prouvable et que l'équation fondamentale est l'expression algébrique d'un corollaire du critère d'équilibrage en LL. Grâce à la combinatoire de tous les connecteurs linéaires, notre approche ouvre des perspectives d'analyse de relations complexes d'accessibilité comme celles de reprise après défa illance dans un système industriel