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 μ-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

1. 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.
2. BMP81.M. Ben-Ari. Z. Manna. A. Pnueli, "The Ternpond Logic of Branching Time", Proc. 8th ACM Syrup, on Principles of Programming Languages, Wi!liam,~burg, 1981, pp. 164-176.
3. 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.
4. Ch74.Y, Choueka, "'l'hcorics of Aut()mata on ~- Tnpes: A Simplified Approach", J. Computer and System Sciences. 8 (1974), pp. 117-141.
5. CKS81.A.K. Challdra, D.C. Kozen, L.J. Stockmeyer, "Altcn~ation", Y. ACM 2:~1 (1981), pp. 114-133.
6. EH82.E.A. Eme ,r,~on, J.Y. i ln'lpcrn,"Dccision Proce(lurcs and Expressivellcss in the Temporal Logic of Branching Time", Proc. 14th ACM 3~mp. on Theory of Computing, San FranciscO, 1982, pp. 169-180.
7. EH83.E.A. Ememon, J.Y. ll~lpern,""Sometimcs" and "Not Never" Revisited: On Branching vs. Linear Time", Proc, lOth ACM Syrup. on Principles of Programming Language~; 1983.
8. 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.
9. Em85.E.A, Emerson, "Automata, tableaux, and temporal logics", to appear in Proc. Workshop on Logics of Programs, Brooklyn, June 1985.
10. ESi84.E.A. Emerson, A.P. Sistla,"Deciding Branching Time Logic", Proc. 16th ACM Syrup. on Theory of Comput#tg Washington, 1984, pp. 14-24.
11. 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.
12. FL79.M.J. Fisher, R.E. Ladner, "Propositional Dynamic Logic of Regular Programs", jr Computer and System $cience~; 18(2), 1979, pp. 194-211.
13. Ga76.D.M., Gabbay, "Investigation in Modal and Tense Logic'; Reidel, }976.
14. Ha83.Z. I labnsinski. "DccMability Problems In Logics of Programs'; Ph.D. Di,,~ertation, Dept. of Mathcmatics, Technical University of Poznan, 1983.
15. 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.
16. 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.
17. HS83.D. ~larcl. R. Shemlan, "Looping vs. Repeating in Dynamic Logic", Information und Control 55(1982), pp. 175-192.
18. Ko83.D. Kozcn, "Results on the Prolx~silional.p.- Calculus", Theoretical Computer Science. 27(1983), pp. 333-354.
19. McN66.R. McNaughton, "Tesling and Generating Infinite Sequences by a Finite Automaton", Information and Control 9 (1966), pp. 521-530
20. 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.
21. Ni80.H. Nishimura, "Descriptively Complete Process Logic", Acta Infotmatica, 14 (1980), pp. 359-369.
22. 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.
23. Pa80.R. Parikh, "Propositional Logics of Programs: Systems, Models and Complexity", Proc, 7th ACM Syrup. on Principles of Programming Languages. Ltrs Vegas, 1980, pp. 186-192.
24. Pa83.R. Parikh, "Propositional Game Logic", Proc. 25 IEEE Syrup. on lCbundations of Computer Science. Tuscon, 1983, pp. 195-200.
25. Pn81.A. Pnueli, "The Temporal Ix)vie of Concurrent Programs", Theoretical Computer Science 13(1981), pp. 45-60.
26. PS83.A. Pnueli, R. Sherman, "Propositional Dynamic Logic of l~ooping Flowcharts', Technical Report, Wcizmann Institute, Rchovot, Israel, 1983.
27. 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.
28. 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.
29. 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,
30. 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.
31. RS59.M.O. R~lbin, D. Scott, "Finite Automata and their Decision Problems", IBM J. Res. & Dev., 3(2), 1959, pp 114-125.
32. Sh84.R. Sherman, "Variants of Propositional Dynamic Logic," Ph.D. Dissertation, The Weizmann Inst. of Science, 1984.
33. SPH84.R. Sherman, A. Pnueli, D. Harel, "Is the Interesting Part of' Process I.ogic Uninteresting?'', SIAM J. Computing 13(1984), pp. 825- 839.
34. St80.R.S. Streett, "A propositional Dynamic Logic for Reasoning about Proglam Divergence", M.Sc. Thesis, M IT, 1980.
35. St82.R.S. Streett, "Propositional Dynamic Logic of Looping and Converse is elementarily decidable'', Information and Control 54(1982), pp. 121-141.
36. SVW85.A.P. Sistla, M.Y. Vardi, P. Wolper, "The Complementation Problem fi)r Buchi Automata with Applications to Temporal Logic", to appear in Proc. 12th Int. Colloq. on Automata, Languages and Programming. 1985.
37. Va84.M.Y. Vardi, "On deterministic w-automata'; to appear.
38. Va85.M.Y. Vardi, "The Taming of Converse: Rea-. soning about Two-Way G an~putations", to appear in !'roe. Workshop on Logics of Programs, Brooklyn, June 1985.
39. VW83.M.Y. Vardi, I'. Wolper, "Yel another process logic", i'roc. Workshop on Logics of Programs 1983. Springcr-Vcdag, Lecture Notes in Computer Science - vol. 164 (Clarke and Kozen, eds.), pp. 501-512.
40. VW84.M.Y. Vardi. P. Wolper, "Automata-theoretic Techni(lues Ibr Modal Logics of Programs", 'rim 16th ACM Syrup. on 7'heory of Comput- Ing. W;}shinglon, 1984, pp. 446--456.

Index Terms

• Computing methodologies

  • Artificial intelligence

    • Search methodologies

      • Discrete space search

      • Game tree search

• Social and professional topics

  • Professional topics

    • Management of computing and information systems

      • Implementation management

        • Pricing and resource allocation

      • Software management

• Software and its engineering

  • Software creation and management

• Theory of computation

  • Logic

    • Programming logic

  • Semantics and reasoning

    • Program reasoning