| 基于DISCOVERER的Petri网不变式自动生成* |
| |
| 引用本文： | 毕忠勤,单美静,陈光喜.基于DISCOVERER的Petri网不变式自动生成*[J].计算机应用研究,2009,26(4):1320-1322. |
| |
| 作者姓名： | 毕忠勤 单美静 陈光喜 |
| |
| 作者单位： | 1. 华东师范大学,上海市高可信计算重点实验室,上海,200062
2. 桂林电子科技大学,数学与计算科学学院,广西,桂林,541004 |
| |
| 基金项目： | 国家自然科学基金重大研究计划重点项目（90718041）；国家重大基础研究计划资助项目（2004CB318003）；国家“863”计划资助项目（2007AA010302）；华东师范大学2008年优秀博士研究生培养基金资助项目（20080029） |
| |
| 摘 要： | 在Petri网的验证中，代数不变式起着非常重要的作用。将Petri网建模为半代数变迁系统，提出了自动生成不变式的算法，该不变式有助于更好地分析Petri网可达空间。算法首先将Petri网的不变式假定为一个含参数系统，然后通过求解半代数系统来求解不变式中的参数；最后，基于DISCOVERER和QEPCAD等Maple软件包实现了该算法，并通过实例说明了算法的有效性。
|
| 关 键 词： | Petri网 不变式 半代数系统 半代数变迁系统 |
Discovering invariants for Petri nets with DISCOVERER |
| |
| BI Zhong-qin,SHAN Mei-jing,CHEN Guang-xi.Discovering invariants for Petri nets with DISCOVERER[J].Application Research of Computers,2009,26(4):1320-1322. |
| |
| Authors: | BI Zhong-qin SHAN Mei-jing CHEN Guang-xi |
| |
| Affiliation: | 1.Shanghai Key Laboratory of Trustworthy Computing;East China Normal University;Shanghai 200062;China;2.School of Mathematics & Computing Science;Guilin University of Electronic Technology;Guilin Guangxi 541004;China |
| |
| Abstract: | This paper transformed Petri nets into a semi-algebraic transition system and presented an algorithm for generating the invariant of Petri nets, which was helpful to increase the accuracy of structural methods in calculating approximations of the reachability space. The method firstly assumed the invariant of Petri nets as a parameterized system, and then evaluated para-meters in the invariant by solving the corresponding semi-algebraic system. And implemented this method associated with the computer algebra software package-DISCOVERER and QEPCAD. From preliminary experimental results, the performance of this method is significant. |
| |
| Keywords: | Petri nets invariant semi-algebraic system semi-algebraic transition system |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机应用研究》浏览原始摘要信息 |
|
点击此处可从《计算机应用研究》下载全文 |
