Deciding branching time logic

ABSTRACT

In this paper we study the full branching time logic (CTL*) in which a path quantifier, either A (“for all paths-&-rdquo;) or E (-&-ldquo;for some path”), prefixes an assertion composed of arbitrary combinations of the usual linear time operators F (“sometime”), G (“always”), X (“nexttime”), and U (“until”). We show that the problem of determining if a CTL* formula is satisfiable in structure generated by a binary relation is decidable in triple exponential time. The decision procedure exploits the special structure of the finite state &ohgr;-automata for linear temporal formulae which allows them to be determinized with only a single exponential blowup in size. We also compare the expressive power of tree automata with CTL* augmented by quantified auxillary propositions.

REFERENCES

• 1: Karl Raymond Abrahamson, Decidability and expressiveness of logics of processes, 1980
• 2: 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]
• 3: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 4: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.117-126, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567080]
• 5: Emerson, E. A., and Clarke, E. M., Using Branching Time Logic to Synthesize Synchronization Skeletons, Science of Computer Programming, vol. 2, pp. 241-266, 1982.
• 6: 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]
• 7: 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]
• 8: Emerson, E. A., Alternative Semantics for Temporal Logics, Theoretical Computer Science, vol. 26, pp. 121-130, 1983.
• 9: Fischer, M. J., and Ladner, R. E, Propositional Dynamic Logic of Regular Programs, JCSS vol. 18, pp. 194-211, 1979.
• 10: Dov Gabbay , Amir Pnueli , Saharon Shelah , Jonathan Stavi, On the temporal analysis of fairness, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567462]
• 11: Hossley, R., and Rackoff, C, The Emptiness Problem For Automata on Infinite Trees, Proc. 13th IEEE Symp. Switching and Automata Theory, pp. 121-124, 1972.
• 12: Leslie Lamport, "Sometime" is sometimes "not never": on the temporal logic of programs, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-185, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567463]
• 13: McNaughton, R., Testing and Generating Infinite Sequences by a Finite Automaton, Information and Control, vol. 9, 1966.
• 14: Zohar Manna , Amir Pnueli, The Modal Logic of Programs, Proceedings of the 6th Colloquium, on Automata, Languages and Programming, p.385-409, July 16-20, 1979
• 15: Meyer, A. R., Weak Monadic Second Order Theory of Successor is Not Elementary Recursive, Boston Logic Colloquium, Springer-Verlag Lecture Notes in Mathematics 453, 1974.
• 16: Pnueli, A., The Temporal Logic of Programs, 19th Annual Symp. on Foundations of Computer Science, 1977.
• 17: Pnueli, A., The Temporal Logic of Concurrent Programs, Theoretical Computer Science, V13, pp. 45-60, 1981.
• 18: Pnueli, A. and Sherman, R., Personal Communication, 1983.
• 19: Rabin, M., Decidability of Second order Theories and Automata on Infinite Trees, Trans. Amer. Math. Society, vol. 141, pp. 1-35, 1969.
• 20: Rabin, M., Automata on Infinite Trees and the Synthesis Problem, Hebrew Univ., Tech. Report no. 37, 1970.
• 21: Rabin, M., personal communication.
• 22: Rabin, M. and Scott, D., Finite Automata and their Decision Problems, IBM J. Research and Development, vol. 3, pp. 114-125, 1959.
• 23: Robert S. Streett, Propositional Dynamic Logic of looping and converse, Proceedings of the thirteenth annual ACM symposium on Theory of computing, p.375-383, May 11-13, 1981, Milwaukee, Wisconsin, United States [doi>10.1145/800076.802492]
• 24: Wolper, P., A Translation from Full Branching Time Temporal Logic to One Letter Propositional Dynamic Logic with Looping, unpublished manuscript, 1982.
• 25: 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

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Temporal logic

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming

  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)

General Terms:
Languages, Theory