×

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
PDFBibTeX XMLCite
Full Text: DOI