Deciding full branching time logic. (English) Zbl 0593.03007

Emerson, E. Allen; Sistla, A. Prasad

Inf. Control 61, 175-201 (1984).

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

Keywords:

finite state omega-automata; modalities; path quantifier; decision procedure; tree automata