Improved upper and lower bounds for modal logics of programs

ABSTRACT

We describe novel techniques for establishing improved upper and lower bounds for modal logics of programs: 1) We introduce hybrid tree automata. These automata seems to be doubly exponential more powerful than Rabin tree automata but their emptiness problem is only exponentially harder (nondeterministic exponential time vs. nondeterministic polynomial time). The satisfiability problem for several logics is reducible to the emptiness problem for hybrid tree automata. Using this reduction we show that the satisfiability problems for Streett's delta-PDL. Kozen's &mgr;-calculus and Parikh's game logic are solvable in nondeterministic exponential time, and the satisfiability problem for Emerson and Halpern's CTL and Vardi and Wolper's process logic (YAPL) are solvable in nondeterministic doubly exponential time. 2) We encode Turing machine computations by Kripke structures where every state in the structure represents a single tape cell. This yields a deterministic doubly exponential time lower bound for CTL and YAPL. 3) For variants of CTL and YAPL that deal only with finite computations we prove completeness for deterministic doubly exponential time.

REFERENCES

• BHP82: M. Bcn-Ari, J.Y. Halpcrn, A. Pnucli, "Dcterministic Propositi()nal Dynamic Logic: Finite Models, Complcxily, and Complctcncss", ,/, Computer and System Science, 25(1982), pp. 402-417.
• BMP81: Mordechai Ben-Ari , Zohar Manna , Amir Pnueli, The temporal logic of branching time, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.164-176, January 26-28, 1981, Williamsburg, Virginia [doi>10.1145/567532.567551]
• Bu62: J.R. Buchi, "On a Decision Method in Restricted Scco~l~l Order Arithmetic", Proc. Int'l Congr. l,ngi~, M('/hod and /'hi/, &'i. 1960, Stnnli)rd University I'rcs,s. 1962, pp, 1-I2.
• Ch74: Y, Choueka, "'l'hcorics of Aut()mata on ~- Tnpes: A Simplified Approach", J. Computer and System Sciences. 8 (1974), pp. 117-141.
• CKS81: A.K. Challdra, D.C. Kozen, L.J. Stockmeyer, "Altcn~ation", Y. ACM 2:~1 (1981), pp. 114-133.
• EH82: E. Allen Emerson , Joseph Y. Halpern, Decision procedures and expressiveness in the temporal logic of branching time, Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.169-180, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802190]
• EH83: E. Allen Emerson , Joseph Y. Halpern, "Sometimes" and "not never" revisited: on branching versus linear time (preliminary report), Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.127-140, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567081]
• EL85: E.A. Emerson, C.L. Lei, "Modalities for Modal Checking: Branching Time Strikes Back". to appear in Proc. lOth ,'tCM Syrup. on Principles of Programming Languagex 1985.
• Em85: E. Allen Emerson, Automata, Tableaux and Temporal Logics (Extended Abstract), Proceedings of the Conference on Logic of Programs, p.79-88, June 17-19, 1985
• ESi84: E. Allen Emerson , A. Prasad Sistla, Deciding branching time logic, Proceedings of the sixteenth annual ACM symposium on Theory of computing, p.14-24, December 1984 [doi>10.1145/800057.808661]
• ESt84: E.A. Emerson, A. P. Streett, "An Elementary Decision Procedure for the/,t-calculus", Proc. llth Int. Colloq. on ,,lutomat~ Languages and Programming 1984, Lecture Notes in Computer Science, Springer-Verlag.
• FL79: M.J. Fisher, R.E. Ladner, "Propositional Dynamic Logic of Regular Programs", jr Computer and System $cience~; 18(2), 1979, pp. 194-211.
• Ga76: D.M., Gabbay, "Investigation in Modal and Tense Logic'; Reidel, }976.
• Ha83: Z. I labnsinski. "DccMability Problems In Logics of Programs'; Ph.D. Di,,~ertation, Dept. of Mathcmatics, Technical University of Poznan, 1983.
• HKP82: D. {larel, D. Kozen, R. Parikh, "Proc'e~s I~gic: Expre~iveness, Deci&lbility, Completenc~,~". Journal of Computer and System Science 25, 2 (1982), pp. 144-170.
• HR72: R. l lt)~slcy, C.W. Rackoll; "q'hc Eillptinu,'ss Problem for Automala OI1 Infinite 'fix:ca", Proc. 13th IEEE Syrup. on Switching and lutomata Theory, 1972, pp. 121-124.
• HS83: D. ~larcl. R. Shemlan, "Looping vs. Repeating in Dynamic Logic", Information und Control 55(1982), pp. 175-192.
• Ko83: D. Kozcn, "Results on the Prolx~silional.p.- Calculus", Theoretical Computer Science. 27(1983), pp. 333-354.
• McN66: R. McNaughton, "Tesling and Generating Infinite Sequences by a Finite Automaton", Information and Control 9 (1966), pp. 521-530
• Me75: A.R. Meyer. "Weak Monadic Second Order Theory of Successor is not Elementary Recursire", Proc. Logic Colloquium 1975, Lecture Notes in Mathematics, vol. 453, Springer- Verlag, pp. 132-154.
• Ni80: H. Nishimura, "Descriptively Complete Process Logic", Acta Infotmatica, 14 (1980), pp. 359-369.
• Pa78: R. Parikh, "A Decidability Result for a Secol~d Order Process Logic", Proceedings 19lh IEEE Symposium on Foundations' of Computer Science, Ann Arlx>r, October 1978.
• Pa80: Rohit Parikh, Propositional logics of programs: systems, models, and complexity, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.186-192, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567464]
• Pa83: R. Parikh, "Propositional Game Logic", Proc. 25 IEEE Syrup. on lCbundations of Computer Science. Tuscon, 1983, pp. 195-200.
• Pn81: A. Pnueli, "The Temporal Ix)vie of Concurrent Programs", Theoretical Computer Science 13(1981), pp. 45-60.
• PS83: A. Pnueli, R. Sherman, "Propositional Dynamic Logic of l~ooping Flowcharts', Technical Report, Wcizmann Institute, Rchovot, Israel, 1983.
• Pr76: V.R. I'ratt, "Semantical Considerations on Floyd-Itoare l_x)gic", Proc. 17th IEEE Syrup. on Pbundations of Cotnpttler Science, } iouston, 1976, pp. 109-121.
• Ra69: M.O. Rabin. "l)ecid;llfilily {ff Second Order 'lh~orics ;~lltl Atalolnal;i t)l! iilfinit~ 'l'rccs", Trans. A MS, 141 (I 909), pp. 1--35.
• Ra70: M.O. Rabin, "Weakly Definable Relations and Special Automata", Proc. Symp. Math. Logic and Foundations of Set Theory (Y. Bar-ltillel, cd.), North-llolland, 1970, pp. 1-23,
• Ra72: M.O. Rabill, "Automata on Infinite Objects and Church's Problem", !'roc. Regional AM$ Conf. Series in Math. 13(197;2), pp. 1-22.
• RS59: M.O. R~lbin, D. Scott, "Finite Automata and their Decision Problems", IBM J. Res. & Dev., 3(2), 1959, pp 114-125.
• Sh84: R. Sherman, "Variants of Propositional Dynamic Logic," Ph.D. Dissertation, The Weizmann Inst. of Science, 1984.
• SPH84: R Sherman , A Pnueli , D Harel, Is the interesting part of process logic uninteresting? A translation from PL to PDL, SIAM Journal on Computing, v.13 n.4, p.825-839, Nov. 1984 [doi>10.1137/0213051]
• St80: R.S. Streett, "A propositional Dynamic Logic for Reasoning about Proglam Divergence", M.Sc. Thesis, M IT, 1980.
• St82: R.S. Streett, "Propositional Dynamic Logic of Looping and Converse is elementarily decidable'', Information and Control 54(1982), pp. 121-141.
• SVW85: A. Prasad Sistla , Moshe Y. Vardi , Pierre Wolper, The Complementation Problem for Büchi Automata with Applications to Temporal Logic (Extended Abstract), Proceedings of the 12th Colloquium on Automata, Languages and Programming, p.465-474, July 15-19, 1985
• Va84: M.Y. Vardi, "On deterministic w-automata'; to appear.
• Va85: Moshe Y. Vardi, The Taming of Converse: Reasoning about Two-way Computations, Proceedings of the Conference on Logic of Programs, p.413-423, June 17-19, 1985
• VW83: Moshe Y. Vardi , Pierre Wolper, Yet Another Process Logic (Preliminary Version), Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.501-512, June 06-08, 1983
• VW84: Moshe Y. Vardi , Pierre Wolper, Automata theoretic techniques for modal logics of programs: (Extended abstract), Proceedings of the sixteenth annual ACM symposium on Theory of computing, p.446-456, December 1984 [doi>10.1145/800057.808711]

INDEX TERMS

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

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.8 Problem Solving, Control Methods, and Search
          Subjects: Graph and tree search strategies

General Terms:
Algorithms, Theory, Verification