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.


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: DOI