{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T10:00:24Z","timestamp":1648893624919},"reference-count":11,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2010,1,13]],"date-time":"2010-01-13T00:00:00Z","timestamp":1263340800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sci. China"],"published-print":{"date-parts":[[2010,3]]},"DOI":"10.1007\/s11704-009-0066-7","type":"journal-article","created":{"date-parts":[[2010,1,13]],"date-time":"2010-01-13T02:11:55Z","timestamp":1263348715000},"page":"78-88","source":"Crossref","is-referenced-by-count":0,"title":["A new model for model checking: cycle-weighted Kripke structure"],"prefix":"10.1007","volume":"4","author":[{"given":"Jiaqi","family":"Zhu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hanpin","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhongyuan","family":"Xu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chunxiang","family":"Xu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,1,13]]},"reference":[{"key":"66_CR1","unstructured":"Clarke E M, Grumberg O, Peled D A. Model Checking. The MIT Press, 1999"},{"key":"66_CR2","first-page":"414","volume-title":"Proceedings of the 5th Annual Symposium on Logic in Computer Science (LICS\u201990)","author":"R. Alur","year":"1990","unstructured":"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\u201990). Philadelphia: IEEE Computer Society Press, 1990, 414\u2013425"},{"issue":"2","key":"66_CR3","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur R, Dill D L. A theory of timed automata. Theoretical Computer Science, 1994, 126(2): 183\u2013235","journal-title":"Theoretical Computer Science"},{"key":"66_CR4","first-page":"76","volume-title":"Proceedings of 16th Real-Time Systems Symposium","author":"K. G. Larsen","year":"1990","unstructured":"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\u201387"},{"issue":"1","key":"66_CR5","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"Alur R, Courcoubetis C, Dill D L. Model-checking in dense realtime. Information and Computation, 1993, 104(1): 2\u201334","journal-title":"Information and Computation"},{"key":"66_CR6","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1142\/9789812831583_0005","volume":"2","author":"S. Campos","year":"1995","unstructured":"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\u2013145","journal-title":"Theories and Experiences for Real-Time System Development, AMAST Series in Computing"},{"issue":"1\u20133","key":"66_CR7","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1016\/j.tcs.2005.11.020","volume":"353","author":"F. Laroussinie","year":"2006","unstructured":"Laroussinie F, Markey N, Schnoebelen P. Efficient timed model checking for discrete-time systems. Theoretical Computer Science, 2006, 353(1\u20133): 249\u2013271","journal-title":"Theoretical Computer Science"},{"issue":"1\u20133","key":"66_CR8","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/S0304-3975(02)00644-8","volume":"297","author":"F. Laroussinie","year":"2003","unstructured":"Laroussinie F, Schnoebelen Ph, Turuani M. On the expressivity and complexity of quantitaitve branching-time temporal logics. Theoretical Computer Science, 2003, 297(1\u20133): 297\u2013315","journal-title":"Theoretical Computer Science"},{"key":"66_CR9","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1007\/BF00355298","volume":"4","author":"E. A. Emerson","year":"1992","unstructured":"Emerson E A, Mok A K, Sistla A P, et al. Quantitative temporal reasoning. Real Time Systems, 1992, 4: 331\u2013352","journal-title":"Real Time Systems"},{"key":"66_CR10","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1109\/COMPSAC.2008.53","volume-title":"Proceedings of 32nd Annual International Computer Software and Applications Conference (COMPSAC 2008)","author":"J. Q. Zhu","year":"2008","unstructured":"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\u2013238"},{"key":"66_CR11","first-page":"559","volume-title":"Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001)","author":"P. K. Pandya","year":"2001","unstructured":"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\u2013573"}],"container-title":["Frontiers of Computer Science in China"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-009-0066-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11704-009-0066-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-009-0066-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T17:01:14Z","timestamp":1559408474000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11704-009-0066-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,1,13]]},"references-count":11,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,3]]}},"alternative-id":["66"],"URL":"https:\/\/doi.org\/10.1007\/s11704-009-0066-7","relation":{},"ISSN":["1673-7350","1673-7466"],"issn-type":[{"value":"1673-7350","type":"print"},{"value":"1673-7466","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,1,13]]}}}