互联网 qkzz.net
全刊杂志网:首页 > 女性 > 文章正文
刊社推荐

基于DISCOVERER的Petri网不变式自动生成


□ 毕忠勤 单美静 陈光喜

   (1.华东师范大学 上海市高可信计算重点实验室, 上海 200062;2. 桂林电子科技大学 数学与计算科学学院,广西 桂林 541004)
  
  摘 要:
  在Petri网的验证中,代数不变式起着非常重要的作用。将Petri网建模为半代数变迁系统,提出了自动生成不变式的算法,该不变式有助于更好地分析Petri网可达空间。算法首先将Petri网的不变式假定为一个含参数系统,然后通过求解半代数系统来求解不变式中的参数;最后,基于DISCOVERER和QEPCAD等Maple软件包实现了该算法,并通过实例说明了算法的有效性。
  关键词:Petri网; 不变式; 半代数系统; 半代数变迁系统
  中图分类号:TP301文献标志码:A
  文章编号:1001-3695(2009)04-1320-03
  
  Discovering invariants for Petri nets with DISCOVERER
  
  BI Zhong-qin1, SHAN Mei-jing1, CHEN Guang-xi2
  
  (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. ......
很抱歉,暂无全文,若需要阅读全文或喜欢本刊物请联系《计算机应用研究》杂志社购买。
欢迎作者提供全文,请点击编辑
分享:
 

了解更多资讯,请关注“木兰百花园”
分享:
 
精彩图文


关键字
支持中国杂志产业发展,请购买、订阅纸质杂志,欢迎杂志社提供过刊、样刊及电子版。
关于我们 | 网站声明 | 刊社管理 | 网站地图 | 联系方式 | 中图分类法 | RSS 2.0订阅 | IP查询
全刊杂志赏析网 2017