# Propositional dynamic logic of flowcharts

## 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.

## Keywords

Regular Expression Expressive Power Atomic Formula Finite Automaton Exponential Time## Preview

Unable to display preview. Download preview PDF.

## References

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