Abstract
This paper begins with the problem of sharpening our understanding of PDL. The position we take here is that PDL, which is ordinarily defined using regular operations on programs, is better understood in terms of finite state automata. Accordingly we rederive some basic PDL results (finite model, deterministic exponential satisfiability) in terms of automata. As corollaries to this we obtain answers to the following open questions. (i) What is the time complexity of satisfiability for propositional flowgraph logic? (ii) Can regular expressions be axiomatized equationally as succinctly as they can be represented with automata? We also show how converse and test relate to flowgraph operations.
The evidence to date strongly suggested that problem (i) should require double exponential time. We give a deterministic one-exponential bound, tight to within a polynomial. Two novel aspects of our algorithm are that it solves the problem by translation to modal logic with minimization, and that the concept of state is abstracted out of the algorithm. The tractability of satisfiability can be traced to two key properties of the definition of flowgraph operations. For (ii) we give for each flowgraph of size n a complete axiomatization of size a polynomail in n, by showing how to axiomatize matrix transitive closure equationally.
Our treatment of converse and test shows that they enjoy the same two key properties as flowgraph operations, permitting a uniform treatment of the bulk of the major flow-of-control constructs.
Preview
Unable to display preview. Download preview PDF.
Bibliography
Abrahamson, K., Decidability and Expressiveness of Logics of Processes, Ph.D. Thesis, TR #80-08-01, Dept. of Comp. Sci., U. of Wash., Seattle, 1980.
Ashcroft, E., and Z. Manna, Translating Program Schemas to While-Schemas, SIAM J. Comput., 4, 2, 125–146, June, 1975.
Dijkstra, E.W., A Discipline of Programming, Prentice-Hall. 1976
Ehrenfeucht, A., and P. Zeiger, Complexity Measures for Regular Expressions, JCSS, 12., 2, 134–146, April, 1976.
Fischer, M. J., and R. Ladner, Propositional Dynamic Logic of Regular Programs, JCSS, 18, 2, 194–211, April 1979.
Floyd, R. W., Assigning Meanings to Programs, In Mathematical Aspects of Computer Science (ed. J.T. Schwartz), 19–32, 1967.
Hoare, C.A.R., An Axiomatic Basis for Computer Programming, CACM 12, 576–580, 1969.
Kleene, S.C., Representation of Events in Nerve Nets, in Automata Studies, (eds. Shannon, C.E. and J. McCarthy), 3–40, Princeton University Press, Princeton, NJ, 1956.
Parikh, R., A Completeness Result for a Propositional Dynamic Logic, Lecture Notes in Computer Science No. 64, 403–415, Springer-Verlag, 1978. Also M.I.T. Laboratory for Computer Science Technical Memorandum No. 106, July 1978.
Pratt, V.R., Models of Program Logics, Proc. 20th IEEE Conference on Foundations of Computer Science, San Juan, PR, Oct. 1979.
Pratt, V.R., Dynamic Algebras: Examples, Constructions, Applications, MIT/LCS/TM-138, M.I.T. Laboratory for Computer Science, May 1979.
Pratt, V.R., Dynamic Algebras and the Nature of Induction, Proc. 12th ACM Symp. on Theory of Computing, 22–28, Los Angeles, CA, May, 1980.
Redko, V.N., On Defining Relations for the Algebra of Regular Events, (Russian), Ukrain. Mat. Z., 16, 120–126, 1964.
Segerberg, K., A Completeness Theorem in the Modal Logic of Programs, Preliminary report. Notices of the AMS, 24, 6, A-552. Oct. 1977.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1982 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pratt, V.R. (1982). Using graphs to understand PDL. In: Kozen, D. (eds) Logics of Programs. Logic of Programs 1981. Lecture Notes in Computer Science, vol 131. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0025792
Download citation
DOI: https://doi.org/10.1007/BFb0025792
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-11212-9
Online ISBN: 978-3-540-39047-3
eBook Packages: Springer Book Archive