【摘要】 在Petri网的验证中,代数不变式起着非常重要的作用。将Petri网建模为半代数变迁系统,提出了自动生成不变式的算法,该不变式有助于更好地分析Petri网可达空间。算法首先将Petri网的不变式假定为一个含参数系统,然后通过求解半代数系统来求解不变式中的参数;最后,基于DISCOVERER和QEPCAD等Maple软件包实现了该算法,并通过实例说明了算法的有效性。更多还原

【Abstract】 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.更多还原