A new model for model checking: cycle-weighted
Kripke structure

doi:10.1007/s11704-009-0066-7

Front. Comput. Sci.

2010, Vol. 4

Issue (1) : 78-88 https://doi.org/10.1007/s11704-009-0066-7

Research articles

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;

Download: PDF(179 KB)
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

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.

Keywords model checking Kripke structure weighted cycles computation tree logic (CTL)

Issue Date: 05 March 2010

Cite this article:

Jiaqi ZHU,Zhongyuan XU,Hanpin WANG, et al. A new model for model checking: cycle-weighted Kripke structure[J]. Front. Comput. Sci., 2010, 4(1): 78-88.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-009-0066-7
https://academic.hep.com.cn/fcs/EN/Y2010/V4/I1/78

	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
	Alur R, Dill D L. A theory of timed automata. Theoretical Computer Science, 1994, 126(2): 183–235 doi: 10.1016/0304-3975(94)90010-8
	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

[1]	Yuanrui ZHANG, Frédéric MALLET, Yixiang CHEN. A verification framework for spatio-temporal consistency language with CCSL as a specification language[J]. Front. Comput. Sci., 2020, 14(1): 105-129.
[2]	Kazuhiro OGATA. A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptions[J]. Front. Comput. Sci., 2019, 13(1): 51-72.
[3]	Anil Kumar KARNA, Yuting CHEN, Haibo YU, Hao ZHONG, Jianjun ZHAO. The role of model checking in software engineering[J]. Front. Comput. Sci., 2018, 12(4): 642-668.
[4]	Yu ZHOU, Nvqi ZHOU, Tingting HAN, Jiayi GU, Weigang WU. Probabilistic verification of hierarchical leader election protocol in dynamic systems[J]. Front. Comput. Sci., 2018, 12(4): 763-776.
[5]	Fei HE, Yuan GAO, Liangze YIN. Efficient software product-line model checking using induction and a SAT solver[J]. Front. Comput. Sci., 2018, 12(2): 264-279.
[6]	Laixiang SHAN,Xiaomin DU,Zheng QIN. Efficient approach of translating LTL formulae into Büchi automata[J]. Front. Comput. Sci., 2015, 9(4): 511-523.
[7]	Luxi CHEN,Linpeng HUANG,Chen LI,Tao ZAN. Integrating behavior analysis into architectural modeling[J]. Front. Comput. Sci., 2015, 9(1): 15-33.
[8]	Yuanjie SI, Jun SUN, Yang LIU, Jin Song DONG, Jun PANG, Shao Jie ZHANG, Xiaohu YANG. Model checking with fairness assumptions using PAT[J]. Front. Comput. Sci., 2014, 8(1): 1-16.
[9]	Savas KONUR. A survey on temporal logics for specifying and verifying real-time systems[J]. Front. Comput. Sci., 2013, 7(3): 370-403.
[10]	Anh Tuan LUU, Jun SUN, Yang LIU, Jin Song DONG, Xiaohong LI, Thanh Tho QUAN. SeVe: automatic tool for verification of security protocols[J]. Front Comput Sci, 2012, 6(1): 57-75.
[11]	Conghua ZHOU, Bo SUN, Zhifeng LIU. Abstraction for model checking multi-agent systems[J]. Front Comput Sci Chin, 2011, 5(1): 14-25.
[12]	Wanwei LIU, Ji WANG, Huowang CHEN, Xiaodong MA, Zhaofei WANG. symbolic model checking APSL[J]. Front Comput Sci Chin, 2009, 3(1): 130-141.

Viewed

Full text

Abstract

Cited

Shared

Discussed