Branching-depth hierarchies
===========================
We study the distinguishing and expressive power of branching temporal
logics with bounded nesting depth of path quantifiers. We define the
fragments CTL*_i and CTL_i of CTL* and CTL, where at most i nestings
of path quantifiers are allowed. path quantifiers in CTL* and CTL
formulas, respectively. We show that for all i > 0, the logic
CTL*_{i+1} has more distinguishing and expressive power than CTL*_i;
thus the branching-depth hierarchy is strict. We describe equivalence
relations H_i that capture CTL*_i: two states in a Kripke structure
are H_i-equivalent iff they agree on exactly all CTL*_i
formulas. While H_1 corresponds to trace equivalence, the limit of the
sequence H_1,H_2,... is Milner's bisimulation. These results are not
surprising, but they give rise to several interesting observations and
problems. In particular, while CTL* and CTL have the same
distinguishing power, this is not the case for CTL*_i and CTL_i. We
define the branching depth of a structure as the minimal index i for
which H_{i+1}=H_i. The branching depth indicates on the possibility of
using bisimulation instead of trace equivalence (and similarly for
simulation and trace containment). We show that while bisimulation can
be calculated in polynomial time, the problem of finding the branching
depth is PSPACE-complete.