本文已被：浏览 1316次 下载 529次
投稿时间：2010-07-12
投稿时间：2010-07-12
中文摘要: 基于模板和量词消去建立了一个求解Petri网不变式的算法.引入一个带参模板作为Petri网的候选不变式,再根据不变式必须满足归纳断言初始条件和承接条件,将Petri网的自动生成问题转化为量词消去问题,并求解出带参模板中的参数得到原Petri网的不变式.最后通过两个算例说明了该算法的有效性.
Abstract: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.
文章编号：20110118 中图分类号： 文献标志码：
基金项目:上海市优秀青年教师培养基金(SDL10010)
| 作者 | 单位 | |
| 毕忠勤 | 上海电力学院 计算机与信息工程学院, 上海 200090 | zqbi@shiep.edu.cn. |
| Author Name | Affiliation | |
| BI Zhong-qin | School of Computer and Information Engineering, Shanghai University of Electric Power, Shanghai 200090, China | zqbi@shiep.edu.cn. |
引用文本：
毕忠勤.基于量词消去的Petri网不变式自动生成[J].上海电力大学学报,2011,27(1):75-78,86.
BI Zhong-qin.Generating Invariants for Petri Net Using Quantifier Elimination[J].Journal of Shanghai University of Electric Power,2011,27(1):75-78,86.
毕忠勤.基于量词消去的Petri网不变式自动生成[J].上海电力大学学报,2011,27(1):75-78,86.
BI Zhong-qin.Generating Invariants for Petri Net Using Quantifier Elimination[J].Journal of Shanghai University of Electric Power,2011,27(1):75-78,86.