Model Checking of Variable Petri Nets by Using the Kripke Structure
提出将可变Petri网转换为Kripke结构的算法，并基于此对系统动态交互属性进行模型检验，适用于移动交互系统的行为分析。
The properties of dynamic interactions in mobile-interactive systems are still difficult to analyze because of the complexity of systems. Thus, we have proposed a new Petri net called the variable petri net (VPN) recently, which specializes in describing dynamic interactions in systems. To make better use of VPN, this article focuses on the model checking method of VPN. It introduces the algorithm to transform a VPN to a Kripke structure that can describe both the system running states and the system connection states in VPN, and the method to transform a property to a temporal logic formula based on VPN and its Kripke structure. The Kripke structure can be optimized by considering the specific property about the system connection states and then be used to perform the targeted verification to the property by using a model checker. A practical example is given to demonstrate the proposed methods.