Application of linear logic to backward reachability analysis of Colored Petri Nets

This paper deals with a formal method for the study of the backward reachability analysis applied on Colored Petri Nets (CPN). The proposed method proceeds in two steps : 1) it translates CPN to terms of the Multiplicative Intuitionistic Linear Logic (MILL); 2) it proves sequents by constructing proof trees. The translation from CPN to MILL must respect some properties such as the semantic associated to tokens. That is why, the First Order MILL (MILLI) is used for translation. The reachability between two markings, the initial marking and the final marking, is expressed by a sequent which can be proven (if the initial marking is backwardreachable from the final one) using firstorder terms unification and/or marking enhancement.