Propositional Dynamic Logic of looping and converse

ABSTRACT

Propositional Dynamic Logic can be extended to include both an infinitary iteration construct delta and a backtracking construct converse. The resulting logic does not satisfy the finite model property, but is nevertheless elementarily decidable. In order to establish this decidability result, deterministic two-way automata on infinite trees are defined and shown to be reducible to nondeterministic one-way automata on infinite trees. The decision procedure suggests a nonstandard semantics for the extended logic for which the finite model property does hold.

REFERENCES

• 1: M. J. Fischer and R. E. Ladner, "Propositional Dynamic Logic of Regular Programs", JCSS, 18, 194-211, 1979.
• 2: D. Gabbay, Axiomatizations of Logics of Programs, Unpublished manuscript, 1977.
• 3: R. Hossley and C. W. Rackoff, "The Emptiness Problem for Automata on Infinite Trees", 13th IEEE Symposium on Switching and Automata Theory, 121-124, 1972.
• 4: A. Meyer, "Weak Monadic Second Order Theory of Successor Is Not Elementary Recursive", Logic Colloquium, Springer-Verlag Lecture Notes in Math. 453, 1974.
• 5: Grazyna Mirkowska, Complete axiomatization of algorithmic properties of program schemes with bounded nondeterministic interpretations, Proceedings of the twelfth annual ACM symposium on Theory of computing, p.14-21, April 28-30, 1980, Los Angeles, California, United States [doi>10.1145/800141.804648]
• 6: Albert R. Meyer , Karl Winklmann, On the expressive power of Dynamic Logic (Preliminary Report), Proceedings of the eleventh annual ACM symposium on Theory of computing, p.167-175, April 30-May 02, 1979, Atlanta, Georgia, United States [doi>10.1145/800135.804410]
• 7: R. Parikh, "A Decidability Result for a Second Order Process Logic", 19th IEEE Symposium on Foundations of Computer Science, 177-183, 1978.
• 8: V. R. Pratt, "Semantical Considerations on Floyd-Hoare Logic", 17th IEEE Symposium on Foundations of Computer Science, 109-121, 1976.
• 9: V. R. Pratt, Applications of Modal Logic to Programming, MIT LCS Technical Memo TM-116, 1978.
• 10: V. R. Pratt, "Models of Program Logics", 20th IEEE Symposium on the Foundations of Computer Science. 115-122, 1979.
• 11: M. O. Rabin, "Decidability of Second Order Theories and Automata on Infinite Trees", Trans. of the Amer. Math. Soc., 141, 1-35, 1969.
• 12: M. O. Rabin, "Automata on Infinite Trees and the Synthesis Problem", Hebrew University Dept. of Mathematics Technical Report No. 37, 1970.
• 13: R. S. Streett, "Propositional Dynamic Logic and Program Divergence", M. S. thesis proposal, Dept. of EECS, MIT, 1979.
• 14: R. S. Streett, A Propositional Dynamic Logic for Reasoning About Program Divergence, M. S. thesis, Dept. of EECS, MIT, 1980.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)
      F.1.3 Complexity Measures and Classes
          Subjects: Reducibility and completeness
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS
      G.2.2 Graph Theory
          Subjects: Path and circuit problems

General Terms:
Languages, Theory