BTL2 and the expressive power of ECTL+

We show that ECTL+, the classical extension of CTL with fairness properties, is expressively equivalent to BTL2, a natural fragment of the monadic logic of order. BTL2 is the branching-time logic with arbitrary quantification over paths, and where path formulae are restricted to quantifier depth 2 first-order formulae in the monadic logic of order. This result, linking ECTL+ to a natural fragment of the monadic logic of order, provides a characterization that other branching-time logics, e.g., CTL, lack. We then go on to show that ECTL+ and BTL2 are not finitely based (i.e., they cannot be defined by a finite set of temporal modalities) and that their model-checking problems are of the same complexity.