基于量词消去的Petri网不变式自动生成  

Generating Invariants for Petri Net Using Quantifier Elimination

作　　者：毕忠勤[1] 

机构地区：[1]上海电力学院计算机与信息工程学院,上海200090

出　　处：《上海电力学院学报》2011年第1期75-78,86,共5页Journal of Shanghai University of Electric Power

基　　金：上海市优秀青年教师培养基金(SDL10010)

摘　　要：基于模板和量词消去建立了一个求解Petri网不变式的算法.引入一个带参模板作为Petri网的候选不变式,再根据不变式必须满足归纳断言初始条件和承接条件,将Petri网的自动生成问题转化为量词消去问题,并求解出带参模板中的参数得到原Petri网的不变式.最后通过两个算例说明了该算法的有效性.A new approach is presented to generate invariants for Petri net based on template and quantifier elimination.The main idea is to introduce a candidate parametric invariant as template and then reduce the invariant generation of Petri net into a quantifier elimination problem using the initial condition and consecution condition which the invariant should satisfy.From the preliminary experiment results,the feasibility of the approach is demonstrated.

关 键 词：PETRI网 不变式 量词消去 半代数变迁系统 

分 类 号：TP393.028[自动化与计算机技术—计算机应用技术]