E. Allen Emerson
A. Prasad Sistla
ABSTRACT
In this paper we study the full branching time logic (CTL*) in which a path quantifier, either A (“for all paths”) 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 ω-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.
- 1.Abrahamson, K., Decidability and Expressiveness of Logics of Processes, PhD Thesis, Univ. of Washington, 1980. Google Scholar
Digital Library
- 2.Ben-Ari, M., Manna, Z., and Pnueli, A., The Temporal Logic of Branching Time. 8th Annual ACM Symp. on Principles of Programming Languages, 1981. Google ScholarDigital Library
- 3.Clarke, E. M., and Emerson, E. A., Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic, Proceedings of the IBM Workshop on Logics of Programs, Springer-Verlag Lecture Notes in Computer Science 131, 1981. Google ScholarDigital Library
- 4.Clarke, E. M., Emerson, E. A., and Sistla, A. P., Automatic Verification of Finite State Concurrent Programs: A Practical Approach, POPL83. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 6.Emerson, E. A., and Halpern, J. Y., Decision Procedures and Expressiveness in the Temporal Logic of Branching Time. 14th Annual ACM Symp. on Theory of Computing, 1982. Google ScholarDigital Library
- 7.Emerson, E. A., and Halpern, J. Y., 'Sometimes' and 'Not Never' Revisited: On Branching versus Linear Time. POPL83. Google ScholarDigital Library
- 8.Emerson, E. A., Alternative Semantics for Temporal Logics, Theoretical Computer Science, vol. 26, pp. 121-130, 1983.Google ScholarCross Ref
- 9.Fischer, M. J., and Ladner, R. E, Propositional Dynamic Logic of Regular Programs, JCSS vol. 18, pp. 194-211, 1979.Google ScholarCross Ref
- 10.Gabbay, D., Pnueli, A., et al., The Temporal Analysis of Fairness. 7th Annual ACM Symp. on Principles of Programming Languages, 1980. Google ScholarDigital Library
- 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.Google Scholar
- 12.Lamport, L., "Sometimes" is Sometimes "Not Never." 7th Annual ACM Symp. on Principles of Programming Languages, 1980. Google ScholarDigital Library
- 13.McNaughton, R., Testing and Generating Infinite Sequences by a Finite Automaton, Information and Control, vol. 9, 1966.Google Scholar
- 14.Manna, Z., and Pnueli, A., The modal logic of programs, Proc. 6th Int. Colloquium on Automata, Languages, and Programming, Springer-Verlag Lecture Notes in Computer Science 71, pp. 385-410, 1979. Google ScholarDigital Library
- 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.Google Scholar
- 16.Pnueli, A., The Temporal Logic of Programs, 19th Annual Symp. on Foundations of Computer Science, 1977.Google Scholar
- 17.Pnueli, A., The Temporal Logic of Concurrent Programs, Theoretical Computer Science, V13, pp. 45-60, 1981.Google ScholarCross Ref
- 18.Pnueli, A. and Sherman, R., Personal Communication, 1983.Google Scholar
- 19.Rabin, M., Decidability of Second order Theories and Automata on Infinite Trees, Trans. Amer. Math. Society, vol. 141, pp. 1-35, 1969.Google Scholar
- 20.Rabin, M., Automata on Infinite Trees and the Synthesis Problem, Hebrew Univ., Tech. Report no. 37, 1970.Google Scholar
- 21.Rabin, M., personal communication.Google Scholar
- 22.Rabin, M. and Scott, D., Finite Automata and their Decision Problems, IBM J. Research and Development, vol. 3, pp. 114-125, 1959.Google ScholarDigital Library
- 23.Streett, R., Propositional Dynamic Logic of Looping and Converse (PhD Thesis), MIT Lab for Computer Science, TR-263, 1981. (a short version appears in STOC81). Google ScholarDigital Library
- 24.Wolper, P., A Translation from Full Branching Time Temporal Logic to One Letter Propositional Dynamic Logic with Looping, unpublished manuscript, 1982.Google Scholar
- 25.Vardi, M., and Wolper, P., Yet Another Process Logic, CMU Workshop on Logics of Programs, Springer-Verlag, 1983. Google ScholarDigital Library
Index Terms
- Deciding branching time logic
Recommendations
Memoryful Branching-Time Logic
LICS '06: Proceedings of the 21st Annual IEEE Symposium on Logic in Computer ScienceTraditional branching-time logics such as CTL* are memoryless: once a path in the computation tree is quantified at a given node, the computation that led to that node is forgotten. Recent work in planning suggests that CTL* cannot easily express ...
Linear time datalog and branching time logic
Logic-based artificial intelligenceWe survey recent results about the relation between Datalog and temporal verification logics. Datalog is a well-known database query language relying on the logic programming paradigm. We introduce Datalog LITE, a fragment of Datalog with Well-founded ...
Branching time? pruning time!
IJCAR'12: Proceedings of the 6th international joint conference on Automated ReasoningThe full branching time logic ctl* is a well-known specification logic for reactive systems. Its satisfiability and model checking problems are well understood. However, it is still lacking a satisfactory sound and complete axiomatisation. The only ...
Comments