{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:27:25Z","timestamp":1759638445867},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540881933"},{"type":"electronic","value":"9783540881940"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-88194-0_12","type":"book-chapter","created":{"date-parts":[[2008,10,17]],"date-time":"2008-10-17T14:56:21Z","timestamp":1224255381000},"page":"167-186","source":"Crossref","is-referenced-by-count":43,"title":["A Unified Model Checking Approach with Projection Temporal Logic"],"prefix":"10.1007","author":[{"given":"Zhenhua","family":"Duan","sequence":"first","affiliation":[]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1002\/malq.19630090502","volume":"9","author":"S.A. Kripke","year":"1963","unstructured":"Kripke, S.A.: Semantical analysis of modal logic I: normal propositional calculi. Z. Math. Logik Grund. Math.\u00a09, 67\u201396 (1963)","journal-title":"Z. Math. Logik Grund. Math."},{"key":"12_CR2","unstructured":"Duan, Z.: An Extended Interval Temporal Logic and A Framing Technique for Temporal Logic Programming. PhD thesis, University of Newcastle Upon Tyne (May 1996)"},{"key":"12_CR3","volume-title":"Temporal Logic and Temporal Logic Programming","author":"Z. Duan","year":"2006","unstructured":"Duan, Z.: Temporal Logic and Temporal Logic Programming. Science Press, Beijing (2006)"},{"key":"12_CR4","unstructured":"Moszkowski, B.: Reasoning about digital circuits. Ph.D Thesis, Department of Computer Science, Stanford University. TRSTAN-CS-83-970 (1983)"},{"issue":"1","key":"12_CR5","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":"12_CR6","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., Koutny, M.: Framed Temporal Logic Programming. Science of Computer Programming\u00a070, 31\u201361 (2008)","journal-title":"Science of Computer Programming"},{"issue":"5","key":"12_CR7","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The Model Checker Spin. IEEE Trans. on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. on Software Engineering"},{"issue":"2","key":"12_CR8","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.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation\u00a098(2), 142\u2013170 (1992)","journal-title":"Information and Computation"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Coudert, O., Madre, J.C.: A unified framework for the formal verification of sequential circuits. In: Proc. IEEE International Conference on Computer-Aided Design (1990)","DOI":"10.1109\/ICCAD.1990.129859"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579. Springer, Heidelberg (1999)"},{"key":"12_CR11","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"12_CR12","series-title":"ASI","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-642-82453-1_5","volume-title":"Logics and Models of Concurrent Systems","author":"A. Pnueli","year":"1985","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems. ASI, vol.\u00a0F 13, pp. 123\u2013144. Springer, Berlin (1985)"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/BFb0023729","volume-title":"Computer-Aided Verification","author":"A. Valmari","year":"1991","unstructured":"Valmari, A.: A stubborn attack on state explosion. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol.\u00a0531, pp. 156\u2013165. Springer, Heidelberg (1991)"},{"issue":"2","key":"12_CR14","doi-asserted-by":"publisher","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. Information and Computation\u00a0110(2), 305\u2013326 (1994)","journal-title":"Information and Computation"},{"key":"12_CR15","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/0167-6423(94)00019-0","volume":"23","author":"J. Esparza","year":"1994","unstructured":"Esparza, J.: Model checking using net unfoldings. Science of Computer Programming\u00a023, 151\u2013195 (1994)","journal-title":"Science of Computer Programming"},{"key":"12_CR16","unstructured":"Penczek, W., Gerth, R., Kuiper, R.: Partial order reductions preserving simulations (submitted for publication, 1999)"},{"issue":"3","key":"12_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. ACM Transactions on Programming Languages and Systems\u00a016(3), 843\u2013871 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/3-540-52559-9_72","volume-title":"Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness","author":"B. Josko","year":"1990","unstructured":"Josko, B.: Verifying the correctness of AADL modules using model checking. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1989. LNCS, vol.\u00a0430, pp. 386\u2013400. Springer, Heidelberg (1990)"},{"key":"12_CR19","unstructured":"Josko, B.: Modular Specification and Verification of Reactive Systems. PhD thesis, Univ. Oldenburg, Fachbereich Informatik (April 1993)"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimati, A., Clark, E.M., Strichman, O., Zhu, Y.: Bounded Model Checking. Advances in Computers \u00a058 (2003)","DOI":"10.1016\/S0065-2458(03)58003-2"},{"issue":"12","key":"12_CR21","first-page":"1035","volume":"C35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers\u00a0C35(12), 1035\u20131044 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"12_CR22","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. In: Agrawal, M., Du, D., Duan, Z., Li, A. (eds.) TAMC 2008. LNCS, vol.\u00a04978, pp. 47\u201358. Springer, Heidelberg (2008)"},{"key":"12_CR23","doi-asserted-by":"publisher","first-page":"1271","DOI":"10.1016\/j.jss.2006.12.540","volume":"80","author":"S. Liu","year":"2007","unstructured":"Liu, S., Wang, H.: An automated approach to specification animation for validation. Journal of Systems and Software\u00a080, 1271\u20131285 (2007)","journal-title":"Journal of Systems and Software"},{"key":"12_CR24","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1016\/j.jss.2007.05.036","volume":"81","author":"S. Liu","year":"2008","unstructured":"Liu, S., Chen, Y.: A relation-based method combining functional and structural testing for test case generation. Journal of Systems and Software\u00a081, 234\u2013248 (2008)","journal-title":"Journal of Systems and Software"},{"key":"12_CR25","first-page":"333","volume":"19","author":"Z. Duan","year":"2004","unstructured":"Duan, Z., Koutny, M.: A framed temporal logic programming language. Journal of Computer Science and Technology\u00a019, 333\u2013344 (2004)","journal-title":"Journal of Computer Science and Technology"},{"key":"12_CR26","first-page":"163","volume-title":"POPL 1980: Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"D. Gabbay","year":"1980","unstructured":"Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: POPL 1980: Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 163\u2013173. ACM Press, New York (1980)"},{"key":"12_CR27","volume-title":"Counter-Free Automata (M.I.T research monograph no.65)","author":"R. McNaughton","year":"1971","unstructured":"McNaughton, R., Papert, S.A.: Counter-Free Automata (M.I.T research monograph no.65). The MIT Press, Cambridge (1971)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-88194-0_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,3]],"date-time":"2019-03-03T20:04:07Z","timestamp":1551643447000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-88194-0_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540881933","9783540881940"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-88194-0_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}