Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
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.
Ehrenfeucht, A. and P. Zeiger, 1976, Complexity measures for regular expressions, J. Comp. Syst. Sci. 12, 2, 134–146.
Floyd, R.W., 1967, Assigning meanings to programs, 19 th AMS Symp. Applied Math. American Math. Society, Providence, R.I. 19–31.
Fischer, M.J. and R. E. Ladner, 1979, Propositional dynamic logic of regular programs, J. Comp. Syst. Sci. 18, 2, 194–211.
Harel, D., 1983, Dynamic logic, In Handbook of Philosophical Logic, Vol. II, Reidel Publishing Company, Holland/USA, in press.
Harel, D. and V. R. Pratt, 1978, Nondeterminism in logics of programs, 5 th AC Symp. on Principles of Programming Languages, 203–213.
Hoare, C. A. R., 1969, An axiomatic basis for computer programing, Comm. Assoc. Mach. 12, 576–583.
Kozen, D. and R. Parikh, 1981, An elementary proof of the completeness of PDL, Theor. Comput. Science 14, 113–118.
Pratt, V. R., 1976, Semantical considerations on Floyd-Hoare logic, 17 th IEEE Symp. on Foundations of Computer Science, 119–121.
Pratt, V. R., 1979, Models of program logics, 20 th IEEE Symp. on Foundations o Computer Science, 115–122.
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.
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.
Streett, R. S., 1983, Propositional dynamic logic of looping and converse is elementarily decidable. Inf. and Cont., in press.
Wolper, P., 1981, Temporal logic can be more expressive, 22 nd IEEE Symp. on Foundations of Computer Science, 340–348.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1983 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Harel, D., Sherman, R. (1983). Propositional dynamic logic of flowcharts. In: Karpinski, M. (eds) Foundations of Computation Theory. FCT 1983. Lecture Notes in Computer Science, vol 158. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-12689-9_104
Download citation
DOI: https://doi.org/10.1007/3-540-12689-9_104
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-12689-8
Online ISBN: 978-3-540-38682-7
eBook Packages: Springer Book Archive