{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:54:22Z","timestamp":1725663262458},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540527534"},{"type":"electronic","value":"9783540471370"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52753-2_48","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T16:42:21Z","timestamp":1330188141000},"page":"322-336","source":"Crossref","is-referenced-by-count":1,"title":["A streamlined temporal completeness theorem"],"prefix":"10.1007","author":[{"given":"Ana","family":"Pasztor","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ildiko","family":"Sain","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"20_CR1","unstructured":"M.Abadi, \u201dThe power of temporal proofs\u201d, preprint of Digital Systems Research Center (1988)."},{"key":"20_CR2","unstructured":"M.Abadi, \u201dTemporal logic was incomplete only temporarily\u201d, Preprint (1989)."},{"key":"20_CR3","unstructured":"M.Abadi and Z.Manna, \u201dA timely resolution\u201d, First Annual Symposium in Computer Science, (1986), 176\u2013186."},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"H. Andreka, \u201dSharpening the characterization of the power of Floyd's method\u201d, in: Logic of Programs and their Applications, ed.: A. Salwicki (Proc. Conf. Poznan 1980), Lecture Notes in Computer Science 148, Springer-Verlag 2983, pp. 1\u201326.","DOI":"10.1007\/3-540-11981-7_1"},{"key":"20_CR5","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1016\/0304-3975(82)90004-4","volume":"17","author":"H. Andreka","year":"1982","unstructured":"H. Andreka, I. Nemeti and I. Sain, \u201cA complete logic for reasoning about programs via nonstandard model theory\u201d, Parts I\u2013II, Theoretical Computer Science 17 (1982), pp. 193\u2013212 and pp. 259\u2013278.","journal-title":"Theoretical Computer Science"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"H.Andreka, I.Nemeti, I.Sain, \u201dOn the strength of temporal proofs\u201d, Proc. Conf. MFCS'89 (Mathem. Foundations of Comp. Sci.), in press (1989).","DOI":"10.1007\/3-540-51486-4_61"},{"key":"20_CR7","unstructured":"B.Biro and I.Sain, \u201dPeano Arithmetic for the time scale of nonstandard models for logics of programs\u201d, Annals of Pure and Applied Logic, to appear."},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"D.Gabbay and F.Guenther (eds), \u201dHandbook of philosophical logic\u201d, D.Reidel Publ. Co. vol II (1984).","DOI":"10.1007\/978-94-009-6259-0"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"D.Gabbay, A.Pnueli, S.Shelah, J.Stavi, \u201dOn the temporal analysis of fairness\u201d, Preprint Weizman Institute of Science, Dept. of Applied Math. (1981).","DOI":"10.1145\/567446.567462"},{"key":"20_CR10","unstructured":"T.Gergely and L.Ury, \u201dFirst-order programming theories\u201d, SZAMALK Technical Report Budapest (1989), 232pp."},{"key":"20_CR11","unstructured":"R.Goldblatt, \u201dLogics of time and computation\u201d, Center for the Study of Language and Information, Lecture Notes Number 7 (1987)."},{"key":"20_CR12","unstructured":"L.Henkin, J.D.Monk, A.Tarski, \u201dCylindric Algebras Part II\u201d, North Holland (1985)."},{"key":"20_CR13","unstructured":"J.A. Makowsky and I. Sain, \u201dWeak second order characterizations of various program verification systems\u201d, Technical Report #457, Technion-Israel Institute of Technology, Comp. Sci. Dept., June 1987. Submitted to Theoretical Computer Science."},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Z.Manna and A.Pnueli, \u201dHow to cook a temporal proof system for your pet language\u201d, Tenth ACM Symposium on Principles of Programming languages, (1983), 141\u2013154.","DOI":"10.1145\/567067.567082"},{"key":"20_CR15","unstructured":"Z.Manna and A.Pnueli, \u201dVerification of concurrent programs: A temporal proof system\u201d, Report No. STAN-CS-83-967, Comp. Sci. Dept., Stanford University, (1983)."},{"issue":"3","key":"20_CR16","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/0167-6423(84)90003-0","volume":"4","author":"Z. Manna","year":"1984","unstructured":"Z. Manna and A. Pnueli, \u201dAdequate proof principles for invariance and liveliness properties of concurrent programs\u201d, Science of Computer Programming, vol. 4, No. 3, (1984), 257\u2013289.","journal-title":"Science of Computer Programming"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"I. Nemeti, \u201dNonstandard dynamic logic\u201d, in: Logics of Programs, ed.: D. Kozen, (Proc. Conf. New York 1981) Lecture Notes in Computer Science 131, Springer-Verlag, 1982, pp. 311\u2013348.","DOI":"10.1007\/BFb0025789"},{"issue":"3","key":"20_CR18","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"S. Owicki","year":"1982","unstructured":"S. Owicki and L. Lamport, \u201dProving liveness properties of concurrent programs\u201d, ACM Transactions on Programming Languages and Systems, vol. 4, No. 3, (1982), 455\u2013495.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"R.Parikh, \u201dA decidability result for second order process logic\u201d, IEEE Symposium on Foundation of Comp. Sci. (1978), 177\u2013183.","DOI":"10.1109\/SFCS.1978.2"},{"key":"20_CR20","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1016\/S0747-7171(86)80013-X","volume":"2","author":"A. Pasztor","year":"1986","unstructured":"A. Pasztor, \u201dNonstandard Algorithmic and Dynamic Logic\u201d, in: J. Symbolic Computation 2 (1986), pp. 59\u201381.","journal-title":"J. Symbolic Computation"},{"key":"20_CR21","unstructured":"A.Pasztor, \u201cPnueli's temporal method is complete for nondeterministic programs\u201d, Florida International University School of Computer Science Research Report 89-09, University Park, Miami, FL 33199, (1989)."},{"key":"20_CR22","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"A. Pnueli, \u201dThe temporal semantics of concurrent programs\u201d, Theoretical Computer Science 13, (1981), 45\u201360.","journal-title":"Theoretical Computer Science"},{"key":"20_CR23","first-page":"667","volume":"42","author":"M.M. Richter","year":"1986","unstructured":"M.M. Richter and M.E. Szabo, \u201dNonstandard computation theory\u201d, In: Algebra, combinatorics, and logic in computer science, Proc. Conf. Gyoer Hungary 1983 (eds: J.Demetrovics, G.Katona, A.Salomaa), Colloq. Math. Soc. J.Bolyai vol 42, North-Holland (1986), 667\u2013693.","journal-title":"Colloq. Math. Soc. J.Bolyai"},{"key":"20_CR24","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1002\/malq.19840303102","volume":"3","author":"I. Sain","year":"1984","unstructured":"I. Sain, \u201dStructured nonstandard dynamic logic\u201d, Zeitschrift fur Math. Logic und Grundlagen der Math. Heft 3, 1984, pp. 481\u2013497.","journal-title":"Zeitschrift fur Math. Logic und Grundlagen der Math."},{"key":"20_CR25","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1016\/0304-3975(85)90024-6","volume":"35","author":"I. Sain","year":"1985","unstructured":"I. Sain, \u201dA simple proof for completeness of Floyd method\u201d, Theoretical Computer Science vol 35 (1985), 345\u2013348.","journal-title":"Theoretical Computer Science"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"I. Sain, \u201dThe reasoning powers of Burstall's (modal logic) and Pnueli's (temporal logic) program verification methods\u201d, in: Logics of Programs, ed.: R. Parikh (Proc. Conf. Brooklyn USA 1985) Lecture Notes in Computer Science 193, Springer-Verlag, pp. 302\u2013319.","DOI":"10.1007\/3-540-15648-8_24"},{"key":"20_CR27","unstructured":"I. Sain, \u201dDynamic logic with nonstandard model theory\u201d, Dissertation, Hungarian Academy of Sciences, Budapest, 1986 (in Hungarian)."},{"key":"20_CR28","unstructured":"I. Sain, \u201dIs \u201cSOME OTHER TIME\u201d sometimes better than \u201cSOMETIME\u201d in proving partial correctness of programs?\u201d, to appear in a special vol. of Studia Logica on nonstandard methods edited by M.M. Richter and M.E. Szabo."},{"key":"20_CR29","doi-asserted-by":"crossref","unstructured":"I.Sain, \u201dElementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic\u201d, Notre Dame Journal of Formal Logic, to appear (1989).","DOI":"10.1305\/ndjfl\/1093635239"},{"key":"20_CR30","unstructured":"I. Sain, \u201dRelative program verifying powers of the various temporal logics\u201d, Information and Control, to appear. An extended abstract of this is [26]."},{"key":"20_CR31","unstructured":"I.Sain, \u201dComparing and characterizing the power of established program verification methods\u201d, In: Many Sorted Logic and its applications (ed: J. Tucker), Proc. Conf. Leeds, Great Britain 1988, to appear."}],"container-title":["Lecture Notes in Computer Science","CSL '89"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52753-2_48.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:25:12Z","timestamp":1605630312000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52753-2_48"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540527534","9783540471370"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-52753-2_48","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]}}}