{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:20:26Z","timestamp":1725571226275},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642174605"},{"type":"electronic","value":"9783642174612"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-17461-2_30","type":"book-chapter","created":{"date-parts":[[2010,12,15]],"date-time":"2010-12-15T04:53:59Z","timestamp":1292388839000},"page":"374-386","source":"Crossref","is-referenced-by-count":0,"title":["A Transformation from PPTL to S1S"],"prefix":"10.1007","author":[{"given":"Cong","family":"Tian","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"30_CR1","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.2. IEEE, New York (1977)"},{"key":"30_CR2","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":"30_CR3","unstructured":"Rosner, R., Pnueli, A.: A choppy logic. In: First Annual IEEE Symposium on Logic In Computer Science, LICS, pp. 306\u2013314 (1986)"},{"key":"30_CR4","unstructured":"Moszkowski, B.: Reasoning about digital circuits. Ph.D Thesis, Department of Computer Science, Stanford University. TRSTAN-CS-83-970 (1983)"},{"key":"30_CR5","first-page":"238","volume-title":"Proceeding of the First IEEE Int\u2019l Conf. on Enginneering of Complex Computer Systems (ICECCS 1995)","author":"B.C. Moszkowski","year":"1995","unstructured":"Moszkowski, B.C.: Compositional reasoning about projected and infinite time. In: Proceeding of the First IEEE Int\u2019l Conf. on Enginneering of Complex Computer Systems (ICECCS 1995), pp. 238\u2013245. IEEE Computer Society Press, Los Alamitos (1995)"},{"key":"30_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)"},{"issue":"1","key":"30_CR7","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":"30_CR8","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)"},{"key":"30_CR9","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"},{"issue":"5","key":"30_CR10","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":"30_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/3-540-58216-9_48","volume-title":"Logic Programming and Automated Reasoning","author":"Z. Duan","year":"1994","unstructured":"Duan, Z., Koutny, M., Holt, C.: Projection in temporal logic programming. In: Pfenning, F. (ed.) LPAR 1994. LNCS, vol.\u00a0822, pp. 333\u2013344. Springer, Heidelberg (1994)"},{"issue":"2","key":"30_CR12","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1093\/logcom\/13.2.195","volume":"13","author":"H. Bowman","year":"2003","unstructured":"Bowman, H., Thompson, S.: A decision procedure and complete axiomatization of interval temporal logic with projection. Journal of logic and Computation\u00a013(2), 195\u2013239 (2003)","journal-title":"Journal of logic and Computation"},{"issue":"1","key":"30_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M. Vardi","year":"1994","unstructured":"Vardi, M., Wolper, P.: Reasoning about infinite computations. Information and Computation\u00a0115(1), 1\u201337 (1994)","journal-title":"Information and Computation"},{"key":"30_CR14","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56922-7_9","volume-title":"Computer Aided Verification","author":"Y. Kesten","year":"1993","unstructured":"Kesten, Y., Manna, Z., McGuire, H., Pnueli, A.: A decision algorithm for full propositional temporal logic. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, Springer, Heidelberg (1993)"},{"key":"30_CR15","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/3-540-58976-7_3","volume-title":"Executable Modal and Temporal Logics","author":"S. Kono","year":"1995","unstructured":"Kono, S.: A combination of clausal and non-clausal temporal logic programs. In: Fisher, M., Owens, R. (eds.) IJCAI-WS 1993. LNCS (LNAI), vol.\u00a0897, pp. 40\u201357. Springer, Heidelberg (1995)"},{"key":"30_CR16","unstructured":"Gomez, R., Bowman, H.: A MONA-based Decision Procedure for Propositional Interval Temporal Logic. In: Workshop of Interval Temporal Logics and Duration Calculi (part of the 15th European Summer School in Logic, Language and Information (August 2003)"},{"key":"30_CR17","first-page":"1","volume-title":"Proceedings of the 1960 International Congress on Logic, Methodology and Philosophy of Science","author":"J.R. B\u00fcchi","year":"1960","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Nagel, E. (ed.) Proceedings of the 1960 International Congress on Logic, Methodology and Philosophy of Science, pp. 1\u201312. Stanford University Press, Stanford (1960)"},{"key":"30_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-540-70918-3_2","volume-title":"STACS 2007","author":"M.Y. Vardi","year":"2007","unstructured":"Vardi, M.Y.: The B\u00fcchi Complementation Saga. In: Thomas, W., Weil, P. (eds.) STACS 2007. LNCS, vol.\u00a04393, pp. 12\u201322. Springer, Heidelberg (2007)"},{"key":"30_CR19","first-page":"163","volume-title":"Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1980","author":"D. Gabbay","year":"1980","unstructured":"Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1980, pp. 163\u2013173. ACM Press, New York (1980)"},{"key":"30_CR20","series-title":"M.I.T research monograph","volume-title":"Counter-Free Automata","author":"R. McNaughton","year":"1971","unstructured":"McNaughton, R., Papert, S.A.: Counter-Free Automata. M.I.T research monograph, vol.\u00a065. The MIT Press, Cambridge (1971)"},{"key":"30_CR21","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\u00fcchi Automata and \u03c9-Expressions. In: Agrawal, M., Du, D.-Z., Duan, Z., Li, A. (eds.) TAMC 2008. LNCS, vol.\u00a04978, pp. 47\u201358. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Combinatorial Optimization and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-17461-2_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,22]],"date-time":"2019-03-22T16:13:14Z","timestamp":1553271194000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-17461-2_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642174605","9783642174612"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-17461-2_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}