{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:12:59Z","timestamp":1759637579708},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642387678"},{"type":"electronic","value":"9783642387685"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38768-5_52","type":"book-chapter","created":{"date-parts":[[2013,5,17]],"date-time":"2013-05-17T00:31:28Z","timestamp":1368750688000},"page":"591-602","source":"Crossref","is-referenced-by-count":6,"title":["Bounded Model Checking for Propositional Projection Temporal Logic"],"prefix":"10.1007","author":[{"given":"Zhenhua","family":"Duan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mengfei","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jia","family":"He","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"52_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"52_CR2","first-page":"46","volume-title":"Proceedings of the 18th IEEE Symposium on Foundations of Computer Science","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The Temporal Logic of Programs. In: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46\u201367. IEEE, New York (1977)"},{"key":"52_CR3","series-title":"Advances in Computers","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume-title":"Bounded Model checking","author":"A. Biere","year":"2003","unstructured":"Biere, A., Clarke, E., et al.: Bounded Model checking. Advances in Computers, vol.\u00a058, pp. 117\u2013148. Academic Press, London (2003)"},{"issue":"1","key":"52_CR4","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/321738.321743","volume":"20","author":"C.L. Liu","year":"1973","unstructured":"Liu, C.L., Layland, J.W.: Scheduling algorithm for multiprogramming in a hard real-time environment. Journal of the ACM\u00a020(1), 46\u201361 (1973)","journal-title":"Journal of the ACM"},{"key":"52_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-540-76650-6_15","volume-title":"Formal Methods and Software Engineering","author":"C. Tian","year":"2007","unstructured":"Tian, C., Duan, Z.: Model Checking Propositional Projection Temporal Logic based on SPIN. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds.) ICFEM 2007. LNCS, vol.\u00a04789, pp. 246\u2013265. Springer, Heidelberg (2007)"},{"issue":"2","key":"52_CR6","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., et al.: Computational Challenges in Bounded Model Checking. International Journal on Software Tools for Technology Transfer\u00a07(2), 174\u2013183 (2005)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"52_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E. Clark","year":"1982","unstructured":"Clark, E., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"52_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/3-540-44585-4_43","volume-title":"Computer Aided Verification","author":"F. Copty","year":"2001","unstructured":"Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.Y.: Benefits of Bounded Model Checking at an Industrial Setting. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 436\u2013453. Springer, Heidelberg (2001)"},{"key":"52_CR9","unstructured":"Holzmann, G.J.: SPIN Model Checker: The Primer and Reference Manual (September 4, 2003)"},{"key":"52_CR10","unstructured":"http:\/\/www.cs.cmu.edu\/~modelcheck\/bmc.html"},{"key":"52_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J.P. Quielle","year":"1982","unstructured":"Quielle, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137, pp. 337\u2013351. Springer, Heidelberg (1982)"},{"issue":"2","key":"52_CR12","doi-asserted-by":"publisher","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., McMillan, K.L., Dill, D.L., Hwang, J.: Symbolic Model Checking: 1020 States and Beyond. Information and Computation\u00a098(2), 142\u2013170 (1992)","journal-title":"Information and Computation"},{"key":"52_CR13","unstructured":"McMillian, K.L.: Symbolic Model Checking. Kluwer Academic Publishers (1993) ISBN: 0-7923-9380-5"},{"key":"52_CR14","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Communications of the ACM\u00a05, 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"52_CR15","unstructured":"Huth, M., Ryan, M.: Logic in Computer Science: Modeling and Reasoning about Systems, 2nd edn., Part 3. China Machine Press (2007) ISBN:978-7-111-21397-0"},{"key":"52_CR16","unstructured":"Moszkowski, B.: Reasoning about digital circuits. Ph.D. Thesis. Stanford University, Stanford (1983)"},{"issue":"3","key":"52_CR17","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. Journal ACM Transactions on Programming Languages and Systems TOPLAS Homepage Archive\u00a016(3), 843\u2013871 (1994)","journal-title":"Journal ACM Transactions on Programming Languages and Systems TOPLAS Homepage Archive"},{"key":"52_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-540-79228-4_4","volume-title":"Theory and Applications of Models of Computation","author":"C. Tian","year":"2008","unstructured":"Tian, C., Duan, Z.: Propositional projection temporal logic, B\u03c9chi automata and \u03c9-regular expressions. In: Agrawal, M., et al. (eds.) TAMC 2008. LNCS, vol.\u00a04978, pp. 47\u201358. Springer, Heidelberg (2008)"},{"key":"52_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.\u00a05885, pp. 286\u2013305. Springer, Heidelberg (2009)"},{"key":"52_CR20","unstructured":"http:\/\/www.cs.cmu.edu\/~modelcheck\/bmc.html"},{"key":"52_CR21","unstructured":"Duan, Z.: An Extended Interval Temporal Logic and a Framing Technique for Temporal Logic Programming. Ph.D. Thesis, University of Newcastle upon Tyne (May 1996)"},{"issue":"1","key":"52_CR22","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s00236-007-0062-z","volume":"45","author":"Z. Duan","year":"2008","unstructured":"Duan, Z., Tian, C., Zhang, L.: A Decision Procedure for Propositional Projection Temporal Logic with Infinite Models. Acta Informatica\u00a045(1), 43\u201378 (2008)","journal-title":"Acta Informatica"},{"key":"52_CR23","unstructured":"Duan, Z., Zhang, L.: A Decision Procedure for Propositional Projection Temporal Logic. Technical Report No.1, Institute of Computing Theory and Technology, Xidian University, Xi\u2019an P.R.China (2005)"},{"issue":"1","key":"52_CR24","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/j.scico.2007.09.001","volume":"70","author":"Z. Duan","year":"2008","unstructured":"Duan, Z., Yang, X., Kounty, M.: Framed Temporal Logic Programming. Science of Computer Programming\u00a070(1), 31\u201361 (2008)","journal-title":"Science of Computer Programming"}],"container-title":["Lecture Notes in Computer Science","Computing and Combinatorics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38768-5_52","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,12]],"date-time":"2019-05-12T22:13:14Z","timestamp":1557699194000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38768-5_52"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642387678","9783642387685"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38768-5_52","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}