# zbMATH — the first resource for mathematics

Deciding full branching time logic. (English) Zbl 0593.03007
Summary: In this paper the full branching time logic $$(CTL^*)$$ is studied. It has basic modalities consisting of a path quantifier, either A (”for all paths”) of E (”for some path”), followed by an arbitrary linear time assertion composed of unrestricted combinations of the usual linear temporal operators F (”sometime”), G (”always”), X (”nexttime”), and U (”until”). It is shown that the problem of determining if a $$CTL^*$$ formula is satisfiable in a structure generated by a binary relation is decidable in triple exponential time. The decision procedure exploits the special structure of the finite state $$\omega$$-automata for linear temporal formulae which allows them to be determinized with only a single exponential blowup in size. Also the expressive power of tree automata is compared with that of $$CTL^*$$ augmented by quantified auxilliary propositions.

##### MSC:
 03B45 Modal logic (including the logic of norms) 03B25 Decidability of theories and sets of sentences 03D05 Automata and formal grammars in connection with logical questions
Full Text: