{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T20:40:24Z","timestamp":1742589624663,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":67,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540111603"},{"type":"electronic","value":"9783540386315"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1981]]},"DOI":"10.1007\/3-540-11160-3_4","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T17:37:58Z","timestamp":1330191478000},"page":"102-144","source":"Crossref","is-referenced-by-count":21,"title":["Propositional dynamic logics of programs: A survey"],"prefix":"10.1007","author":[{"given":"Rohit","family":"Parikh","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"4_CR1","first-page":"21","volume-title":"Proc. Conf. on Parallel Programs","author":"K. Abrahamson","year":"1979","unstructured":"Abrahamson, Karl, Modal Logic of Concurrent Nondeterministic Pograms, Proc. Conf. on Parallel Programs, Evian, France, 1979, 21\u201333."},{"key":"4_CR2","volume-title":"The Design and Analysis of Computer Algorithms","author":"A. V. Aho","year":"1974","unstructured":"Aho A.V., J.E. Hopcroft, and J.D. Ullman, The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading, Mass., 1974."},{"key":"4_CR3","volume-title":"Math. Found. of Comp. Sci.","author":"L. Banachowski","year":"1977","unstructured":"Banachowski, L., A. Kreczmar, G. Mirkowska, H. Rasiowa, A. Salwicki., An Introduction to Algorithmic Logic; Metamathematical Investigations in the Theory of Programs, In Math. Found. of Comp. Sci. (eds. Mazurkiewicz and Pawlak), Banach Center Publications, Warsaw. 1977."},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Berman, F., A completeness technique for D-axiomatizable semantics, Proc. 11th ACM Symp. on Theory of Comp. (May 1979), 160\u2013166.","DOI":"10.1145\/800135.804409"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Ben-Ari, M., Halpern, J., and Pnueli, A., Finite Models for Deterministic Propositional Dynamic Logic, Proceedings of the 8th ICALP conference, Jerusalem 1981, Springer LNCS 115, pp. 249\u2013263.","DOI":"10.1007\/3-540-10843-2_21"},{"key":"4_CR6","unstructured":"Berman, F. and M. Paterson., Test-Free Propositional Dynamic Logic is Strictly Weaker than PDL, T.R. 77-10-02, Dept. of Computer Science, Univ. of Washington, Seattle. Nov. 1977."},{"key":"4_CR7","volume-title":"Models and Ultraproducts","author":"J. S. Bell","year":"1971","unstructured":"Bell, J.S. and A.B. Slomson, Models and Ultraproducts. North Holland, Amsterdam, 1971."},{"key":"4_CR8","volume-title":"Regular Algebra and Finite Machines","author":"J. H. Conway","year":"1971","unstructured":"Conway, J.H. Regular Algebra and Finite Machines. Chapman-Hall, London, 1971."},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Chandra, A., Halpern, J., Meyer, A., and Parikh, R., Equations between Regular Terms and an Application to Process Logic, Proceedings of STOC 1981, pp. 384\u2013390.","DOI":"10.1145\/800076.802493"},{"key":"4_CR10","volume-title":"A Programming Logic","author":"R. L. Constable","year":"1978","unstructured":"Constable, R.L. and M.J. O'Donnell. A Programming Logic. Winthrop, Cambridge, Mass., 1978."},{"key":"4_CR11","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BF01705528","volume":"1","author":"E. Engeler","year":"1967","unstructured":"Engeler, E., Algorithmic properties of structures, Math. Systems Theory. 1, 183\u2013195. 1967.","journal-title":"Math. Systems Theory."},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Fischer, M.J. and R.E. Ladner., Propositional Modal Logic of Programs, Proc. 9th Ann. ACM Symp. on Theory of Computing, 286\u2013294, Boulder, Col., May 1977.","DOI":"10.1145\/800105.803418"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Floyd, R.W., Assigning Meanings to Programs, In Mathematical Aspects of Computer Science (ed. J.T. Schwartz), 19\u201332, 1967.","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"4_CR14","unstructured":"Gabbay, D., Axiomatizations of Logics of Programs, Typescript, Nov. 1977."},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Gabbay G., Pnueli, A. Shelah, S. and Stavi, J., The Temporal Analysis of Fairness, 7th Annual ACM Symposium on POPL, Jan 1980, 163\u2013173.","DOI":"10.1145\/567446.567462"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Greif, I. and A. R. Meyer, Specifying Programming Language Semantics, Proc. 6th Ann. ACM Symp. on Principles of Programming Languages, 180\u2013189, San Antonio, Texas, Jan. 1979.","DOI":"10.1145\/567752.567769"},{"key":"4_CR17","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-9855-7","volume-title":"Lectures on Boolean Algebras","author":"P. R. Halmos","year":"1974","unstructured":"Halmos, P.R. Lectures on Boolean Algebras. Springer Verlag, New York, 1974."},{"key":"4_CR18","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1016\/0020-0190(79)90022-X","volume":"8","author":"D. Harel","year":"1979","unstructured":"Harel, D., Two Results on Process Logic, Information Processing Letters, 8 (1979) 195\u2013198.","journal-title":"Information Processing Letters"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Harel, D. First Order Dynamic Logic, Lecture Notes in Computer Science, no. 68, Springer Verlag 1979.","DOI":"10.1007\/3-540-09237-4"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Harel, D., Kozen, D., Parikh, R., Process Logic: Expressiveness, Decidability, Completeness, Proc. IEEE-FOCS 1980, pp. 129\u2013142.","DOI":"10.1109\/SFCS.1980.35"},{"key":"4_CR21","first-page":"135","volume":"3","author":"C. A. R. R. Hoare","year":"1974","unstructured":"Hoare, C.A.R., and Lauer, P.E., Consistent and Complementary Formal Theories of the Semantics of Programming Languages. Acta Informatica 3, (1974) 135\u2013153.","journal-title":"Acta Informatica"},{"key":"4_CR22","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C. A. R. R. Hoare","year":"1969","unstructured":"Hoare, C.A.R., An Axiomatic Basis for Computer Programming, CACM 12, 576\u2013580, 1969.","journal-title":"CACM"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Harel, D., Pnueli, A., and Stavi, J., Propositional Dynamic Logic of Recursive Programs, Research report, May 1981.","DOI":"10.1109\/SFCS.1981.38"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Halpern, J., and Reif, J., The Propositional Dynamic Logic of Deterministic, Well-structured Programs, MIT-LCS TM no. 198, March 1981. To appear in Proc IEEE-FOCS 1981.","DOI":"10.1109\/SFCS.1981.49"},{"key":"4_CR25","unstructured":"Kamp, H., Tense Logic and the Theory of Linear Order, Ph.D. thesis, UCLA 1968."},{"key":"4_CR26","volume-title":"Model Theory for Infinitary Logic","author":"H. J. Keisler","year":"1971","unstructured":"Keisler, H.J. Model Theory for Infinitary Logic. North Holland, Amsterdam, 1971."},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Kozen, D., A representation theorem for models of *-free PDL, Proc. 7th Int. Colloq. on Automata, Languages, and Programming, Lecture Notes in Computer Science 85, ed. Goos and Hartmanis, Springer-Verlag, Berlin, 1980, 351\u2013362. Also Report RC7864, IBM Research, Yorktown Heights, New York, Sept. 1979.","DOI":"10.1007\/3-540-10003-2_83"},{"key":"4_CR28","unstructured":"Kozen, D., On the duality of dynamic algebras and Kripke models, Report RC7893, IBM Research, Yorktown Heights, New York, Oct. 1979."},{"key":"4_CR29","unstructured":"Kozen, D., On the representation of dynamic algebras, Report RC7898, IBM Research, Yorktown Heights, New York, Oct. 1979."},{"key":"4_CR30","volume-title":"On the representation of dynamic algebras II, Report RC8290","author":"D. Kozen","year":"1980","unstructured":"Kozen, D., On the representation of dynamic algebras II, Report RC8290, IBM Research, Yorktown Heights, New York, May 1980."},{"key":"4_CR31","volume-title":"On induction vs. *-continuity, Report RC8468","author":"D. Kozen","year":"1980","unstructured":"Kozen, D., On induction vs. *-continuity, Report RC8468, IBM Research, Yorktown Heights, New York, Sept. 1980."},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"Kozen, D., Semantics of Probabilistic Programs, 20th IEEE-FOCS Symposium, San Juan, 1979, 101\u2013114.","DOI":"10.1109\/SFCS.1979.38"},{"key":"4_CR33","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/0304-3975(81)90019-0","volume":"14","author":"D. Kozen","year":"1981","unstructured":"Kozen, D. and Parikh, R., An elementary Completeness Proof for PDL, TCS vol 14 (1981) pp. 113\u2013118.","journal-title":"TCS"},{"key":"4_CR34","unstructured":"Kripke, S., Semantical considerations on Modal Logic, Acta Philosophica Fennica, 83\u201394, 1963."},{"key":"4_CR35","unstructured":"Litvinchouk, S.D. and V.R. Pratt., A Proof-checker for Dynamic Logic, Proc. 5th Int. Joint Conf. on AI, 552\u2013558, Boston, Aug. 1977."},{"key":"4_CR36","unstructured":"Manna, Z., Mathematical Theory of Computation. McGraw-Hill, 1974."},{"key":"4_CR37","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1007\/BFb0064872","volume":"453","author":"A. Meyer","year":"1974","unstructured":"Meyer, A., WSIS is not elementary decidable, Proceedings of the Boston Logic Colloquium, edited by R. Parikh, Springer Lecture Notes in Mathematics vol. 453, 1974, pp. 132\u2013154.","journal-title":"Springer Lecture Notes in Mathematics"},{"key":"4_CR38","doi-asserted-by":"crossref","unstructured":"Mirkowska, G., Complete Axiomatisation of Algorithmic Properties of Program Schemes with Bounded Nondeterministic Interpretations, 12th Annual ACM-STOC Symposium (1980), 14\u201321.","DOI":"10.1145\/800141.804648"},{"key":"4_CR39","first-page":"238","volume":"115","author":"A. Meyer","year":"1981","unstructured":"Meyer, A., Street, R., and Mirkowska, G., The Deducibility Problem in Propositional Dynamic Logic, Proc. 8th ICALP, Springer LNCS 115 (1981) pp. 238\u2013248.","journal-title":"Proc. 8th ICALP"},{"key":"4_CR40","volume-title":"Every free algebra in the variety generated by the representable dynamic algebras is separable and representable, manuscript","author":"I. Nemeti","year":"1980","unstructured":"Nemeti, I., Every free algebra in the variety generated by the representable dynamic algebras is separable and representable, manuscript, Hungarian Academy of Sciences, Budapest, 1980."},{"key":"4_CR41","doi-asserted-by":"crossref","unstructured":"Nishimura, H., Descriptively Complete Process Logic, typescript, Kyoto University, Dec. 1979.","DOI":"10.1007\/BF00286492"},{"key":"4_CR42","doi-asserted-by":"crossref","unstructured":"Owicki, S., A Consistent and Complete Deductive System for the Verification of Parallel Programs, Proc. 8th Ann. ACM Symp. on Theory of Computing, 73\u201386. Hershey PA. May 1976.","DOI":"10.1145\/800113.803634"},{"key":"4_CR43","unstructured":"Parikh, R., A Completeness Result for PDL, Manuscript dated 11\/29\/77."},{"key":"4_CR44","first-page":"403","volume-title":"A Completeness Result for PDL, Symposium on Mathematical Foundations of Computer Science","author":"R. Parikh","year":"1978","unstructured":"Parikh, R., A Completeness Result for PDL, Symposium on Mathematical Foundations of Computer Science, Zakopane, Poland, Springer LNCS 64, Sept. 1978, pp. 403\u2013415."},{"key":"4_CR45","doi-asserted-by":"crossref","unstructured":"Parikh, R., Second Order Process Logic, 19th IEEE Symposium on Foundations of Computer Science. Oct. 1978 pp. 177\u2013183.","DOI":"10.1109\/SFCS.1978.2"},{"key":"4_CR46","doi-asserted-by":"crossref","unstructured":"Parikh, R., Propositional Logics of Programs, Proc. 7th Ann. ACM Symp. on Principles of Programming Languages, Las Vegas, Jan. 1980. pp. 186\u2013192.","DOI":"10.1145\/567446.567464"},{"key":"4_CR47","unstructured":"Parikh, R., Some Applications of Topology to Program Semantics, to appear in Math. Systems theory."},{"key":"4_CR48","doi-asserted-by":"crossref","unstructured":"Pnueli, A., The Temporal Logic of Programs, 18th IEEE Symposium on Foundations of Computer Science, 46\u201357. Oct. 1977, pp. 46\u201357.","DOI":"10.1109\/SFCS.1977.32"},{"key":"4_CR49","doi-asserted-by":"crossref","unstructured":"Pratt, V.R., Semantical Considerations on Floyd-Hoare Logic, Proc. 17th Ann. IEEE Symp. on Foundations of Comp. Sci., 109\u2013121. Oct. 1976, pp. 109\u2013121.","DOI":"10.1109\/SFCS.1976.27"},{"key":"4_CR50","doi-asserted-by":"crossref","unstructured":"Pratt, V.R., A Practical Decision Method for Propositional Dynamic Logic, Proc. 10th Annual ACM Symposium on Theory of Computing, 326\u2013337, San Diego, Calif., May 1978.","DOI":"10.1145\/800133.804362"},{"key":"4_CR51","doi-asserted-by":"crossref","unstructured":"Pratt, V.R., Process Logic, Proc. 6th Ann. ACM Symp. on Principles of Programming Languages, Jan. 1979.","DOI":"10.1145\/567752.567761"},{"key":"4_CR52","doi-asserted-by":"crossref","unstructured":"Pratt, V.R., Models of Program Logics, 20th IEEE-FOCS Symposium, San Juan, 1979, 115\u2013122.","DOI":"10.1109\/SFCS.1979.24"},{"key":"4_CR53","unstructured":"Pratt, V.R., Dynamic Algebras: Examples, Constructions, Applications, MIT\/LCS\/TM-138, July 1979."},{"key":"4_CR54","volume-title":"Proc. 6th International Congress for Logic, Philosophy, and Methodology of Science","author":"V. R. Pratt","year":"1979","unstructured":"Pratt, V.R., Dynamic Logic, Proc. 6th International Congress for Logic, Philosophy, and Methodology of Science, Hanover, W. Germany, Aug. 1979."},{"key":"4_CR55","doi-asserted-by":"crossref","unstructured":"Pratt, V.R., Dynamic algebras and the nature of induction, Proc. 12th ACM Symp. on Theory of Computing (May 1980), 22\u201328.","DOI":"10.1145\/800141.804649"},{"key":"4_CR56","first-page":"120","volume":"16","author":"V. N. Redko","year":"1964","unstructured":"Redko, V.N., On Defining Relations for the Algebra of Regular Events (Russian) Ukrain. Math. Z. 16 (1964), 120\u2013126.","journal-title":"Ukrain. Math. Z."},{"key":"4_CR57","doi-asserted-by":"crossref","unstructured":"Reif, J., Logics for Probabilistic Computation, 12th Annual ACM-STOC Symposium (1980), 8\u201313.","DOI":"10.1145\/800141.804647"},{"key":"4_CR58","first-page":"1","volume":"141","author":"M. Rabin","year":"1969","unstructured":"Rabin, M., Decidability of Second Order Theories and Automata on Infinite Trees, Transactions of the Amer. Math. Soc., 141 (1969) 1\u201335.","journal-title":"Transactions of the Amer. Math. Soc."},{"key":"4_CR59","unstructured":"Reiterman, J. and V. Trnkova, Dynamic algebras which are not Kripke structures, Proc. 9th Symp. on Math. Found. of Computer Science (Aug. 1980), 528\u2013538."},{"key":"4_CR60","unstructured":"Reiterman, J. and V. Trnkova, private communication."},{"key":"4_CR61","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1145\/321312.321326","volume":"13","author":"A. Salomaa","year":"1966","unstructured":"Salomaa, A., Two Complete Axiom Systems for the Algebra of Regular Events, Jour. ACM 13 (1966), 158\u2013169.","journal-title":"Jour. ACM"},{"key":"4_CR62","unstructured":"Salwicki, A., Formalized Algorithmic Languages, Bull. Acad. Pol. Sci., Ser. Sci. Math. Astr. Phys. Vol. 18. No. 5. 1970."},{"key":"4_CR63","unstructured":"Segerberg, K., A Completeness Theorem in the Modal Logic of Programs, Preliminary report. Notices of the AMS, 24, 6, A-552. Oct. 1977."},{"key":"4_CR64","unstructured":"Semyonov, A.L., Some Algorithmic Problems for Systems of Algorithmic Algebras, Doklady vol. 239 (1978)."},{"key":"4_CR65","unstructured":"Stockmeyer, L., The Complexity of Decision Procedures, MIT project MAC report TR-133, July 1974."},{"key":"4_CR66","unstructured":"Street, R., Propositional Dynamic Logic of Looping and Converse, Proc. 13th ACM-STOC Symposium (1981), pp. 375\u2013383."},{"key":"4_CR67","first-page":"482","volume-title":"Symposium on Mathematical Foundations of Computer Science","author":"B. Valiev","year":"1979","unstructured":"Valiev, B., On Axiomatisation of Deterministic Propositional Dynamic Logic, Symposium on Mathematical Foundations of Computer Science, Olomouc, Czechoslovakia, Sept. 1979, 482\u2013491."}],"container-title":["Lecture Notes in Computer Science","Logic of Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-11160-3_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T20:16:04Z","timestamp":1742588164000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-11160-3_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1981]]},"ISBN":["9783540111603","9783540386315"],"references-count":67,"URL":"https:\/\/doi.org\/10.1007\/3-540-11160-3_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1981]]}}}