{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T00:43:21Z","timestamp":1777596201255,"version":"3.51.4"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"11","license":[{"start":{"date-parts":[[2016,10,10]],"date-time":"2016-10-10T00:00:00Z","timestamp":1476057600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Sci. China Inf. Sci."],"published-print":{"date-parts":[[2016,11]]},"DOI":"10.1007\/s11432-015-0882-6","type":"journal-article","created":{"date-parts":[[2016,10,12]],"date-time":"2016-10-12T14:11:51Z","timestamp":1476281511000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":27,"title":["Model checking concurrent systems with MSVL"],"prefix":"10.1007","volume":"59","author":[{"given":"Nan","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,10,10]]},"reference":[{"key":"882_CR1","first-page":"52","volume-title":"Proceedings of the Workshop on Logic of Programs","author":"E M Clarke","year":"1981","unstructured":"Clarke E M, Emerson E A. Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proceedings of the Workshop on Logic of Programs, New York, 1981. 52\u201371"},{"key":"882_CR2","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"Proceedings of the Colloquium on International Symposium on Programming","author":"J Queille","year":"1982","unstructured":"Queille J, Sifakis J. Specification and verification of concurrent systems in CESAR. In: Proceedings of the Colloquium on International Symposium on Programming, Turin, 1982. 337\u2013351"},{"key":"882_CR3","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1145\/1592761.1592781","volume":"52","author":"E M Clarke","year":"2009","unstructured":"Clarke E M, Emerson E A, Sifakis J. Model checking: algorithmic verification and debugging. Commun ACM, 2009, 52: 74\u201384","journal-title":"Commun ACM"},{"key":"882_CR4","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/BF00709154","volume":"1","author":"A Valmari","year":"1992","unstructured":"Valmari A. A stubborn attack on state explosion. Form Method Syst Des, 1992, 1: 297\u2013322","journal-title":"Form Method Syst Des"},{"key":"882_CR5","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J R Burch","year":"1992","unstructured":"Burch J R, Clarke E M, McMillan K L, et al. Symbolic model checking: 1020 states and beyond. Inform Comput, 1992, 98: 142\u2013170","journal-title":"Inform Comput"},{"key":"882_CR6","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere A, Cimati A, Clarke E M, et al. Bounded model checking. Adv Comput, 2003, 58: 117\u2013148","journal-title":"Adv Comput"},{"key":"882_CR7","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E M Clarke","year":"1992","unstructured":"Clarke E M, Grumberg O, Long D E. Model checking and abstraction. ACM Trans Progr Lang Syst, 1992, 16: 1512\u20131542","journal-title":"ACM Trans Progr Lang Syst"},{"key":"882_CR8","doi-asserted-by":"crossref","first-page":"1206","DOI":"10.1109\/TSE.2014.2357442","volume":"40","author":"C Tian","year":"2014","unstructured":"Tian C, Duan Z H, Duan Z. Making CEGAR more efficient in software model checking. IEEE Trans Softw Eng, 2014, 40: 1206\u20131223","journal-title":"IEEE Trans Softw Eng"},{"key":"882_CR9","first-page":"167","volume-title":"Proceedings of the International Conference on Formal Engineering Methods","author":"Z H Duan","year":"2008","unstructured":"Duan Z H, Tian C. A unified model checking approach with projection temporal logic. In: Proceedings of the International Conference on Formal Engineering Methods, Kitakyushu-City, 2008. 167\u2013186"},{"key":"882_CR10","volume-title":"Temporal Logic and Temporal Logic Programming","author":"Z H Duan","year":"2005","unstructured":"Duan Z H. Temporal Logic and Temporal Logic Programming. Beijing: Science Press, 2005"},{"key":"882_CR11","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1006\/inco.1994.1035","volume":"110","author":"P Godefroid","year":"1994","unstructured":"Godefroid P, Wolper P. A partial approach to model checking. Inform Comput, 1994, 110: 305\u2013326","journal-title":"Inform Comput"},{"key":"882_CR12","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E M Clarke","year":"2003","unstructured":"Clarke E M, Grumberg O, Jha S, et al. Counterexample-guided abstraction refinement for symbolic model checking. J ACM, 2003, 50: 752\u2013794","journal-title":"J ACM"},{"key":"882_CR13","doi-asserted-by":"crossref","first-page":"544","DOI":"10.1016\/j.tcs.2015.08.039","volume":"609","author":"Z H Duan","year":"2016","unstructured":"Duan Z H, Tian C, Zhang N. A canonical form based decision procedure and model checking approach for propositional projection temporal logic. Theor Comput Sci, 2016, 609: 544\u2013560","journal-title":"Theor Comput Sci"},{"key":"882_CR14","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1016\/j.tcs.2014.02.011","volume":"554","author":"Z H Duan","year":"2014","unstructured":"Duan Z H, Tian C. A practical decision procedure for propositional projection temporal logic with infinite models. Theor Comput Sci, 2014, 554: 169\u2013190","journal-title":"Theor Comput Sci"},{"key":"882_CR15","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Proceedings of the International Conference Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening D, Tautschnig M. CBMC \u2014 C bounded model checker. In: Proceedings of the International Conference Tools and Algorithms for the Construction and Analysis of Systems, Grenoble, 2014. 389\u2013391"},{"key":"882_CR16","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Proceedings of the International SPIN Workshop on Model Checking of Software","author":"T A Henzinger","year":"2003","unstructured":"Henzinger T A, Jhala R, Majumdar R, et al. Software verification with Blast. In: Proceedings of the International SPIN Workshop on Model Checking of Software, Portland, 2003. 235\u2013239"},{"key":"882_CR17","first-page":"35","volume-title":"Proceedings of the International Conference on Formal Methods in Computer-Aided Design","author":"T Ball","year":"2010","unstructured":"Ball T, Bounimova E, Kumar R, et al. SLAM2: static driver verification with under 4% false alarms. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design, Lugano, 2010. 35\u201342"},{"key":"882_CR18","doi-asserted-by":"crossref","first-page":"1729","DOI":"10.1016\/j.tcs.2010.12.047","volume":"412","author":"C Tian","year":"2011","unstructured":"Tian C, Duan Z H. Expressiveness of propositional projection temporal logic with star. Theor Comput Sci, 2011, 412: 1729\u20131744","journal-title":"Theor Comput Sci"},{"key":"882_CR19","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0049-237X(09)70564-6","volume":"44","author":"J R B\u00a8uchi","year":"1966","unstructured":"B\u00a8uchi J R. Symposium on decision problems: on a decision method in restricted second order arithmetic. Stud Logic Found Math, 1966, 44: 1\u201311","journal-title":"Stud Logic Found Math"},{"key":"882_CR20","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/S1574-6526(07)03002-7","volume":"3","author":"C P Gomes","year":"2008","unstructured":"Gomes C P, Kautz H, Sabharwal A, et al. Satisfiability solvers. Found Artif Intell, 2008, 3: 89\u2013134","journal-title":"Found Artif Intell"},{"key":"882_CR21","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/j.scico.2007.09.001","volume":"70","author":"Z H Duan","year":"2008","unstructured":"Duan Z H, Yang X X, Koutny M. Framed temporal logic programming. Sci Comput Program, 2008, 70: 31\u201361","journal-title":"Sci Comput Program"},{"key":"882_CR22","first-page":"62","volume-title":"Proceedings of the InternationalWorkshop of Structured Object-Oriented Formal Language and Method","author":"X B Wang","year":"2013","unstructured":"Wang X B, Duan Z H, Zhao L. Formalizing and implementing types in MSVL. In: Proceedings of the InternationalWorkshop of Structured Object-Oriented Formal Language and Method, Queenstown, 2013. 62\u201375"},{"key":"882_CR23","doi-asserted-by":"crossref","unstructured":"Zhang N, Duan Z H, Tian C. A mechanism of function calls in MSVL. Theor Comput Sci, in press. doi: 10.1016\/j.tcs.2016.02.037","DOI":"10.1016\/j.tcs.2016.02.037"},{"key":"882_CR24","first-page":"306","volume-title":"Proceedings of the Symposium on Logic in Computer Science","author":"R Rosner","year":"1986","unstructured":"Rosner R, Pnueli A. A choppy logic. In: Proceedings of the Symposium on Logic in Computer Science, Cambridge, 1986. 306\u2013313"},{"key":"882_CR25","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1093\/logcom\/13.2.195","volume":"13","author":"H Bowman","year":"2003","unstructured":"Bowman H, Thompson S J. A decision procedure and complete axiomatization of finite interval temporal logic with projection. J Logic Comput, 2003, 13: 195\u2013239","journal-title":"J Logic Comput"},{"key":"882_CR26","volume-title":"Toward a Unified Logical Basis for Programming Languages","author":"C S Tang","year":"1981","unstructured":"Tang C S. Toward a Unified Logical Basis for Programming Languages. Technology Report, No. STAN-CS-81-865. 1981"},{"key":"882_CR27","volume-title":"Executing Temporal Logic Programs","author":"B C Moszkowski","year":"1986","unstructured":"Moszkowski B C. Executing Temporal Logic Programs. Cambridge: Cambridge University Press, 1986"}],"container-title":["Science China Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-015-0882-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11432-015-0882-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-015-0882-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,25]],"date-time":"2017-06-25T00:56:18Z","timestamp":1498352178000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11432-015-0882-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,10,10]]},"references-count":27,"journal-issue":{"issue":"11","published-print":{"date-parts":[[2016,11]]}},"alternative-id":["882"],"URL":"https:\/\/doi.org\/10.1007\/s11432-015-0882-6","relation":{},"ISSN":["1674-733X","1869-1919"],"issn-type":[{"value":"1674-733X","type":"print"},{"value":"1869-1919","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,10,10]]},"article-number":"118101"}}