{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,29]],"date-time":"2025-06-29T08:40:06Z","timestamp":1751186406154,"version":"3.41.0"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2017,12,26]],"date-time":"2017-12-26T00:00:00Z","timestamp":1514246400000},"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":[[2018,5]]},"DOI":"10.1007\/s11432-017-9152-x","type":"journal-article","created":{"date-parts":[[2017,12,28]],"date-time":"2017-12-28T11:14:04Z","timestamp":1514459644000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Symbolic model checking for discrete real-time systems"],"prefix":"10.1007","volume":"61","author":[{"given":"Xiangyu","family":"Luo","sequence":"first","affiliation":[]},{"given":"Lijun","family":"Wu","sequence":"additional","affiliation":[]},{"given":"Qingliang","family":"Chen","sequence":"additional","affiliation":[]},{"given":"Haibo","family":"Li","sequence":"additional","affiliation":[]},{"given":"Lixiao","family":"Zheng","sequence":"additional","affiliation":[]},{"given":"Zuxi","family":"Chen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,12,26]]},"reference":[{"key":"9152_CR1","volume-title":"Model Checking","author":"E M Clarke","year":"2000","unstructured":"Clarke E M, Grumberg O, Peled D A. Model Checking. London: The MIT Press, 2000"},{"key":"9152_CR2","volume-title":"The Stanford Encyclopedia of Philosophy","author":"V Goranko","year":"2015","unstructured":"Goranko V, Galton A. Temporal logic. In: The Stanford Encyclopedia of Philosophy. San Francisco: Metaphysics Research Lab, Stanford University, 2015"},{"key":"9152_CR3","volume-title":"The^SPIN Model Checker-Primer and Reference Manual","author":"G J Holzmann","year":"2004","unstructured":"Holzmann G J. The SPIN Model Checker-Primer and Reference Manual. Boston: Addison-Wesley, 2004"},{"key":"9152_CR4","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Proceedings of the 14th International Conference on Computer Aided Verification (CAV 2002)","author":"A Cimatti","year":"2002","unstructured":"Cimatti A, Clarke E M, Giunchiglia E, et al. Nusmv 2: an opensource tool for symbolic model checking. In: Proceedings of the 14th International Conference on Computer Aided Verification (CAV 2002). Berlin: Springer, 2002. 359\u2013364"},{"key":"9152_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K L McMillan","year":"1993","unstructured":"McMillan K L. Symbolic Model Checking. Norwell: Kluwer Academic Publisher, 1993"},{"key":"9152_CR6","first-page":"171","volume-title":"Proceedings of the 22th International Conference on Computer Aided Verification (CAV 2010)","author":"A Pnueli","year":"2010","unstructured":"Pnueli A, Sa\u2019ar Y, Zuck L D. Jtlv: a framework for developing verification algorithms. In: Proceedings of the 22th International Conference on Computer Aided Verification (CAV 2010). Berlin: Springer, 2010. 171\u2013174"},{"key":"9152_CR7","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1093\/comjnl\/bxm009","volume":"50","author":"K L Su","year":"2007","unstructured":"Su K L, Sattar A, Luo X Y. Model checking temporal logics of knowledge via OBDDs. Comput J, 2007, 50: 403\u2013420","journal-title":"Comput J"},{"key":"9152_CR8","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K G Larsen","year":"1997","unstructured":"Larsen K G, Pettersson P, Wang Y. UPPAAL in a nutshell. Int J Softw Tools Tech Transfer, 1997, 1: 134\u2013152","journal-title":"Int^J Softw Tools Tech Transfer"},{"key":"9152_CR9","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T A Henzinger","year":"1997","unstructured":"Henzinger T A, Ho P-H, Howard W-T. HYTECH: a model checker for hybrid systems. Int J Softw Tools Tech Transfer, 1997, 1: 110\u2013122","journal-title":"Int^J Softw Tools Tech Transfer"},{"key":"9152_CR10","doi-asserted-by":"crossref","first-page":"546","DOI":"10.1007\/BFb0028779","volume-title":"Proceedings of the 10th International Conference on Computer Aided Verification (CAV 1998)","author":"M Bozga","year":"1998","unstructured":"Bozga M, Daws C, Maler O, et al. Kronos: a model-checking tool for real-time systems. In: Proceedings of the 10th International Conference on Computer Aided Verification (CAV 1998). London: Springer-Verlag, 1998. 546\u2013550"},{"key":"9152_CR11","doi-asserted-by":"crossref","first-page":"248","DOI":"10.1016\/j.scico.2015.08.002","volume":"111","author":"M Georges","year":"2015","unstructured":"Georges M, Christoph S. Fully symbolic TCTL model checking for complete and incomplete real-time systems. Sci Comput Program, 2015, 111: 248\u2013276","journal-title":"Sci Comput Program"},{"key":"9152_CR12","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. Model-checking in dense real-time. Inf Comput, 1993, 104: 2\u201334","journal-title":"Inf Comput"},{"key":"9152_CR13","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1006\/inco.1993.1025","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur R, Henzinger T A. Real-time logics: complexity and expressiveness. Inf Comput, 1993, 104: 35\u201377","journal-title":"Inf Comput"},{"key":"9152_CR14","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R Alur","year":"1994","unstructured":"Alur R, Henzinger T A. A really temporal logic. J ACM, 1994, 41: 181\u2013204","journal-title":"J ACM"},{"key":"9152_CR15","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R Alur","year":"1996","unstructured":"Alur R, Feder T, Henzinger T A. The benefits of relaxing punctuality. J ACM, 1996, 43: 116\u2013146","journal-title":"J ACM"},{"key":"9152_CR16","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1016\/S1567-8326(02)00022-X","volume":"52","author":"L Aceto","year":"2002","unstructured":"Aceto L, Laroussinie F. Is your model checker on time? On the complexity of model checking for timed modal logics. J Log Algebr Program, 2002, 52: 7\u201351","journal-title":"J Log Algebr Program"},{"key":"9152_CR17","volume-title":"Handbook of Model Checking","author":"P Bouyer","year":"2017","unstructured":"Bouyer P, Fahrenberg U, Larsen K G, et al. Model checking real-time systems. In: Handbook of Model Checking. Berlin: Springer-Verlag, 2017"},{"key":"9152_CR18","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/s10009-015-0378-x","volume":"19","author":"A Lomuscio","year":"2017","unstructured":"Lomuscio A, Qu H Y, Raimondi F. MCMAS: an open-source model checker for the verification of multi-agent systems. Int J Softw Tools Tech Transfer, 2017, 19: 9\u201330","journal-title":"Int^J Softw Tools Tech Transfer"},{"key":"9152_CR19","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R E Bryant","year":"1992","unstructured":"Bryant R E. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput Surv, 1992, 24: 293\u2013318","journal-title":"ACM Comput Surv"},{"key":"9152_CR20","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 Syst, 1992, 4: 331\u2013352","journal-title":"Real-Time Syst"},{"key":"9152_CR21","volume-title":"Formal verification of embedded real-time systems","author":"M Fruth","year":"2005","unstructured":"Fruth M. Formal verification of embedded real-time systems. Dissertation for Ph.D. Degree. Dresden: TU Dresden, 2005"},{"key":"9152_CR22","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/978-3-540-69850-0_11","volume-title":"25 Years of Model Checking:^History, Achievements, Perspectives","author":"A Pnueli","year":"2008","unstructured":"Pnueli A, Zaks A. On the merits of temporal testers. In: 25 Years of Model Checking: History, Achievements, Perspectives. Berlin: Springer, 2008. 172\u2013195"},{"key":"9152_CR23","first-page":"30","volume-title":"Proceedings of the 27th International Conference on Computer Aided Verification (CAV 2015)","author":"B Finkbeiner","year":"2015","unstructured":"Finkbeiner B, Rabe M N, S\u00b4anchez C. Algorithms for model checking HyperLTL and HyperCTL*. In: Proceedings of the 27th International Conference on Computer Aided Verification (CAV 2015). Berlin: Springer, 2015. 30\u201348"},{"key":"9152_CR24","doi-asserted-by":"crossref","first-page":"424","DOI":"10.1007\/978-3-319-08867-9_28","volume-title":"Proceedings of the 27th International Conference on Computer Aided Verification (CAV 2014)","author":"A Cimatti","year":"2014","unstructured":"Cimatti A, Griggio A, Mover S, et al. Verifying LTL properties of hybrid systems with k-liveness. In: Proceedings of the 27th International Conference on Computer Aided Verification (CAV 2014). Berlin: Springer, 2014. 424\u2013440"},{"key":"9152_CR25","first-page":"13","volume-title":"Proceedings of the 27th International Conference on Computer Aided Verification (CAV 2015)","author":"B Cook","year":"2015","unstructured":"Cook B, Khlaaf H, Piterman N. On automation of CTL* verification for infinite-state systems. In: Proceedings of the 27th International Conference on Computer Aided Verification (CAV 2015). Berlin: Springer, 2015. 13\u201329."},{"key":"9152_CR26","doi-asserted-by":"crossref","first-page":"118101","DOI":"10.1007\/s11432-015-0882-6","volume":"59","author":"N Zhang","year":"2016","unstructured":"Zhang N, Duan Z H, Tian C. Model checking concurrent systems with MSVL. Sci China Inf Sci, 2016, 59: 118101","journal-title":"Sci China Inf Sci"},{"key":"9152_CR27","first-page":"37","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015)","author":"F Immler","year":"2015","unstructured":"Immler F. Verified reachability analysis of continuous systems. In: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015). Berlin: Springer, 2015. 37\u201351"},{"key":"9152_CR28","first-page":"052101","volume":"57","author":"W Lin","year":"2014","unstructured":"Lin W, Wu M, Yang Z F, et al. Exact safety verification of hybrid systems using sums-of-squares representation. Sci China Inf Sci, 2014, 57: 052101","journal-title":"Sci China Inf Sci"}],"container-title":["Science China Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-017-9152-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11432-017-9152-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-017-9152-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,29]],"date-time":"2025-06-29T08:26:24Z","timestamp":1751185584000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11432-017-9152-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,26]]},"references-count":28,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2018,5]]}},"alternative-id":["9152"],"URL":"https:\/\/doi.org\/10.1007\/s11432-017-9152-x","relation":{},"ISSN":["1674-733X","1869-1919"],"issn-type":[{"type":"print","value":"1674-733X"},{"type":"electronic","value":"1869-1919"}],"subject":[],"published":{"date-parts":[[2017,12,26]]},"article-number":"052106"}}