A practical decision method for propositional dynamic logic (Preliminary Report)

ABSTRACT

We give a new characterization of the set of satisfiable formulae of propositional dynamic logic (PDL) based on the method of tableaux. From it we derive a heuristically efficient goal-directed proof procedure and a complete axiom system for PDL. The proof procedure illustrates a striking connection between natural deduction and symbolic execution. The completeness proof for the axiom system incorporates a method for the automatic synthesis of invariants. We also augment DL with new modalities throughout, during, and preserves, supply a new semantic foundation for DL programs, and show how to extend the satisfiability characterizations for PDL to throughout.

REFERENCES

• 1: Berman, F. and M. Paterson. Test-Free Propositional Dynamic Logic is Strictly Weaker than PDL. T.R. 977-10-09-, Dept. of Computer Science, Univ. of Washington, Seattle. Nov. 1977.
• 2: Beth, E.W. The Foundations of Mathematics. North Holland, 1959.
• 3: Robert L. Constable, On the theory of programming logics, Proceedings of the ninth annual ACM symposium on Theory of computing, p.269-285, May 04-04, 1977, Boulder, Colorado, United States [doi>10.1145/800105.803417]
• 4: Edsger W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, v.18 n.8, p.453-457, Aug. 1975 [doi>10.1145/360933.360975]
• 5: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 6: Elgot, C.C. Structured Programming With and Without GO TO Statements. IEEE Transactions on Software Engineering, SE-2, 1, 41-53, March 1976.
• 7: Engeler, E. Algorithmic properties of structures. Math. Sys. Thy. 1, 183-195. 1967.
• 8: Michael J. Fischer , Richard E. Ladner, Propositional modal logic of programs, Proceedings of the ninth annual ACM symposium on Theory of computing, p.286-294, May 04-04, 1977, Boulder, Colorado, United States [doi>10.1145/800105.803418]
• 9: Gabbay, D. Axiomatizations of Logics of Programs. Manuscript, under cover dated Nov. 1977.
• 10: Gentzen, G. Untersuchungen ueber das Logische Schliessen, Math. Zeitschr, 39,176-210.
• 11: Seymour Ginsburg , Edwin H. Spanier, Mappings of languages by two-tape devices, Journal of the ACM (JACM), v.12 n.3, p.423-434, July 1965 [doi>10.1145/321281.321294]
• 12: D. Harel , A. R. Meyer , V. R. Pratt, Computability and completeness in logics of programs (Preliminary Report), Proceedings of the ninth annual ACM symposium on Theory of computing, p.261-268, May 04-04, 1977, Boulder, Colorado, United States [doi>10.1145/800105.803416]
• 13: David Harel , Vaughan R. Pratt, Nondeterminism in logics of programs, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.203-213, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512782]
• 14: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 15: Hoare, C.A.R. Some Properties of Nondeterministic Computations. The Queen's Univ., Belfast. 1976
• 16: Hintikka, K.J.J. Form and content in quantification theory. Acta Philosophica Fennica 8, 7-55. 1955.
• 17: Kripke, S.A. Semantical analysis of modal logic I: normal modal propositional calculi. Zeitschr. f Math. Logik und Grundlagen d. Math., 9, 67-96. 1963.
• 18: Litvintchouk, S.D. and V.R. Pratt. A Proof-checker for Dynamic Logic. Proc. 5th Int. Joint Conf. on AI, 559.-558, Boston, Aug. 1977.
• 19: Parikh, R. A Completeness Result for PDL. Manuscript dated 11/29/77.
• 20: Pratt, V.R. Semantical Considerations on Floyd-Hoare Logic. Proc. 17th Ann. IEEE Symp. on Foundations of Comp. Sci., 109-121. 1976.
• 21: Vaughan R. Pratt, The competence/performance dichotomy in programming preliminary report, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.194-200, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512968]
• 22: Salwicki, A. Formalized Algorithmic Languages. Bull Acad. Pol. Sci., Ser. Sci. Math. Astr. Phys. Vol. 18. No. 5. 1970.
• 23: Sogerberg, K. A Completeness Theorem in the Modal Logic of Programs. Preliminary report. Notices of the AMS, 24, 6, A-552. Oct. 1977.
• 24: Smullyan, R.M. First-Order Logic. Springer-Verlag, Berlin. 1968.
• 25: Ben Wegbreit, The synthesis of loop predicates, Communications of the ACM, v.17 n.2, p.102-113, Feb. 1974 [doi>10.1145/360827.360850]