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.
No takes yet. Share an insight, caveat, or question.
Emerson et al. (1984) studied this question.