Deciding branching time logic

Publisher Website
Google Scholar
Abstract
In this paper we study the full branching time logic (CTL*) in which a path quantifier, either A (“for all paths-&-rdquo;) 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 &ohgr;-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.

This publication has 0 references indexed in Scilit: