随机Petri网模型到马尔可夫链的转换算法的证明

作     者：何炎祥 沈华 HE Yan-xiang;SHEN Hua

作者机构：武汉大学计算机学院武汉430072 武汉大学软件工程国家重点实验室武汉430072 湖北工业大学计算机学院武汉430068 

基　　金：国家自然科学基金项目(91118003 61170022)资助 

出 版 物：《小型微型计算机系统》 (Journal of Chinese Computer Systems)

年 卷 期：2014年第35卷第2期

页      码：339-342页

摘      要：随机Petri网具有很强的模型描述能力,马尔可夫链是一种常用的性能分析模型.为了有效利用随机Petri网进行性能的定量分析,给出了一个详细完整的随机Petri网模型转换为同构马尔可夫链的算法.运用Floyd不变式断言法证明了算法的部分正确性,运用良序集法证明了算法的终止性.算法是部分正确的且是可终止的,这个证明结论说明算法是完全正确的.为了佐证证明结论,基于Java和SQL Server设计开发了一个软件平台,在此平台上实现了转换算法,测试实例的测试结果验证了算法的正确性.对算法时间复杂性的分析表明算法是有效的.

主 题 词：随机Petri网 马尔可夫链 算法正确性证明 Floyd不变式断言法 良序集法 算法复杂性分析 

学科分类：08[工学] 081201[081201] 0812[工学-测绘类] 

核心收录：

D　O　I：10.3969/j.issn.1000-1220.2014.02.028

馆 藏 号：203858397...