论文研究 基于DISCOVERER的Petri网不变式自动生成.pdf

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