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

• 作者: 单美静 毕忠勤 陈光喜
• 来源期刊: 计算机应用研究
• 关键词: Petri网 不变式 半代数系统 半代数变迁系统
• 年，卷（期）: 2009,（4）
• 所属期刊栏目: 软件技术研究
• 页码范围: 1320-1322,1337
• 页数: 4页
• 分类号: TP301
• 语种: 中文
• DOI: 10.3969/j.issn.1001-3695.2009.04.035

摘要

在Petri网的验证中,代数不变式起着非常重要的作用.将Petri网建模为半代数变迁系统,提出了自动生成不变式的算法,该不变式有助于更好地分析Petri网可达空间.算法首先将Petri网的不变式假定为一个含参数系统,然后通过求解半代数系统来求解不变式中的参数;最后,基于DISCOVERER和QEPCAD等Maple软件包实现了该算法,并通过实例说明了算法的有效性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	毕忠勤	华东师范大学上海市高可信计算重点实验室	5	13	2.0	3.0
2	陈光喜	桂林电子科技大学数学与计算科学学院	82	455	12.0	16.0
3	单美静	华东师范大学上海市高可信计算重点实验室	5	6	1.0	2.0