A new model for model checking: cycle-weighted
Kripke structure
A new model for model checking: cycle-weighted
Kripke structure
Jiaqi ZHU,Hanpin WANG,Zhongyuan XU,Chunxiang XU,
Key Laboratory of
High Confidence Software Technologies, Ministry of Education, School
of Electronic Engineering and Computer Science, Peking University,
Beijing 100871, China;
Abstract：This paper proposes a new model, named cycle-weighted Kripke structure (CWKS), based on the traditional Kripke structure. It adds two integer weights to some transitions of the Kripke structure, restricting when these transitions can occur. These weights mainly specify the occurrences of some cycles in a Kripke structure, giving a range of how many times these cycles may be executed repeatedly. This new model can efficiently describe some quantitative discrete-time characters of reactive and concurrent systems, so it is significant for some model checking problems. We also define a subset of CWKS, named conditional CWKS, which satisfies a constraint referring to the weighted transitions in the structure. The paper modifies the explicit computation tree logic (CTL) model checking algorithm to accommodate the conditional CWKS. It can also be regarded as the foundation of some more complex models obtained by extending from the Kripke structure, which will be studied in the future.
. A new model for model checking: cycle-weighted
Kripke structure[J]. Front. Comput. Sci., 2010, 4(1): 78-88.
Jiaqi ZHU, Hanpin WANG, Zhongyuan XU, Chunxiang XU, . A new model for model checking: cycle-weighted
Kripke structure. Front. Comput. Sci., 2010, 4(1): 78-88.
Clarke E M, Grumberg O, Peled D A. Model Checking. The MIT Press, 1999
Alur R, Courcoubetis C, Dill D L. Model-checking for real-time systems. In: Proceedings of the 5th Annual Symposium on Logic in ComputerScience (LICS’90). Philadelphia: IEEE Computer Society Press, 1990, 414–425
Larsen K G, Pettersson P, Yi W. Compositional and symbolic model-checking of real-timesystems. In: Proceedings of 16th Real-TimeSystems Symposium. Pisa: IEEE Computer Society Press, 1990, 76–87
Alur R, Courcoubetis C, Dill D L. Model- checking in dense real-time. Information and Computation, 1993, 104(1): 2–34 doi: 10.1006/inco.1993.1024
Campos S, Clarke E M. Real-time symbolic modelchecking for discrete time models. Theoriesand Experiences for Real-Time System Development, AMAST Series inComputing, 1995, 2: 129–145
Laroussinie F, Markey N, Schnoebelen P. Efficient timed model checking for discrete-time systems. Theoretical Computer Science, 2006, 353(1―3): 249–271 doi: 10.1016/j.tcs.2005.11.020
Laroussinie F, Schnoebelen Ph, Turuani M. On the expressivity and complexity of quantitaitve branching-timetemporal logics. Theoretical Computer Science, 2003, 297(1―3): 297–315 doi: 10.1016/S0304-3975(02)00644-8
Emerson E A, Mok A K, Sistla A P, et al. Quantitative temporal reasoning. Real Time Systems, 1992, 4: 331–352 doi: 10.1007/BF00355298
Zhu J Q, Wang H P, Xu Z Y. A new temporal logic CTL[k-QDDC] and its verification. In: Proceedings of 32nd Annual International ComputerSoftware and Applications Conference (COMPSAC 2008). Turku: IEEEComputer Society Press, 2008, 235–238
Pandya P K. Model checking CTL*[DC]. In: Proceedingsof Tools and Algorithms for the Construction and Analysis of Systems(TACAS 2001). Genova: Springer, 2001, 559–573
