{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T04:14:17Z","timestamp":1751688857759,"version":"3.41.0"},"publisher-location":"Singapore","reference-count":28,"publisher":"Springer Singapore","isbn-type":[{"type":"print","value":"9789811308956"},{"type":"electronic","value":"9789811308963"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-981-13-0896-3_56","type":"book-chapter","created":{"date-parts":[[2018,6,11]],"date-time":"2018-06-11T15:06:46Z","timestamp":1528729606000},"page":"563-573","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Bounded Correctness Checking for Extended CTL Properties with Past Operators"],"prefix":"10.1007","author":[{"given":"Fei","family":"Pu","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,6,12]]},"reference":[{"key":"56_CR1","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"56_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/11499107_32","volume-title":"Theory and Applications of Satisfiability Testing","author":"N Dershowitz","year":"2005","unstructured":"Dershowitz, N., Hanna, Z., Katz, J.: Bounded model checking with QBF. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 408\u2013414. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11499107_32"},{"key":"56_CR3","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimmatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117\u2013148 (2003)","journal-title":"Adv. Comput."},{"key":"56_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/11513988_10","volume-title":"Computer Aided Verification","author":"K Heljanko","year":"2005","unstructured":"Heljanko, K., Junttila, T., Latvala, T.: Incremental and Complete Bounded Model Checking for Full PLTL. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 98\u2013111. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_10"},{"key":"56_CR5","first-page":"135","volume":"51","author":"W Penczek","year":"2002","unstructured":"Penczek, W., Wozna, B., Zbrzezny, A.: Bounded model checking for the universal fragment of CTL. Fundam. Inform. 51, 135\u2013156 (2002)","journal-title":"Fundam. Inform."},{"key":"56_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/978-3-540-75596-8_29","volume-title":"Automated Technology for Verification and Analysis","author":"R Oshman","year":"2007","unstructured":"Oshman, R., Grumberg, O.: A new approach to bounded model checking for branching time logics. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 410\u2013424. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75596-8_29"},{"key":"56_CR7","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1006\/inco.1999.2817","volume":"156","author":"F Laroussinie","year":"2000","unstructured":"Laroussinie, F., Schnoebelen, P.: Specification in CTL past for verification in CTL. Inf. Comput. 156, 236\u2013263 (2000)","journal-title":"Inf. Comput."},{"key":"56_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-319-08867-9_39","volume-title":"Computer Aided Verification","author":"O Inverso","year":"2014","unstructured":"Inverso, O., Tomasco, E., Fischer, B., La Torre, S., Parlato, G.: Bounded model checking of multi-threaded C programs via lazy sequentialization. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 585\u2013602. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_39"},{"key":"56_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/3-540-36577-X_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Benedetti","year":"2003","unstructured":"Benedetti, M., Cimatti, A.: Bounded Model checking for past LTL. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 18\u201333. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_3"},{"key":"56_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-642-54862-8_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Armando","year":"2014","unstructured":"Armando, A., Carbone, R., Compagna, L.: SATMC: A SAT-based model checker for security-critical systems. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 31\u201345. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_3"},{"key":"56_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Tautschnig, M.: CBMC \u2013 C bounded model checker. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389\u2013391. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_26"},{"key":"56_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"KL McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publisher, Dordrecht (1993)"},{"key":"56_CR13","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Binary decision diagrams and beyond: enabling technologies for formal verification. In: ICCAD, pp. 236\u2013243 (1995)","DOI":"10.1109\/ICCAD.1995.480018"},{"key":"56_CR14","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.entcs.2006.12.022","volume":"174","author":"T Jussila","year":"2006","unstructured":"Jussila, T., Biere, A.: Compressing BMC encodings with QBF. Electron. Notes Theor. Comput. Sci. 174, 45\u201356 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"1","key":"56_CR15","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E Allen","year":"1986","unstructured":"Allen, E.: Sometimes and Not Never revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151\u2013178 (1986)","journal-title":"J. ACM"},{"key":"56_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-319-08587-6_16","volume-title":"Automated Reasoning","author":"W Zhang","year":"2014","unstructured":"Zhang, W.: QBF encoding of temporal properties and QBF-based verification. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 224\u2013239. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_16"},{"key":"56_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2014.10.026","volume":"564","author":"W Zhang","year":"2015","unstructured":"Zhang, W., Smentics, B.: Theor. Comput. Sci. 564, 1\u201329 (2015)","journal-title":"Theor. Comput. Sci."},{"key":"56_CR18","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1016\/j.ipl.2017.06.008","volume":"127","author":"X Zhaowei","year":"2017","unstructured":"Zhaowei, X., Zhang, W.: Linear templates of ACTL formulas with an application to SAT-based verification. Inf. Process. Lett. 127, 6\u201316 (2017)","journal-title":"Inf. Process. Lett."},{"key":"56_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-642-10373-5_15","volume-title":"Formal Methods and Software Engineering","author":"W Zhang","year":"2009","unstructured":"Zhang, W.: Bounded semantics of CTL and SAT-based verification. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 286\u2013305. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-10373-5_15"},{"key":"56_CR20","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/s10009-004-0182-5","volume":"7","author":"E Clarke","year":"2005","unstructured":"Clarke, E., Kroening, D., Ouaknine, J., Strichman, O.: Computational challenges in bounded model checking. Int. J. Softw. Tools Technol. Transfer 7, 174\u2013183 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"56_CR21","doi-asserted-by":"crossref","unstructured":"Ganai, M.K., Gupta, A.: Accelerating high-level bounded model checking. In: ICCAD, pp. 794\u2013801 (2006)","DOI":"10.1109\/ICCAD.2006.320122"},{"key":"56_CR22","doi-asserted-by":"crossref","first-page":"65","DOI":"10.3233\/FUN-2004-63104","volume":"63","author":"B Wozna","year":"2004","unstructured":"Wozna, B.: ATCL* properties and bounded model checking. Fundam. Inform. 63, 65\u201387 (2004)","journal-title":"Fundam. Inform."},{"key":"56_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-30494-4_18","volume-title":"Formal Methods in Computer-Aided Design","author":"A Cimatti","year":"2004","unstructured":"Cimatti, A., Roveri, M., Sheridan, D.: Bounded verification of past LTL. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 245\u2013259. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30494-4_18"},{"key":"56_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-319-21401-6_20","volume-title":"Automated Deduction \u2013 CADE-25","author":"K Ji","year":"2015","unstructured":"Ji, K.: CTL model checking in deduction modulo. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 295\u2013310. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_20"},{"issue":"7\u20138","key":"56_CR25","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1016\/j.scico.2011.02.003","volume":"77","author":"S Kemper","year":"2012","unstructured":"Kemper, S.: SAT-based verification for timed component connectors. Sci. Comput. Program. 77(7\u20138), 779\u2013798 (2012)","journal-title":"Sci. Comput. Program."},{"key":"56_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/978-3-540-93900-9_29","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Wimmer","year":"2008","unstructured":"Wimmer, R., Braitling, B., Becker, B.: Counterexample generation for discrete-time markov chains using bounded model checking. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 366\u2013380. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-93900-9_29"},{"key":"56_CR27","unstructured":"Gomes, C., Selman, B., Kautz, H.: SAT encodings of state-space reachability problems in numeric domains. In: IJCAI, pp. 1918\u20131923 (2007)"},{"key":"56_CR28","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-73595-3_24","volume-title":"Automated Deduction \u2013 CADE-21","author":"JA Navarro-P\u00e9rez","year":"2007","unstructured":"Navarro-P\u00e9rez, J.A., Voronkov, A.: Encodings of bounded LTL model checking in effectively propositional logic. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 346\u2013361. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_24"}],"container-title":["Communications in Computer and Information Science","Geo-Spatial Knowledge and Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-13-0896-3_56","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T02:21:35Z","timestamp":1751682095000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-981-13-0896-3_56"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9789811308956","9789811308963"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-981-13-0896-3_56","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"GSKI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Geo-Spatial Knowledge and Intelligence","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Chiang Mai","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Thailand","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 December 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 December 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"gski2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.grmse2017.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}