A new model for model checking: cycle-weighted Kripke structure. (English) Zbl 1267.68148
Summary: 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.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
References:
| [1] | Clarke E M, Grumberg O, Peled D A. Model Checking. The MIT Press, 1999 |
| [2] | Alur R, Courcoubetis C, Dill D L. Model-checking for real-time systems. In: Proceedings of the 5th Annual Symposium on Logic in Computer Science (LICS’90). Philadelphia: IEEE Computer Society Press, 1990, 414–425 · Zbl 0769.68088 |
| [3] | Alur R, Dill D L. A theory of timed automata. Theoretical Computer Science, 1994, 126(2): 183–235 · Zbl 0803.68071 · doi:10.1016/0304-3975(94)90010-8 |
| [4] | Larsen K G, Pettersson P, Yi W. Compositional and symbolic model-checking of real-time systems. In: Proceedings of 16th Real-Time Systems Symposium. Pisa: IEEE Computer Society Press, 1990, 76–87 |
| [5] | Alur R, Courcoubetis C, Dill D L. Model-checking in dense realtime. Information and Computation, 1993, 104(1): 2–34 · Zbl 0783.68076 · doi:10.1006/inco.1993.1024 |
| [6] | Campos S, Clarke E M. Real-time symbolic model checking for discrete time models. Theories and Experiences for Real-Time System Development, AMAST Series in Computing, 1995, 2: 129–145 · doi:10.1142/9789812831583_0005 |
| [7] | Laroussinie F, Markey N, Schnoebelen P. Efficient timed model checking for discrete-time systems. Theoretical Computer Science, 2006, 353(1–3): 249–271 · Zbl 1088.68107 · doi:10.1016/j.tcs.2005.11.020 |
| [8] | Laroussinie F, Schnoebelen Ph, Turuani M. On the expressivity and complexity of quantitaitve branching-time temporal logics. Theoretical Computer Science, 2003, 297(1–3): 297–315 · Zbl 1019.03012 · doi:10.1016/S0304-3975(02)00644-8 |
| [9] | Emerson E A, Mok A K, Sistla A P, et al. Quantitative temporal reasoning. Real Time Systems, 1992, 4: 331–352 · Zbl 0765.68121 · doi:10.1007/BF00355298 |
| [10] | 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 Computer Software and Applications Conference (COMPSAC 2008). Turku: IEEE Computer Society Press, 2008, 235–238 |
| [11] | Pandya P K. Model checking CTL*[DC]. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001). Genova: Springer, 2001, 559–573 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
