Skip to main content
SpringerLink
Log in

Dynamic Logic

  • Chapter
Handbook of Philosophical Logic

Part of the book series: Handbook of Philosophical Logic ((HALO,volume 4))

Abstract

Dynamic Logic (DL) is a formal system for reasoning about programs. Traditionally, this has meant formalizing correctness specifications and proving rigorously that those specifications are met by a particular program. Other activities fall into this category as well: determining the equivalence of programs, comparing the expressive power of various programming constructs, synthesizing programs from specifications, etc. Formal systems too numerous to mention have been proposed for these purposes, each with its own peculiarities.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 129.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

Bibliography

  1. K. Abrahamson. Decidability and expressiveness of logics of processes. PhD thesis, Univ. of Washington, 1980.

    Google Scholar 

  2. S. I. Adian. The Burnside Problem and Identities in Groups. Springer-Verlag, 1979.

    Book  Google Scholar 

  3. A. V. Aho, J. E. Hopcroft, and J. D. Ullman. The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading, Mass., 1975.

    Google Scholar 

  4. S. Ambler, M. Kwiatkowska, and N. Measor. Duality and the completeness of the modal μ-calculus. Theor. Comput. Sci., 151(1):3–27, November 1995.

    Article  Google Scholar 

  5. H. Andréka, I. Németi, and I. Sain. A complete logic for reasoning about programs via nonstandard model theory, part I. Theor. Comput. Sci., 17:193–212, 1982.

    Article  Google Scholar 

  6. H. Andréka, I. Németi, and I. Sain. A complete logic for reasoning about programs via nonstandard model theory, part II. Theor. Comput. Sci., 17:259–278, 1982.

    Article  Google Scholar 

  7. K. R. Apt and E.-R. Olderog. Verification of Sequential and Concurrent Programs. Springer-Verlag, 1991.

    Book  Google Scholar 

  8. K. R. Apt and G. Plotkin. Countable nondeterminism and random assignment. J. Assoc. Comput. Mach., 33:724–767, 1986.

    Article  Google Scholar 

  9. K. R. Apt. Ten years of Hoare’s logic: a survey—part I. ACM Trans. Programming Languages and Systems, 3:431–483, 1981.

    Article  Google Scholar 

  10. K. V. Archangelsky. A new finite complete solvable quasiequational calculus for algebra of regular languages. Manuscript, Kiev State University, 1992.

    Google Scholar 

  11. A. Arnold. An initial semantics for the μ-calculus on trees and Rabin’s complementation lemma. Technical report, University of Bordeaux, 1997.

    Google Scholar 

  12. A. Arnold. The μ-calculus on trees and Rabin’s complementation theorem. Technical report, University of Bordeaux, 1997.

    Google Scholar 

  13. R. C. Backhouse. Closure Algorithms and the Star-Height Problem of Regular Languages. PhD thesis, Imperial College, London, U.K., 1975.

    Google Scholar 

  14. R. C. Backhouse. Program Construction and Verification. Prentice-Hall, 1986.

    Google Scholar 

  15. C. Baier and M. Kwiatkowska. On the verification of qualitative properties of probabilistic processes under fairness constraints. Information Processing Letters, 66(2):71–79, April 1998.

    Article  Google Scholar 

  16. L. Banachowski, A. Kreczmar, G. Mirkowska, H. Rasiowa, and A. Salwicki. An introduction to algorithmic logic: metamathematical investigations in the theory of programs. In Mazurkiewitz and Pawlak, editors, Math. Found. Comput. Sci., pages 7–99. Banach Center, Warsaw, 1977.

    Google Scholar 

  17. M. Ben-Ari, J. Y. Halpern, and A. Pnueli. Deterministic propositional dynamic logic: finite models, complexity and completeness. J. Comput. Syst. Sci., 25:402–417, 1982.

    Article  Google Scholar 

  18. F. Berman and M. Paterson. Propositional dynamic logic is weaker without tests. Theor. Comput. Sci., 16:321–328, 1981.

    Article  Google Scholar 

  19. P. Berman, J. Y. Halpern, and J. Tiuryn. On the power of non-determinism in dynamic logic. In Nielsen and Schmidt, editors, Proc 9th Colloq. Automata Lang. Prog., volume 140 of Lect. Notes in Comput. Sci., pages 48–60. Springer-Verlag, 1982.

    Google Scholar 

  20. F. Berman. Expressiveness hierarchy for PDL with rich tests. Technical Report 78–11–01, Comput. Sci. Dept., Univ. of Washington, 1978.

    Google Scholar 

  21. F. Berman. A completeness technique for D-axiomatizable semantics. In Proc. 11th Symp. Theory of Comput., pages 160–166. ACM, 1979.

    Google Scholar 

  22. F. Berman. Semantics of looping programs in propositional dynamic logic. Math. Syst. Theory, 15:285–294, 1982.

    Article  Google Scholar 

  23. G. Bhat and R. Cleaveland. Efficient local model checking for fragments of the modal μ-calculus. In T. Margaria and B. Steffen, editors, Proc. Second Int. Workshop Tools and Algorithms for the Construction and Analysis of Systems (TACAS’96), volume 1055 of Lect. Notes in Comput. Sci., pages 107–112. Springer-Verlag, March 1996.

    Chapter  Google Scholar 

  24. S. L. Bloom and Z. Esik. Program correctness and matricial iteration theories. In Proc. 7th Int. Conf. Mathematical Foundations of Programming Semantics, volume 598 of Lecture Notes in Computer Science, pages 457–476. Springer-Verlag, 1992.

    Chapter  Google Scholar 

  25. S. L. Bloom and Z. Esik. Equational axioms for regular sets. Math. Struct. Comput. Sci., 3:1–24, 1993.

    Article  Google Scholar 

  26. R. Blute, J. Desharnais, A. Edelat, and P. Panangaden. Bisimulation for labeled Markov processes. In Proc. 12th Symp. Logic in Comput. Sci., pages 149–158. IEEE, 1997.

    Google Scholar 

  27. M. Boffa. Une remarque sur les systèmes complets d’identités rationnelles. Informatique Théoretique et Applications/Theoretical Informatics and Applications, 24(4):419–423, 1990.

    Google Scholar 

  28. Maurice Boffa. Une condition impliquant toutes les identités rationnelles. Informatique Théoretique et Applications/Theoretical Informatics and Applications, 29(6):515–518, 1995.

    Google Scholar 

  29. M. Bonsangue and M. Kwiatkowska. Reinterpreting the modal μ-calculus. In A. Ponse, M. de Rijke, and Y. Venema, editors, Modal Logic and Process Algebra, pages 65–83. CSLI Lecture Notes, August 1995.

    Google Scholar 

  30. E. Börger. Spectralproblem and completeness of logical decision problems. In G. Hasenjaeger, E. Borger and D. Rödding, editors, Logic and Machines: Decision Problems and Complexity, Proceedings, volume 171 of Lect. Notes in Comput. Sci., pages 333–356. Springer-Verlag, 1984.

    Chapter  Google Scholar 

  31. J. C. Bradfield. The modal μ-calculus alternation hierarchy is strict. In U. Montanari and V. Sassone, editors, Proc. CONCUR’96, volume 1119 of Lect. Notes in Comput. Sci., pages 233–246. Springer, 1996.

    Google Scholar 

  32. R. M. Burstall. Program proving as hand simulation with a little induction. Information Processing, pages 308–312, 1974.

    Google Scholar 

  33. A. Chandra, D. Kozen, and L. Stockmeyer. Alternation. J. Assoc. Comput. Mach., 28(1):114–133, 1981.

    Article  Google Scholar 

  34. B. F. Chellas. Modal Logic: An Introduction. Cambridge University Press, 1980.

    Book  Google Scholar 

  35. E. M. Clarke. Programming language constructs for which it is impossible to obtain good Hoare axiom systems. J. Assoc. Comput. Mach., 26:129–147, 1979.

    Article  Google Scholar 

  36. R. Cleaveland. Efficient model checking via the equational μ-calculus. In Proc. 11th Symp. Logic in Comput. Sci., pages 304–312. IEEE, July 1996.

    Google Scholar 

  37. Ernie Cohen, Dexter Kozen, and Frederick Smith. The complexity of Kleene algebra with tests. Technical Report 96–1598, Computer Science Department, Cornell University, July 1996.

    Google Scholar 

  38. E. Cohen. Hypotheses in Kleene algebra. Available as ftp://ftp.telcordia.com/pub/ernie/research/homepage.html, April 1994.

    Google Scholar 

  39. E. Cohen. Lazy caching. Available as ftp://ftp.telcordia.com/pub/ernie/research/homepage.html, 1994.

    Google Scholar 

  40. E. Cohen. Using Kleene algebra to reason about concurrency control. Available as ftp://ftp.telcordia.com/pub/ernie/research/homepage.html, 1994.

    Google Scholar 

  41. R. L. Constable and M. O’Donnell. A Programming Logic. Winthrop, 1978.

    Google Scholar 

  42. R. L. Constable. On the theory of programming logics. In Proc. 9th Symp. Theory of Comput., pages 269–285. ACM, May 1977.

    Google Scholar 

  43. J. H. Conway. Regular Algebra and Finite Machines. Chapman and Hall, London, 1971.

    Google Scholar 

  44. S. A. Cook. Soundness and completeness of an axiom system for program verification. SIAM J. Comput., 7:70–80, 1978.

    Article  Google Scholar 

  45. C. Courcoubetis and M. Yannakakis. Verifying temporal properties of finite-state probabilistic programs. In Proc. 29th Symp. Foundations of Comput Sci., pages 338–345. IEEE, October 1988.

    Google Scholar 

  46. P. Cousot. Methods and logics for proving programs. In J. van Leeuwen, editor, Handbood of Theoretical Computer Science, volume B, pages 841–993. Elsevier, Amsterdam, 1990.

    Google Scholar 

  47. L. Csirmaz. A completeness theorem for dynamic logic. Notre Dame J. Formal Logic, 26:51–60, 1985.

    Article  Google Scholar 

  48. M. D. Davis, R. Sigal, and E. J. Weyuker. Computability. Complexity, and Languages: Fundamentals of Theoretical Computer Science. Academic Press, 1994.

    Google Scholar 

  49. J. de Bakker. Mathematical Theory of Program Correctness. Prentice-Hall, 1980.

    Google Scholar 

  50. E. A. Emerson and J. Y. Halpern. Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. Syst. Sci., 30(1):1–24, 1985.

    Article  Google Scholar 

  51. E. A. Emerson and J. Y. Halpern. “Sometimes” and “not never” revisited: on branching vs. linear time temporal logic. J. ACM, 33(1):151–178, 1986.

    Article  Google Scholar 

  52. E. A. Emerson and C. Jutla. The complexity of tree automata and logics of programs. In Proc. 29th Symp. Foundations of Comput. Sci., pages 328–337. IEEE, October 1988.

    Google Scholar 

  53. E. A. Emerson and C. Jutla. On simultaneously determinizing and complementing ω-automata. In Proc. 4th Symp. Logic in Comput. Sci. IEEE, June 1989.

    Google Scholar 

  54. E. A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional μ-calculus. In Proc. 1st Symp. Logic in Comput. Sci., pages 267–278. IEEE, June 1986.

    Google Scholar 

  55. E. A. Emerson and C. L. Lei. Modalities for model checking: branching time strikes back. Sci. Comput. Programming, 8:275–306, 1987.

    Article  Google Scholar 

  56. E. A. Emerson and P. A. Sistla. Deciding full branching-time logic. Infor. and Control, 61:175–201, 1984.

    Article  Google Scholar 

  57. E. A. Emerson. Automata, tableax, and temporal logics. In R. Parikh, editor, Proc. Workshop on Logics of Programs, volume 193 of Lect. Notes in Comput. Sci., pages 79–88. Springer-Verlag, 1985.

    Chapter  Google Scholar 

  58. E. A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of theoretical computer science, volume B: formal models and semantics, pages 995–1072. Elsevier, 1990.

    Google Scholar 

  59. E. Engeler. Algorithmic properties of structures. Math. Syst. Theory, 1:183–195, 1967.

    Article  Google Scholar 

  60. J. Engelfriet. Iterated pushdown automata and complexity classes. In Proceedings of the Fifteenth Annual ACM Symposium on Theory of Computing, pages 365–373, Boston, Massachusetts, 1983.

    Chapter  Google Scholar 

  61. M. M. Erimbetov. On the expressive power of programming logics. In Proc. Alma-Ata Conf. Research in Theoretical Programming, pages 49–68, 1981. In Russian.

    Google Scholar 

  62. Y. A. Feldman and D. Harel. A probabilistic dynamic logic. J. Comput. Syst. Sci., 28:193–215, 1984.

    Article  Google Scholar 

  63. Y. A. Feldman. A decidable propositional dynamic logic with explicit probabilities. Infor, and Control, 63:11–38, 1984.

    Article  Google Scholar 

  64. M. J. Fischer and R. E. Ladner. Propositional modal logic of programs. In Proc. 9th Symp. Theory of Comput., pages 286–294. ACM, 1977.

    Google Scholar 

  65. M. J. Fischer and R. E. Ladner. Propositional dynamic logic of regular programs. J. Comput. Syst. Sci., 18(2):194–211, 1979.

    Article  Google Scholar 

  66. R. W. Floyd. Assigning meanings to programs. In Proc. Symp. Appl. Math., volume 19, pages 19–31. AMS, 1967.

    Google Scholar 

  67. H. Friedman. Algorithmic procedures, generalized Turing algorithms, and elementary recursion theory. In Gandy and Yates, editors, Logic Colloq. 1969, pages 361–390. North-Holland, 1971.

    Google Scholar 

  68. D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the temporal analysis of fairness. In Proc. 7th Symp. Princip. Prog. Lang., pages 163–173. ACM, 1980.

    Google Scholar 

  69. D. Gabbay, I. Hodkinson, and M. Reynolds. Temporal Logic-Mathematical Foundations and Computational Aspects. Oxford University Press, 1994.

    Book  Google Scholar 

  70. D. Gabbay. Axiomatizations of logics of programs. Unpublished, 1977.

    Google Scholar 

  71. R. Goldblatt. Axiomatising the Logic of Computer Programming, volume 130 of Lect. Notes in Comput. Sci. Springer-Verlag, 1982.

    Google Scholar 

  72. R. Goldblatt. Logics of time and computation. Technical Report Lect. Notes 7, Center for the Study of Language and Information, Stanford Univ., 1987.

    Google Scholar 

  73. S. Greibach. Theory of Program Structures: Schemes, Semantics, Verification, volume 36 of Lecture Notes in Computer Science. Springer Verlag, 1975.

    Book  Google Scholar 

  74. D. Gries. The Science of Programming. Springer-Verlag, 1981.

    Book  Google Scholar 

  75. Yu. Gurevich. Algebras of feasible functions. In 24-th IEEE Annual Symposium on Foundations of Computer Science, pages 210–214, 1983.

    Chapter  Google Scholar 

  76. J. Y. Halpern and J. H. Reif. The propositional dynamic logic of deterministic, well-structured programs. In Proc. 22nd Symp. Found. Comput. Sci., pages 322–334. IEEE, 1981.

    Google Scholar 

  77. J. Y. Halpern and J. H. Reif. The propositional dynamic logic of deterministic, well-structured programs. Theor. Comput. Sci., 27:127–165, 1983.

    Article  Google Scholar 

  78. J. Y. Halpern. On the expressive power of dynamic logic II. Technical Report TM-204, MIT/LCS, 1981.

    Google Scholar 

  79. J. Y. Halpern. Deterministic process logic is elementary. In Proc. 23rd Symp. Found. Comput. Sci., pages 204–216. IEEE, 1982.

    Google Scholar 

  80. J. Y. Halpern. Deterministic process logic is elementary. Infor. and Control, 57(l):56–89, 1983.

    Article  Google Scholar 

  81. H. Hansson and B. Jonsson. A logic for reasoning about time and probability. Formal Aspects of Computing, 6:512–535, 1994.

    Article  Google Scholar 

  82. D. Harel and D. Kozen. A programming language for the inductive sets, and applications. Information and Control, 63(1–2):118–139, 1984.

    Article  Google Scholar 

  83. D. Harel and M. S. Paterson. Undecidability of PDL with (Math). J. Comput. Syst. Sci., 29:359–365, 1984.

    Article  Google Scholar 

  84. D. Harel and D. Peleg. More on looping vs. repeating in dynamic logic. Information Processing Letters, 20:87–90, 1985.

    Article  Google Scholar 

  85. D. Harel and V. R. Pratt. Nondeterminism in logics of programs. In Proc. 5th Symp. Princip. Prog. Lang., pages 203–213. ACM, 1978.

    Google Scholar 

  86. D. Harel and D. Raz. Deciding properties of nonregular programs. SIAM J. Comput., 22:857–874, 1993.

    Article  Google Scholar 

  87. D. Harel and D. Raz. Deciding emptiness for stack automata on infinite trees. Information and Computation, 113:278–299, 1994.

    Article  Google Scholar 

  88. D. Harel and R. Sherman. Looping vs. repeating in dynamic logic. Infor. and Control, 55:175–192, 1982.

    Article  Google Scholar 

  89. D. Harel and R. Sherman. Propositional dynamic logic of flowcharts. Infor. and Control, 64:119–135, 1985.

    Article  Google Scholar 

  90. D. Harel and E. Singerman. More on nonregular PDL: Finite models and Fibonacci-like programs. Information and Computation, 128:109–118, 1996.

    Article  Google Scholar 

  91. D. Harel, A. R. Meyer, and V. R. Pratt. Computability and completeness in logics of programs. In Proc. 9th Symp. Theory of Comput., pages 261–268. ACM, 1977.

    Google Scholar 

  92. D. Harel, A. Pnueli, and M. Vardi. Two dimensional temporal logic and PDL with intersection. Unpublished, 1982.

    Google Scholar 

  93. D. Harel, D. Kozen, and R. Parikh. Process logic: Expressiveness, decidability, completeness. J. Comput. Syst. Sci., 25(2):144–170, 1982.

    Article  Google Scholar 

  94. D. Harel, A. Pnueli, and J. Stavi. Propositional dynamic logic of nonregular programs. J. Comput. Syst. Sci., 26:222–243, 1983.

    Article  Google Scholar 

  95. D. Harel, D. Kozen, and J. Tiuryn. Dynamic Logic. MIT Press, Cambridge, MA, 2000.

    Google Scholar 

  96. D. Harel. First-Order Dynamic Logic, volume 68 of Lect. Notes in Comput. Sci. Springer-Verlag, 1979.

    Book  Google Scholar 

  97. D. Harel. Dynamic logic. In Gabbay and Guenthner, editors, Handbook of Philosophical Logic, volume II: Extensions of Classical Logic, pages 497–604. Reidel, 1984.

    Chapter  Google Scholar 

  98. D. Harel. Recurring dominoes: Making the highly undecidable highly understandable. Annals of Discrete Mathematics, 24:51–72, 1985.

    Google Scholar 

  99. D. Harel. Algorithmics: The Spirit of Computing. Addison-Wesley, second edition, 1992.

    Google Scholar 

  100. S. Hart, M. Sharir, and A. Pnueli. Termination of probabilistic concurrent programs. In Proc. 9th Symp. Princip. Prog. Lang., pages 1–6. ACM, 1982.

    Google Scholar 

  101. C. Hartonas. Duality for modal μ-logics. Theor. Comput. Sci., 202(1–2):193–222, 1998.

    Article  Google Scholar 

  102. M. C. B. Hennessy and G. D. Plotkin. Full abstraction for a simple programming language. In Proc. Symp. Semantics of Algorithmic Languages, volume 74 of Lecture Notes in Computer Science, pages 108–120. Springer-Verlag, 1979.

    Google Scholar 

  103. P. Hitchcock and D. Park. Induction rules and termination proofs. In M. Nivat, editor, Int. Colloq. Automata Lang. Prog., pages 225–251. North-Holland, 1972.

    Google Scholar 

  104. C. A. R. Hoare. An axiomatic basis for computer programming. Comm. Assoc. Comput. Mach., 12:576–580, 583, 1969.

    Google Scholar 

  105. M. Hopkins and D. Kozen. Parikh’s theorem in commutative Kleene algebra. In Proc. Conf. Logic in Computer Science (LICS’99), pages 394–401. IEEE, July 1999.

    Google Scholar 

  106. G. E. Hughes and M. J. Cresswell. An Introduction to Modal Logic. Methuen, 1968.

    Google Scholar 

  107. M. Huth and M. Kwiatkowska. Quantitative analysis and model checking. In Proc. 12th Symp. Logic in Comput. Sci., pages 111–122. IEEE, 1997.

    Google Scholar 

  108. Y. I. Ianov. The logical schemes of algorithms. In Problems of Cybernetics, volume 1, pages 82–140. Pergamon Press, 1960.

    Google Scholar 

  109. K. Iwano and K. Steiglitz. A semiring on convex polygons and zero-sum cycle problems. SIAM J. Comput, 19(5):883–901, 1990.

    Article  Google Scholar 

  110. C. Jou and S. Smolka. Equivalences, congruences and complete axiomatizations for probabilistic processes. In Proc. CONCUR’90, volume 458 of Lecture Notes in Comput. Sci., pages 367–383. Springer-Verlag, 1990.

    Google Scholar 

  111. R. Kaivola. Using Automata to Characterise Fixed Point Temporal Logics. PhD thesis, University of Edinburgh, April 1997. Report CST-135–97.

    Google Scholar 

  112. H. W. Kamp. Tense logics and the theory of linear order. PhD thesis, UCLA, 1968.

    Google Scholar 

  113. J. Keisler. Model Theory for Infinitary Logic. North Holland, 1971.

    Google Scholar 

  114. A.J. Kfoury and A.P. Stolboushkin. An infinite pebble game and applications. Information and Computation, 136:53–66, 1997.

    Article  Google Scholar 

  115. A.J. Kfoury. Definability by programs in first-order structures. Theoretical Computer Science, 25:1–66, 1983.

    Article  Google Scholar 

  116. A. J. Kfoury. Definability by deterministic and nondeterministic programs with applications to first-order dynamic logic. Infor. and Control, 65(2–3):98–121, 1985.

    Article  Google Scholar 

  117. S. C. Kleene. Representation of events in nerve nets and finite automata. In C. E. Shannon and J. McCarthy, editors, Automata Studies, pages 3–41. Princeton University Press, Princeton, N.J., 1956.

    Google Scholar 

  118. P. M. W. Knijnenburg. On axiomatizations for propositional logics of programs. Technical Report RUU-CS-88–34, Rijksuniversiteit Utrecht, November 1988.

    Google Scholar 

  119. T. Koren and A. Pnueli. There exist decidable context-free propositional dynamic logics. In Proc. Symp. on Logics of Programs, volume 164 of Lecture Notes in Computer Science, pages 290–312. Springer-Verlag, 1983.

    Google Scholar 

  120. W. Kowalczyk, D. Niwinski, and J. Tiuryn. A generalization of Cook’s auxiliary-pushdown-automata theorem. Fundamenta Informaticae, XII:497–506, 1987.

    Google Scholar 

  121. D. Kozen and R. Parikh. An elementary proof of the completeness of FPL. Theor. Comput. Sci., 14(1):113–118, 1981.

    Article  Google Scholar 

  122. D. Kozen and R. Parikh. A decision procedure for the propositional μ-calculus. In Clarke and Kozen, editors, Proc. Workshop on Logics of Programs, volume 164 of Lecture Notes in Computer Science, pages 313–325. Springer-Verlag, 1983.

    Google Scholar 

  123. D. Kozen and M.-C. Patron. Certification of compiler optimizations using Kleene algebra with tests. In J. Lloyd, V. Dahl, U. Furbach, M. Kerber, K.-K. Lau, C. Palamidessi, L. M. Pereira, Y. Sagiv, and P. J. Stuckey, editors, Proc. 1st Int. Conf. Computational Logic (CL2000), volume 1861 of Lecture Notes in Artificial Intelligence, pages 568–582, London, July 2000. Springer-Verlag.

    Google Scholar 

  124. D. Kozen and F. Smith. Kleene algebra with tests: Completeness and decidability. In D. van Dalen and M. Bezem, editors, Proc. 10th Int. Workshop Computer Science Logic (CSL’96), volume 1258 of Lecture Notes in Computer Science, pages 244–259, Utrecht, The Netherlands, September 1996. Springer-Verlag.

    Google Scholar 

  125. D. Kozen and J. Tiuryn. Logics of programs. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 789–840. North Holland, Amsterdam, 1990.

    Google Scholar 

  126. D. Kozen. Dynamic algebra. In E. Engeler, editor, Proc. Workshop on Logic of Programs, volume 125 of Lecture Notes in Computer Science, pages 102–144. Springer-Verlag, 1979. chapter of Propositional dynamic logics of programs: A survey by Rohit Parikh.

    Google Scholar 

  127. D. Kozen. On the duality of dynamic algebras and Kripke models. In E. Engeler, editor, Proc. Workshop on Logic of Programs, volume 125 of Lecture Notes in Computer Science, pages 1–11. Springer-Verlag, 1979.

    Google Scholar 

  128. D. Kozen. On the representation of dynamic algebras. Technical Report RC7898, IBM Thomas J. Watson Research Center, October 1979.

    Google Scholar 

  129. D. Kozen. On the representation of dynamic algebras II. Technical Report RC8290, IBM Thomas J. Watson Research Center, May 1980.

    Google Scholar 

  130. D. Kozen. A representation theorem for models of *-free PDL. In Proc. 7th Colloq. Automata, Languages, and Programming, pages 351–362. EATCS, July 1980.

    Chapter  Google Scholar 

  131. D. Kozen. Logics of programs. Lecture notes, Aarhus University, Denmark, 1981.

    Google Scholar 

  132. D. Kozen. On induction vs. *-continuity. In Kozen, editor, Proc. Workshop on Logic of Programs, volume 131 of Lecture Notes in Computer Science, pages 167–176, New York, 1981. Springer-Verlag.

    Google Scholar 

  133. D. Kozen. On the expressiveness of μ. Manuscript, 1981.

    Google Scholar 

  134. D. Kozen. Semantics of probabilistic programs. J. Comput. Syst. Sci., 22:328–350, 1981.

    Article  Google Scholar 

  135. D. Kozen. Results on the propositional μ-calculus. In Proc. 9th Int. Colloq. Automata, Languages, and Programming, pages 348–359, Aarhus, Denmark, July 1982. EATCS.

    Chapter  Google Scholar 

  136. D. Kozen. Results on the propositional μ-calculus. Theor. Comput. Sci., 27:333–354, 1983.

    Article  Google Scholar 

  137. D. Kozen. A Ramsey theorem with infinitely many colors. In Lenstra, Lenstra, and van Emde Boas, editors, Dopo Le Parole, pages 71–72. University of Amsterdam, Amsterdam, May 1984.

    Google Scholar 

  138. D. Kozen. A probabilistic PDL. J. Comput. Syst. Sci., 30(2):162–178, April 1985.

    Article  Google Scholar 

  139. D. Kozen. A finite model theorem for the propositional μ-calculus. Studia Logica, 47(3):233–241, 1988.

    Article  Google Scholar 

  140. D. Kozen. On Kleene algebras and closed semirings. In Rovan, editor, Proc. Math. Found. Comput. Sci., volume 452 of Lecture Notes in Computer Science, pages 26–47, Banska-Bystrica, Slovakia, 1990. Springer-Verlag.

    Google Scholar 

  141. D. Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. In Proc. 6th Symp. Logic in Comput. Sci., pages 214–225, Amsterdam, July 1991. IEEE.

    Google Scholar 

  142. D. Kozen. The Design and Analysis of Algorithms. Springer-Verlag, New York, 1991.

    Google Scholar 

  143. D. Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. Infor. and Comput., 110(2):366–390, May 1994.

    Article  Google Scholar 

  144. D. Kozen. On action algebras. In J. van Eijck and A. Visser, editors, Logic and Information Flow, pages 78–88. MIT Press, 1994.

    Google Scholar 

  145. D. Kozen. Kleene algebra with tests and commutativity conditions. In T. Margaria and B. Steffen, editors, Proc. Second Int. Workshop Tools and Algorithms for the Construction and Analysis of Systems (TACAS’96), volume 1055 of Lecture Notes in Computer Science, pages 14–33, Passau, Germany, March 1996. Springer-Verlag.

    Chapter  Google Scholar 

  146. D. Kozen. Automata and Computability. Springer-Verlag, New York, 1997.

    Book  Google Scholar 

  147. D. Kozen. Kleene algebra with tests. Transactions on Programming Languages and Systems, 19(3):427–443, May 1997.

    Article  Google Scholar 

  148. D. Kozen. On the complexity of reasoning in Kleene algebra. In Proc. 12th Symp. Logic in Comput. Sci., pages 195–202, Los Alamitos, Ca., June 1997. IEEE.

    Google Scholar 

  149. D. Kozen. Typed Kleene algebra. Technical Report 98–1669, Computer Science Department, Cornell University, March 1998.

    Google Scholar 

  150. D. Kozen. On Hoare logic and Kleene algebra with tests. In Proc. Conf. Logic in Computer Science (LICS’99), pages 167–172. IEEE, July 1999.

    Google Scholar 

  151. D. Kozen. On Hoare logic, Kleene algebra, and types. Technical Report 99–1760, Computer Science Department, Cornell University, July 1999. Abstract in: Abstracts of 11th Int. Congress Logic, Methodology and Philosophy of Science, Ed. J. Cachro and K. Kijania-Placek, Krakow, Poland, August 1999, p. 15. To appear in: Proc. 11th Int. Congress Logic, Methodology and Philosophy of Science, ed. P. Gardenfors, K. Kijania-Placek and J. Wolenski, Kluwer.

    Google Scholar 

  152. Daniel Krob. A complete system of B-rational identities. Theoretical Computer Science, 89(2):207–343, October 1991.

    Article  Google Scholar 

  153. W. Kuich and A. Salomaa. Semirings, Automata, and Languages. Springer-Verlag, Berlin, 1986.

    Book  Google Scholar 

  154. W. Kuich. The Kleene and Parikh theorem in complete semirings. In T. Ottmann, editor, Proc. 14th Colloq. Automata, Languages, and Programming, volume 267 of Lecture Notes in Computer Science, pages 212–225, New York, 1987. EATCS, Springer-Verlag.

    Chapter  Google Scholar 

  155. R. E. Ladner. Unpublished, 1977.

    Google Scholar 

  156. L. Lamport. “Sometime” is sometimes “not never”. Proc. 1th Symp. Princip. Prog. Lang., pages 174–185, 1980.

    Google Scholar 

  157. D. Lehmann and S. Shelah. Reasoning with time and chance. Infor. and Control, 53(3):165–198, 1982.

    Article  Google Scholar 

  158. H. R. Lewis and C. H. Papadimitriou. Elements of the Theory of Computation. Prentice Hall, 1981.

    Google Scholar 

  159. R. J. Lipton. A necessary and sufficient condition for the existence of Hoare logics. In Proc. 18th Symp. Found. Comput. Sci., pages 1–6. IEEE, 1977.

    Google Scholar 

  160. D. C. Luckham, D. Park, and M. Paterson. On formalized computer programs. J. Comput. Syst. Sci., 4:220–249, 1970.

    Article  Google Scholar 

  161. A. Mader. Verification of Modal Properties Using Boolean Equation Systems. PhD thesis, Fakultt fr Informatik, Technische Universitt Mnchen, September 1997.

    Google Scholar 

  162. J. A. Makowsky and I. Sain. On the equivalence of weak second-order and nonstandard time semantics for various program verification systems. In Proc. 1st Symp. Logic in Comput. Sci., pages 293–300. IEEE, 1986.

    Google Scholar 

  163. J. A. Makowsky. Measuring the expressive power of dynamic logics: an application of abstract model theory. In Proc. 7th Int. Colloq. Automata Lang. Prog., volume 80 of Lect. Notes in Comput. Sci., pages 409–421. Springer-Verlag, 1980.

    Google Scholar 

  164. J. A. Makowsky and M. L. Tiomkin. Probabilistic propositional dynamic logic. Manuscript, 1980.

    Google Scholar 

  165. Z. Manna and A. Pnueli. Verification of concurrent programs: temporal proof principles. In D. Kozen, editor, Proc. Workshop on Logics of Programs, volume 131 of Lect. Notes in Comput. Sci., pages 200–252. Springer-Verlag, 1981.

    Google Scholar 

  166. Z. Manna and A. Pnueli. Specification and verification of concurrent programs by ?-automata. In Proc. 14th Symp. Principles of Programming Languages, pages 1–12. ACM, January 1987.

    Google Scholar 

  167. Z. Manna. Mathematical Theory of Computation. McGraw-Hill, 1974.

    Google Scholar 

  168. W. S. McCulloch and W. Pitts. A logical calculus of the ideas immanent in nervous activity. Bull. Math. Biophysics, 5:115–143, 1943.

    Article  Google Scholar 

  169. K. Mehlhorn. Graph Algorithms and NP-Completeness, volume II of Data Structures and Algorithms. Springer-Verlag, 1984.

    Google Scholar 

  170. A. R. Meyer and J. Y. Halpern. Axiomatic definitions of programming languages: a theoretical assessment. J. Assoc. Comput. Mach., 29:555–576, 1982.

    Article  Google Scholar 

  171. A. R. Meyer and R. Parikh. Definability in dynamic logic. J. Comput. Syst. Sci., 23:279–298, 1981.

    Article  Google Scholar 

  172. A. R. Meyer and J. Tiuryn. A note on equivalences among logics of programs. In D. Kozen, editor, Proc. Workshop on Logics of Programs, volume 131 of Lect. Notes in Comput. Sci., pages 282–299. Springer-Verlag, 1981.

    Google Scholar 

  173. A. R. Meyer and J. Tiuryn. Equivalences among logics of programs. Journal of Computer and Systems Science, 29:160–170, 1984.

    Article  Google Scholar 

  174. A. R. Meyer and K. Winklmann. Expressing program looping in regular dynamic logic. Theor. Comput. Sci., 18:301–323, 1982.

    Article  Google Scholar 

  175. A. R. Meyer, R. S. Streett, and G. Mirkowska. The deducibility problem in propositional dynamic logic. In E. Engeler, editor, Proc. Workshop Logic of Programs, volume 125 of Lect. Notes in Comput. Sci., pages 12–22. Springer-Verlag, 1981.

    Chapter  Google Scholar 

  176. G. L. Miller. Riemann’s hypothesis and tests for primality. J. Comput. Syst. Sci., 13:300–317, 1976.

    Article  Google Scholar 

  177. G. Mirkowska. On formalized systems of algorithmic logic. Bull. Acad. Polon. Sci. Ser. Sci. Math. Astron. Phys., 19:421–428, 1971.

    Google Scholar 

  178. G. Mirkowska. Algorithmic logic with nondeterministic programs. Fund. Informaticae, 111:45–64, 1980.

    Google Scholar 

  179. G. Mirkowska. PAL—propositional algorithmic logic. In E. Engeler, editor, Proc. Workshop Logic of Programs, volume 125 of Lect. Notes in Comput. Sci., pages 23–101. Springer-Verlag, 1981.

    Chapter  Google Scholar 

  180. G. Mirkowska. PAL—propositional algorithmic logic. Fund. Infor-maticae, IV:675–760, 1981.

    Google Scholar 

  181. C. Morgan, A. McIver, and K. Seidel. Probabilistic predicate transformers. ACM Trans. Programming Languages and Systems, 8(1): 1–30, 1999.

    Google Scholar 

  182. Y. N. Moschovakis. Elementary Induction on Abstract Structures. North-Holland, 1974.

    Google Scholar 

  183. D. E. Muller, A. Saoudi, and P. E. Schupp. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are de-cidable in exponential time. In Proc. 3rd Symp. Logic in Computer Science, pages 422–427. IEEE, July 1988.

    Google Scholar 

  184. I. Németi. Every free algebra in the variety generated by the repre-sentable dynamic algebras is separable and representable. Manuscript, 1980.

    Google Scholar 

  185. I. Németi. Nonstandard dynamic logic. In D. Kozen, editor, Proc. Workshop on Logics of Programs, volume 131 of Lect. Notes in Comput. Sci., pages 311–348. Springer-Verlag, 1981.

    Google Scholar 

  186. K. C. Ng and A. Tarski. Relation algebras with transitive closure, abstract 742–02–09. Notices Amer. Math. Soc, 24:A29–A30, 1977.

    Google Scholar 

  187. K. C. Ng. Relation Algebras with Transitive Closure. PhD thesis, University of California, Berkeley, 1984.

    Google Scholar 

  188. H. Nishimura. Sequential method in propositional dynamic logic. Acta Informatica, 12:377–400, 1979.

    Article  Google Scholar 

  189. H. Nishimura. Descriptively complete process logic. Acta Informatica, 14:359–369, 1980.

    Article  Google Scholar 

  190. D. Niwinski. The propositional μ-calculus is more expressive than the propositional dynamic logic of looping. University of Warsaw, 1984.

    Google Scholar 

  191. R. Parikh and A. Mahoney. A theory of probabilistic programs. In E. Clarke and D. Kozen, editors, Proc. Workshop on Logics of Programs, volume 164 of Lect. Notes in Comput. Sci., pages 396–402. Springer-Verlag, 1983.

    Google Scholar 

  192. R. Parikh. The completeness of propositional dynamic logic. In Proc. 7th Symp. on Math. Found. of Comput. Sci., volume 64 of Lect. Notes in Comput. Sci., pages 403–415. Springer-Verlag, 1978.

    Google Scholar 

  193. R. Parikh. A decidability result for second order process logic. In Proc. 19th Symp. Found. Comput. Sci., pages 177–183. IEEE, 1978.

    Google Scholar 

  194. R. Parikh. Propositional dynamic logics of programs: a survey. In E. Engeler, editor, Proc. Workshop on Logics of Programs, volume 125 of Lect. Notes in Comput. Sci., pages 102–144. Springer-Verlag, 1981.

    Chapter  Google Scholar 

  195. R. Parikh. Propositional game logic. In Proc. 23rd IEEE Symp. Foundations of Computer Science, 1983.

    Google Scholar 

  196. D. Park. Finiteness is μ-ineffable. Theor. Comput. Sci., 3:173–181, 1976.

    Article  Google Scholar 

  197. M. S. Paterson and C. E. Hewitt. Comparative schematol-ogy. In Record Project MA C Conf. on Concurrent Systems and Parallel Computation, pages 119–128. ACM, 1970.

    Google Scholar 

  198. J. P. Pecuchet. On the complementation of Büchi automata. Theor. Comput. Sci., 47:95–98, 1986.

    Article  Google Scholar 

  199. D. Peleg. Communication in concurrent dynamic logic. J. Comput. Sys. Sci., 35:23–58, 1987.

    Article  Google Scholar 

  200. D. Peleg. Concurrent dynamic logic. J. Assoc. Comput. Mach., 34(2):450–479, 1987.

    Article  Google Scholar 

  201. D. Peleg. Concurrent program schemes and their logics. Theor. Comput. Sci., 55:1–45, 1987.

    Article  Google Scholar 

  202. W. Peng and S. Purushothaman Iyer. A new type of pushdown-tree automata on infinite trees. Int. J. of Found. of Comput. Sci., 6(2): 169–186, 1995.

    Article  Google Scholar 

  203. G. L. Peterson. The power of tests in propositional dynamic logic. Technical Report 47, Comput. Sci. Dept., Univ. of Rochester, 1978.

    Google Scholar 

  204. A. Pnueli. The temporal logic of programs. In Proc. 18th Symp. Found. Comput. Sci., pages 46–57. IEEE, 1977.

    Google Scholar 

  205. V. R. Pratt. Semantical considerations on Floyd-Hoare logic. In Proc. 17th Symp. Found. Comput. Sci., pages 109–121. IEEE, 1976.

    Google Scholar 

  206. V. R. Pratt. A practical decision method for propositional dynamic logic. In Proc. 10th Symp. Theory of Comput, pages 326–337. ACM, 1978.

    Google Scholar 

  207. V. R. Pratt. Dynamic algebras: examples, constructions, applications. Technical Report TM-138, MIT/LCS, July 1979.

    Google Scholar 

  208. V. R. Pratt. Models of program logics. In Proc. 20th Symp. Found. Comput. Sci., pages 115–122. IEEE, 1979.

    Google Scholar 

  209. V. R. Pratt. Process logic. In Proc. 6th Symp. Princip. Prog. Lang., pages 93–100. ACM, 1979.

    Google Scholar 

  210. V. R. Pratt. Dynamic algebras and the nature of induction. In Proc. 12th Symp. Theory of Comput., pages 22–28. ACM, 1980.

    Google Scholar 

  211. V. R. Pratt. A near-optimal method for reasoning about actions. J. Comput. Syst. Sci., 20(2):231–254, 1980.

    Article  Google Scholar 

  212. V. R. Pratt. A decidable μ-calculus: preliminary report. In Proc. 22nd Symp. Found. Comput. Sci., pages 421–427. IEEE, 1981.

    Google Scholar 

  213. V. R. Pratt. Using graphs to understand PDL. In D. Kozen, editor, Proc. Workshop on Logics of Programs, volume 131 of Lect. Notes in Comput. Sci., pages 387–396. Springer-Verlag, 1981.

    Google Scholar 

  214. V. Pratt. Dynamic algebras as a well-behaved fragment of relation algebras. In D. Pigozzi, editor, Proc. Conf. on Algebra and Computer Science, volume 425 of Lecture Notes in Computer Science, pages 77–110, Ames, Iowa, June 1988. Springer-Verlag.

    Google Scholar 

  215. V. Pratt. Action logic and pure induction. In J. van Eijck, editor, Proc. Logics in AI: European Workshop JELIA’90, volume 478 of Lecture Notes in Computer Science, pages 97–120, New York, September 1990. Springer-Verlag.

    Google Scholar 

  216. M. O. Rabin and D. S. Scott. Finite automata and their decision problems. IBM J. Res. Develop., 3(2):115–125, 1959.

    Article  Google Scholar 

  217. M. O. Rabin. Probabilistic algorithms for testing primality. J. Number Theory, 12:128–138, 1980.

    Article  Google Scholar 

  218. L. H. Ramshaw. Formalizing the analysis of algorithms. PhD thesis, Stanford Univ., 1981.

    Google Scholar 

  219. H. Rasiowa and R. Sikorski. Mathematics of Metamathematics. Polish Scientific Publishers, PWN, 1963.

    Google Scholar 

  220. V. N. Redko. On defining relations for the algebra of regular events. Ukrain. Mat. Z., 16:120–126, 1964. In Russian.

    Google Scholar 

  221. J. Reif. Logics for probabilistic programming. In Proc. 12th Symp. Theory of Comput., pages 8–13. ACM, 1980.

    Google Scholar 

  222. H. Rogers. Theory of Recursive Functions and Effective Computability. McGraw-Hill, 1967.

    Google Scholar 

  223. S. Safra. On the complexity of ω-automata. In Proc. 29th Symp. Foundations of Comput. Sci., pages 319–327. IEEE, October 1988.

    Google Scholar 

  224. J. Sakarovitch. Kleene’s theorem revisited: A formal path from Kleene to Chomsky. In A. Kelemenova and J. Keleman, editors, Trends, Techniques, and Problems in Theoretical Computer Science, volume 281 of Lecture Notes in Computer Science, pages 39–50, New York, 1987. Springer-Verlag.

    Chapter  Google Scholar 

  225. A. Salomaa. Two complete axiom systems for the algebra of regular events. J. Assoc. Comput. Mach., 13(1):158–169, January 1966.

    Article  Google Scholar 

  226. A. Salwicki. Formalized algorithmic languages. Bull. Acad. Polon. Sci. Ser. Sci. Math. Astron. Phys., 18:227–232, 1970.

    Google Scholar 

  227. A. Salwicki. Algorithmic logic: a tool for investigations of programs. In Butts and Hintikka, editors, Logic Foundations of Mathematics and Computability Theory, pages 281–295. Reidel, 1977.

    Chapter  Google Scholar 

  228. V.Y. Sazonov. Polynomial computability and recursivity in finite domains. Elektronische Informationsverarbeitung und Kibernetik, 16:319–323, 1980.

    Google Scholar 

  229. D. S. Scott and J. W. de Bakker. A theory of programs. IBM Vienna, 1969.

    Google Scholar 

  230. R. Segala and N. Lynch. Probabilistic simulations for probabilistic processes. In Proc. CONCUR’94, volume 836 of Lecture Notes in Comput. Sci., pages 481–496. Springer-Verlag, 1994.

    Google Scholar 

  231. K. Segerberg. A completeness theorem in the modal logic of programs (preliminary report). Not. Amer. Math. Soc, 24(6):A-552, 1977.

    Google Scholar 

  232. J. R. Shoenfield. Mathematical Logic. Addison-Wesley, 1967.

    Google Scholar 

  233. H. Sholz. Ein ungelöstes Problem in der symbolischen Logik. The Journal of Symbolic Logic, 17:160, 1952.

    Google Scholar 

  234. A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. In Proc. 14th Symp. Theory of Comput., pages 159–168. ACM, 1982.

    Google Scholar 

  235. A. P. Sistla, M. Y. Vardi, and P. Wolper. The complementation problem for Büchi automata with application to temporal logic. Theor. Comput. Sci., 49:217–237, 1987.

    Article  Google Scholar 

  236. O. Sokolsky and S. Smolka. Incremental model checking in the modal μ-calculus. In D. Dill, editor, Proc. Conf. Computer Aided Verification, volume 818 of Lect. Notes in Comput. Sci., pages 352–363. Springer, June 1994.

    Google Scholar 

  237. B. Steffen, T. Margaria, A. Classen, V. Braun, R. Nisius, and M. Reitenspiess. A constraint oriented service environment. In T. Margaria and B. Steffen, editors, Proc. Second Int. Workshop Tools and Algorithms for the Construction and Analysis of Systems (TACAS’96), volume 1055 of Lect. Notes in Comput. Sci., pages 418–421. Springer, March 1996.

    Chapter  Google Scholar 

  238. C. Stirling and D. Walker. Local model checking in the modal μ-calculus. In Proc. Int. Joint Conf. Theory and Practice of Software Develop. (TAPSOFT89), volume 352 of Lect. Notes in Comput. Sci., pages 369–383. Springer, March 1989.

    Google Scholar 

  239. C. Stirling. Modal and temporal logics. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, pages 477–563. Clarendon Press, 1992.

    Google Scholar 

  240. L. J. Stockmeyer and A. R. Meyer. Word problems requiring exponential time. In Proc. 5th Symp. Theory of Computing, pages 1–9, New York, 1973. ACM.

    Google Scholar 

  241. A. P. Stolboushkin and M. A. Taitslin. Deterministic dynamic logic is strictly weaker than dynamic logic. Infor. and Control, 57:48–55, 1983.

    Article  Google Scholar 

  242. A.P. Stolboushkin. Regular dynamic logic is not interpretable in deterministic context-free dynamic logic. Information and Computation, 59:94–107, 1983.

    Google Scholar 

  243. A.P. Stolboushkin. Some complexity bounds for dynamic logic. In Proc. 4th Symp. Logic in Comput. Sci., pages 324–332. IEEE, June 1989.

    Google Scholar 

  244. R. Streett and E. A. Emerson. The propositional μ-calculus is elementary. In Proc. 11th Int. Colloq. on Automata Languages and Programming, pages 465–472. Springer, 1984. Lect. Notes in Comput. Sci. 172.

    Chapter  Google Scholar 

  245. R. S. Streett. Propositional dynamic logic of looping and converse. In Proc. 13th Symp. Theory of Comput., pages 375–381. ACM, 1981.

    Google Scholar 

  246. R. S. Streett. Propositional dynamic logic of looping and converse is elementarily decidable. Infor. and Control, 54:121–141, 1982.

    Article  Google Scholar 

  247. R. S. Streett. Fixpoints and program looping: reductions from the propositional μ-calculus into propositional dynamic logics of looping. In R. Parikh, editor, Proc. Workshop on Logics of Programs, volume 193 of Lect. Notes in Comput. Sci., pages 359–372. Springer-Verlag, 1985.

    Chapter  Google Scholar 

  248. R. Streett. Fixpoints and program looping: reductions from the propositional μ-calculus into propositional dynamic logics of looping. In Parikh, editor,Proc. Workshop on Logics of Programs 1985, pages 359–372. Springer, 1985. Lect. Notes in Comput. Sci. 193.

    Google Scholar 

  249. R. E. Tarjan. A unified approach to path problems. J. Assoc. Comput. Mach., pages 577–593, 1981.

    Google Scholar 

  250. H. Thiele. Wissenschaftstheoretische Untersuchungen in algorithmischen sprachen. In Theorie der Graphschemata-Kalkale Veb Deutscher Verlag der Wissenschaften. Berlin, 1966.

    Google Scholar 

  251. W. Thomas. Languages, automata, and logic. Technical Report 9607, Christian-Albrechts-Universität Kiel, May 1997.

    Google Scholar 

  252. J. Tiuryn and P. Urzyczyn. Some relationships between logics of programs and complexity theory. In Proc. 24th Symp. Found. Comput. Sci., pages 180–184. IEEE, 1983.

    Google Scholar 

  253. J. Tiuryn and P. Urzyczyn. Remarks on comparing expressive power of logics of programs. In Chytil and Koubek, editors, Proc. Math. Found. Comput. Sci., volume 176 of Lect. Notes in Comput. Sci., pages 535–543. Springer-Verlag, 1984.

    Google Scholar 

  254. J. Tiuryn and P. Urzyczyn. Some relationships between logics of programs and complexity theory. Theor. Comput. Sci., 60:83–108, 1988.

    Article  Google Scholar 

  255. J. Tiuryn. A survey of the logic of effective definitions. In E. Engeler, editor, Proc. Workshop on Logics of Programs, volume 125 of Lect. Notes in Comput. Sci., pages 198–245. Springer-Verlag, 1981.

    Chapter  Google Scholar 

  256. J. Tiuryn. Unbounded program memory adds to the expressive power of first-order programming logics. In Proc. 22nd Symp. Found. Comput. Sci., pages 335–339. IEEE, 1981.

    Google Scholar 

  257. J. Tiuryn. Unbounded program memory adds to the expressive power of first-order programming logics. Infor. and Control, 60:12–35, 1984.

    Article  Google Scholar 

  258. J. Tiuryn. Higher-order arrays and stacks in programming: an application of complexity theory to logics of programs. In Gruska and Rovan, editors, Proc. Math. Found. Comput. Sci., volume 233 of Lect. Notes in Comput. Sci., pages 177–198. Springer-Verlag, 1986.

    Google Scholar 

  259. J. Tiuryn. A simplified proof of DDL > DL. Information and Computation, 81:1–12, 1989.

    Article  Google Scholar 

  260. V. Trnkova and J. Reiterman. Dynamic algebras which are not Kripke structures. In Proc. 9th Symp. on Math. Found. Comput. Sci., pages 528–538, 1980.

    Google Scholar 

  261. A. M. Turing. On computable numbers with an application to the Entscheidungsproblem. Proc. London Math. Soc, 42:230–265, 1936. Erratum: Ibid., 43 (1937), pp. 544–546.

    Google Scholar 

  262. P. Urzyczyn. A necessary and sufficient condition in order that a Herbrand interpretation be expressive relative to recursive programs. Information and Control, 56:212–219, 1983.

    Article  Google Scholar 

  263. P. Urzyczyn. “During” cannot be expressed by “after”. Journal of Computer and System Sciences, 32:97–104, 1986.

    Article  Google Scholar 

  264. P. Urzyczyn. Deterministic context-free dynamic logic is more expressive than deterministic dynamic logic of regular programs. Fundamenta Informaticae, 10:123–142, 1987.

    Google Scholar 

  265. P. Urzyczyn. Logics of programs with Boolean memory. Fundamenta Informaticae, XI:21–40, 1988.

    Google Scholar 

  266. M. K. Valiev. Decision complexity of variants of propositional dynamic logic. In Proc. 9th Symp. Math. Found. Comput. Sci., volume 88 of Lect. Notes in Comput. Sci., pages 656–664. Springer-Verlag, 1980.

    Google Scholar 

  267. P. van Emde Boas. The connection between modal logic and algorithmic logics. In Symp. on Math. Found. of Comp. Sci., pages 1–15, 1978.

    Google Scholar 

  268. M. Y. Vardi and L. Stockmeyer. Improved upper and lower bounds for modal logics of programs: preliminary report. In Proc. 17th Symp. Theory of Comput, pages 240–251. ACM, May 1985.

    Google Scholar 

  269. M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. 1st Symp. Logic in Computer Science, pages 332–344. IEEE, June 1986.

    Google Scholar 

  270. M. Y. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. J. Comput. Syst. Sci., 32:183–221, 1986.

    Article  Google Scholar 

  271. M. Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proc. 26th Symp. Found. Comput. Sci., pages 327–338. IEEE, October 1985.

    Google Scholar 

  272. M. Y. Vardi. The taming of the converse: reasoning about two-way computations. In R. Parikh, editor, Proc. Workshop on Logics of Programs, volume 193 of Lect. Notes in Comput. Sci., pages 413–424. Springer-Verlag, 1985.

    Chapter  Google Scholar 

  273. M. Y. Vardi. Verification of concurrent programs: the automata-theoretic framework. In Proc. 2nd Symp. Logic in Comput. Sci., pages 167–176. IEEE, June 1987.

    Google Scholar 

  274. M. Vardi. Linear vs. branching time: a complexity-theoretic perspective. In Proc. 13th Symp. Logic in Comput. Sci., pages 394–405. IEEE, 1998.

    Google Scholar 

  275. M. Y. Vardi. Reasoning about the past with two-way automata. In Proc. 25th Int. Colloq. Automata Lang. Prog., volume 1443 of Lect. Notes in Comput. Sci., pages 628–641. Springer-Verlag, July 1998.

    Google Scholar 

  276. I. Walukiewicz. Completeness result for the propositional μ-calculus. In Proc. 8th IEEE Symp. Logic in Comput. Sci., June 1993.

    Google Scholar 

  277. I. Walukiewicz. Completeness of Kozen’s axiomatisation of the propositional μ-calculus. In Proc. 10th Symp. Logic in Comput. Sci., pages 14–24. IEEE, June 1995.

    Google Scholar 

  278. I. Walukiewicz. Completeness of Kozen’s axiomatisation of the propositional μ-calculus. Infor. and Comput., 157(1–2): 142–182, February-March 2000.

    Article  Google Scholar 

  279. M. Wand. A new incompleteness result for Hoare’s system. J. Assoc. Comput. Mach., 25:168–175, 1978.

    Article  Google Scholar 

  280. P. Wolper. Temporal logic can be more expressive. In Proc. 22nd Symp. Foundations of Computer Science, pages 340–348. IEEE, 1981.

    Google Scholar 

  281. P. Wolper. Temporal logic can be more expressive. Infor. and Control, 56:72–99, 1983.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. The Weizmann Institute of Science, Rehovot, Israel

    David Harel

  2. Cornell University, Ithaca, New York, USA

    Dexter Kozen

  3. The University of Warsaw, Warsaw, Poland

    Jerzy Tiuryn

Authors
  1. David Harel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dexter Kozen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jerzy Tiuryn
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. King’s College, London, UK

    D. M. Gabbay

  2. Centrum für Informations- und Sprachverarbeitung, Ludwig-Maximilians-Universität München, Germany

    F. Guenthner

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer Science+Business Media Dordrecht

About this chapter

Cite this chapter

Harel, D., Kozen, D., Tiuryn, J. (2001). Dynamic Logic. In: Gabbay, D.M., Guenthner, F. (eds) Handbook of Philosophical Logic. Handbook of Philosophical Logic, vol 4. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-0456-4_2

Download citation

  • DOI: https://doi.org/10.1007/978-94-017-0456-4_2

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-90-481-5877-5

  • Online ISBN: 978-94-017-0456-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation