Propositional dynamic logic of flowcharts

  • D. Harel
  • R. Sherman
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 158)


Following a suggestion of Pratt, we consider propositional dynamic logic in which programs are nondeterministic finite automata over atomic programs and tests (i.e., flowcharts), rather than regular expressions. While the resulting version of PDL, call it APDL, is clearly equivalent in expressive power to PDL, it is also (in the worst case) exponentially more succinct. In particular, deciding its validity problem by reducing it to that of PDL leads to a double exponential time procedure, although PDL itself is decidable in exponential time.

We present an elementary combined proof of the completeness of a simple axiom system for APDL and decidability of the validity problem in exponential time. The results are thus stronger than those for PDL since PDL can be encoded in APDL with no additional cost, and the proofs simpler, since induction on the structure of programs is virtually eliminated. Our axiom system for APDL relates to the PDL system just as Floyd's proof method for partial correctness relates to Hoare's.


Regular Expression Expressive Power Atomic Formula Finite Automaton Exponential Time 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BHP]
    Ben-Ari, M., J. Y. Halpern and A. Pnueli, 1982, Deterministic propositional dynamic logic: finite models, complexity and completeness, J. Comp. Syst. Sci. 25, 402–417.Google Scholar
  2. [EZ]
    Ehrenfeucht, A. and P. Zeiger, 1976, Complexity measures for regular expressions, J. Comp. Syst. Sci. 12, 2, 134–146.Google Scholar
  3. [F]
    Floyd, R.W., 1967, Assigning meanings to programs, 19 th AMS Symp. Applied Math. American Math. Society, Providence, R.I. 19–31.Google Scholar
  4. [FL]
    Fischer, M.J. and R. E. Ladner, 1979, Propositional dynamic logic of regular programs, J. Comp. Syst. Sci. 18, 2, 194–211.Google Scholar
  5. [Ha]
    Harel, D., 1983, Dynamic logic, In Handbook of Philosophical Logic, Vol. II, Reidel Publishing Company, Holland/USA, in press.Google Scholar
  6. [HP]
    Harel, D. and V. R. Pratt, 1978, Nondeterminism in logics of programs, 5 th AC Symp. on Principles of Programming Languages, 203–213.Google Scholar
  7. [Ho]
    Hoare, C. A. R., 1969, An axiomatic basis for computer programing, Comm. Assoc. Mach. 12, 576–583.Google Scholar
  8. [KP]
    Kozen, D. and R. Parikh, 1981, An elementary proof of the completeness of PDL, Theor. Comput. Science 14, 113–118.Google Scholar
  9. [P1]
    Pratt, V. R., 1976, Semantical considerations on Floyd-Hoare logic, 17 th IEEE Symp. on Foundations of Computer Science, 119–121.Google Scholar
  10. [P2]
    Pratt, V. R., 1979, Models of program logics, 20 th IEEE Symp. on Foundations o Computer Science, 115–122.Google Scholar
  11. [P3]
    Pratt, V. R., 1981, Using graphs to understand PDL, Workshop on logics of programs, (D. Kozen ed.), Lect. Notes in Comput. Sci. 131, Springer-Verlag, New York, 387–396.Google Scholar
  12. [SH]
    Sherman., R. and D. Harel, 1983, A combined proof of one exponential decidability and completeness for PDL, 1 st Int. Workshop on Found. Theoret. Comput. Sci., GTI, Paderborn, 221–233.Google Scholar
  13. [S]
    Streett, R. S., 1983, Propositional dynamic logic of looping and converse is elementarily decidable. Inf. and Cont., in press.Google Scholar
  14. [W]
    Wolper, P., 1981, Temporal logic can be more expressive, 22 nd IEEE Symp. on Foundations of Computer Science, 340–348.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1983

Authors and Affiliations

  • D. Harel
    • 1
  • R. Sherman
    • 1
  1. 1.Department of Applied MathematicsThe Weizmann Institute of ScienceRehovotIsrael

Personalised recommendations