Discovering invariants for Petri nets with DISCOVERER
基于DISCOVERER的Petri网不变式自动生成*

This paper transformed Petri nets into a semi-algebraic transition system and presented an algorithm for generating the invariant of Petri nets, which was helpful to increase the accuracy of structural methods in calculating approximations of the reachability space. The method firstly assumed the invariant of Petri nets as a parameterized system, and then evaluated para-meters in the invariant by solving the corresponding semi-algebraic system. And implemented this method associated with the computer algebra software package-DISCOVERER and QEPCAD. From preliminary experimental results, the performance of this method is significant.