  We use the algebraic framework for languages of infinite trees introduced in
[4] to derive effective characterisations of various temporal logics, in
particular the logic EF (a fragment of CTL) and its counting variant cEF.
