论文部分内容阅读
基于模板和量词消去建立了一个求解Petri网不变式的算法.引入一个带参模板作为Petri网的候选不变式,再根据不变式必须满足归纳断言初始条件和承接条件,将Petri网的自动生成问题转化为量词消去问题,并求解出带参模板中的参数得到原Petri网的不变式.最后通过两个算例说明了该算法的有效性.