| 基于量词消去的Petri网不变式自动生成 |
| |
| 引用本文： | 毕忠勤. 基于量词消去的Petri网不变式自动生成[J]. 上海电力学院学报, 2011, 27(1): 75-78,86 |
| |
| 作者姓名： | 毕忠勤 |
| |
| 作者单位： | 上海电力学院,计算机与信息工程学院,上海,200090 |
| |
| 基金项目： | 上海市优秀青年教师培养基金 |
| |
| 摘 要： | 基于模板和量词消去建立了一个求解Petri网不变式的算法.引入一个带参模板作为Petri网的候选不变式,再根据不变式必须满足归纳断言初始条件和承接条件,将Petri网的自动生成问题转化为量词消去问题,并求解出带参模板中的参数得到原Petri网的不变式.最后通过两个算例说明了该算法的有效性.
|
| 关 键 词： | Petri网 不变式 量词消去 半代数变迁系统 |
| 收稿时间： | 2010-07-12 |
Generating Invariants for Petri Net Using Quantifier Elimination |
| |
| 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 |
| |
| Authors: | BI Zhong-qin |
| |
| Affiliation: | BI Zhong-qin (School of Computer and Information Engineering,Shanghai University of Electric Power,Shanghai 200090,China) |
| |
| 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. |
| |
| Keywords: | Petri net invariant quantifier elimination semi-algebraic transition system |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《上海电力学院学报》浏览原始摘要信息 |
|
点击此处可从《上海电力学院学报》下载全文 |
