Prove of Algorithm for Converting Stochastic Petri Net Model to Markov Chain
HE Yan-xian · Journal of Chinese Computer Systems · 2014
Stochastic Petri net has strong description ability.Markov chain is commonly used as a performance analysis model.In order to effectively using Stochastic Petri net to performance quantitative analysis,this paper presents a detailed and complete algorithm for converting Stochastic Petri net model to isomorphic Markov chain.The Partial correctness of the algorithm is proved by Floyd invariant assertion method.The Termination of the algorithm is proved by well-ordered set method.The algorithm is completely correct,which can be illustrated by the conclusion which is that the algorithm is partial correct and can be terminated.In order to verify the prove conclusion,the algorithm is implemented on a software platform,which is designed and developed based on Java and SQL Server.The time complexity analysis of the algorithm shows that the algorithm is effective.