{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,2]],"date-time":"2025-07-02T11:47:46Z","timestamp":1751456866722},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540766483"},{"type":"electronic","value":"9783540766506"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-76650-6_15","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T07:12:49Z","timestamp":1193382769000},"page":"246-265","source":"Crossref","is-referenced-by-count":15,"title":["Model Checking Propositional Projection Temporal Logic Based on SPIN"],"prefix":"10.1007","author":[{"given":"Cong","family":"Tian","sequence":"first","affiliation":[]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_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":"15_CR2","first-page":"306","volume-title":"LICS","author":"R. Rosner","year":"1986","unstructured":"Rosner, R., Pnueli, A.: A choppy logic. In: LICS, pp. 306\u2013314. IEEE Computer Society Press, Los Alamitos (1986)"},{"key":"15_CR3","unstructured":"Moszkowski, B.: Reasoning about digital circuits. Ph.D Thesis, Department of Computer Science, Stanford University. TRSTAN-CS-83-970 (1983)"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-45022-X_19","volume-title":"Automata, Languages and Programming","author":"B. Moszkowski","year":"2000","unstructured":"Moszkowski, B.: An Automata-Theoretic Completeness Proof for Interval Temporal Logic. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol.\u00a01853, pp. 223\u2013234. Springer, Heidelberg (2000)"},{"issue":"5","key":"15_CR5","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"C. Zhou","year":"1991","unstructured":"Zhou, C., Hoare, C.A.R., Ravn, A.P.: A calculus of duration. Information Processing Letters\u00a040(5), 269\u2013275 (1991)","journal-title":"Information Processing Letters"},{"key":"15_CR6","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":"15_CR7","volume-title":"Temporal Logic and Temporal Logic Programming","author":"Z. Duan","year":"2006","unstructured":"Duan, Z.: Temporal Logic and Temporal Logic Programming. Science Press, China (2006)"},{"key":"15_CR8","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), \n                    \n                      http:\/\/www.paper.edu.cn\/process\/download.jsp?file=200611-427"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1007\/978-3-540-72504-6_47","volume-title":"TAMC 2007","author":"Z. Duan","year":"2007","unstructured":"Duan, Z., Tian, C.: Decidability of Propositional Projection Temporal Logic with Infinite Models. In: TAMC 2007. LNCS, vol.\u00a04484, pp. 521\u2013532. Springer, Heidelberg (2007)"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/11562931_27","volume-title":"Logic Programming","author":"Z. Duan","year":"2005","unstructured":"Duan, Z., Yang, X., Koutny, M.: Semantics of Framed Temporal Logic Programs. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol.\u00a03668, pp. 256\u2013270. Springer, Heidelberg (2005)"},{"key":"15_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The temporal logic of reactive and concurrent systems","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems. Springer, Heidelberg (1992)"},{"key":"15_CR12","volume-title":"Introduction to Automata Theory, Languages and Computation","author":"J. Hopcroft","year":"2001","unstructured":"Hopcroft, J., Motwani, R., Ullman, J.: Introduction to Automata Theory, Languages and Computation, 2nd edn. Addison-Wesley, Reading (2001)","edition":"2"},{"key":"15_CR13","first-page":"332","volume-title":"LICS 1986","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS 1986, pp. 332\u2013344. IEEE CS Press, Los Alamitos (1986)"},{"key":"15_CR14","first-page":"36","volume-title":"Proc. 10th LICS","author":"B. Dutertre","year":"1995","unstructured":"Dutertre, B.: Complete proof systems for first order interval temporal logic. In: Proc. 10th LICS, pp. 36\u201343. IEEE Computer Soc. Press, Los Alamitos (1995)"},{"issue":"5","key":"15_CR15","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"},{"key":"15_CR16","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. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schroeder public key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol.\u00a01055, pp. 147\u2013166. Springer, Heidelberg (1996)"},{"issue":"12","key":"15_CR18","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"R. Needham","year":"1978","unstructured":"Needham, R., Schroeder, M.: Using encryption for authentication in large networks of computers. Communications of the ACM\u00a021(12), 993\u2013999 (1978)","journal-title":"Communications of the ACM"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/3-540-45510-8_1","volume-title":"MOVEP 2000","author":"S. Merz","year":"2001","unstructured":"Merz, S.: Model Checking: A Tutorial Overview. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol.\u00a02067, pp. 3\u201338. Springer, Heidelberg (2001)"},{"key":"15_CR20","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P.L. Wolper","year":"1983","unstructured":"Wolper, P.L.: Temporal logic can be more expressive. Information and Control\u00a056, 72\u201399 (1983)","journal-title":"Information and Control"}],"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-76650-6_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:57:14Z","timestamp":1619521034000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-76650-6_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540766483","9783540766506"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-76650-6_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}