{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T12:59:28Z","timestamp":1748350768256},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540156482"},{"type":"electronic","value":"9783540395270"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1985]]},"DOI":"10.1007\/3-540-15648-8_31","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T13:22:31Z","timestamp":1330176151000},"page":"413-424","source":"Crossref","is-referenced-by-count":22,"title":["The taming of converse: Reasoning about two-way computations"],"prefix":"10.1007","author":[{"given":"Moshe Y.","family":"Vardi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"31_CR1","doi-asserted-by":"crossref","first-page":"402","DOI":"10.1016\/0022-0000(82)90018-6","volume":"25","author":"M. Ben-Ari","year":"1982","unstructured":"M. Ben-Ari, J.Y. Halpern, A. Pnueli, \u201cDeterministic Propositional Dynamic Logic: Finite Models, Complexity, and Completeness\u201d, J. Computer and System Science, 25(1982), pp. 402\u2013417.","journal-title":"J. Computer and System Science"},{"key":"31_CR2","unstructured":"J.R. B\u00fcchi, \u201cOn a Decision Method in Restricted Second Order Arithmetic\u201d, Proc. Int'l Congr. Logic, Method and Phil. Sci. 1960. Stanford University Press, 1962, pp. 1\u201312."},{"key":"31_CR3","unstructured":"R. Danecki, \u201cPropositional Dynamic Logic with Strong Looping Predicate\u201d, 1984."},{"key":"31_CR4","unstructured":"J. de Bakker, Mathematical theory of program correctness, Prentice hall, 1980."},{"issue":"2","key":"31_CR5","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M.J. Fisher","year":"1979","unstructured":"M.J. Fisher, R.E. Ladner, \u201cPropositional Dynamic Logic of Regular Programs\u201d, J. Computer and System Sciences, 18(2), 1979, pp. 194\u2013211.","journal-title":"J. Computer and System Sciences"},{"key":"31_CR6","unstructured":"J.Y. Halpern, private communication, 1983."},{"key":"31_CR7","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/S0019-9958(82)90553-8","volume":"55","author":"D. Harel","year":"1982","unstructured":"D. Harel, R. Sherman, \u201cLooping vs. Repeating in Dynamic Logic\u201d, Information and Control 55(1982), pp. 175\u2013192.","journal-title":"Information and Control"},{"key":"31_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/3-540-12689-9_104","volume-title":"Propositional Dynamic Logic of Flowcharts","author":"D. Harel","year":"1983","unstructured":"D. Harel, R. Sherman, \u201cPropositional Dynamic Logic of Flowcharts\u201d, Proc. Int. Conf. on Foundations of Computation Theory, Lecture Notes in Computer Science, vol. 158, Springer-Verlag, Berlin, 1983, pp. 195\u2013206."},{"key":"31_CR9","unstructured":"Parikh, R.: A completeness result for PDL. Symp. on Math. Foundations of Computer Science, Zakopane, 1978."},{"key":"31_CR10","doi-asserted-by":"crossref","unstructured":"V.R. Pratt, \u201cSemantical Considerations on Floyd-Hoare Logic\u201d, Proc. 17th IEEE Symp. on Foundations of Computer Science, Houston, October 1976, pp. 109\u2013121.","DOI":"10.1109\/SFCS.1976.27"},{"key":"31_CR11","doi-asserted-by":"crossref","unstructured":"V.R. Pratt, \u201cModels of Program Logics\u201d, Proc. 20th IEEE Symp. on Foundation of Computer Science, San Juan, 1979, pp. 115\u2013122.","DOI":"10.1109\/SFCS.1979.24"},{"key":"31_CR12","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0022-0000(80)90061-6","volume":"20","author":"V.R. Pratt","year":"1980","unstructured":"V.R. Pratt, \u201cA Near-Optimal Method for Reasoning about Action\u201d, J. Computer and Systems Sciences 20(1980), pp. 231\u2013254.","journal-title":"J. Computer and Systems Sciences"},{"key":"31_CR13","series-title":"Yorktown-Heights, Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1007\/BFb0025792","volume-title":"Using Graphs to understand PDL","author":"V.R. Pratt","year":"1982","unstructured":"V.R. Pratt, \u201cUsing Graphs to understand PDL\u201d, Proc. Workshop on Logics of Programs, (D. Kozen, ed.), Yorktown-Heights, Lecture Notes in Computer Science, vol. 131, Springer-Verlag, Berlin, 1982, pp. 387\u2013396."},{"key":"31_CR14","unstructured":"A. Pnueli, R. Sherman, \u201cPropositional Dynamic Logic of Looping Flowcharts\u201d, Technical Report, Weizmann Institute, Rehovot, Israel, 1983."},{"key":"31_CR15","doi-asserted-by":"crossref","unstructured":"M.O. Rabin, \u201cWeakly Definable Relations and Special Automata\u201d, Proc. Symp. Math. Logic and Foundations of Set Theory (Y. Bar-Hillel, ed.), North-Holland, 1970, pp. 1\u201323.","DOI":"10.1016\/S0049-237X(08)71929-3"},{"key":"31_CR16","unstructured":"R. Sherman, \u201cVariants of Propositional Dynamic Logic,\u201d Ph.D. Dissertation, The Weizmann Inst. of Science, 1984."},{"key":"31_CR17","unstructured":"R.S. Streett, \u201cA Propositional Dynamic Logic for Reasoning about Program Divergence\u201d, M.Sc. Thesis, MIT, 1980."},{"key":"31_CR18","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/S0019-9958(82)91258-X","volume":"54","author":"R.S. Streett","year":"1982","unstructured":"R.S. Streett, \u201cPropositional Dynamic Logic of Looping and Converse is elementarily decidable\u201d, Information and Control 54(1982), pp. 121\u2013141.","journal-title":"Information and Control"},{"key":"31_CR19","doi-asserted-by":"crossref","unstructured":"M.Y. Vardi, L. Stockmeyer, \u201cImproved Upper and Lower Bounds for Modal Logics of Programs\u201d, To appear in Proc. 17th ACM Symp. on Theory of Computing, Providence, May 1985.","DOI":"10.1145\/22145.22173"},{"key":"31_CR20","doi-asserted-by":"crossref","unstructured":"M. Y. Vardi, P. Wolper, \u201cAutomata Theoretic Techniques for Modal Logics of Programs\u201d, IBM Research Report, October 1984. A preliminary version appeared in Proc. ACM Symp. on Theory of Computing, Washington, April 1984, pp. 446\u2013456.","DOI":"10.1145\/800057.808711"}],"container-title":["Lecture Notes in Computer Science","Logics of Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-15648-8_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:08:36Z","timestamp":1605625716000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-15648-8_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1985]]},"ISBN":["9783540156482","9783540395270"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-15648-8_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1985]]}}}