  Our main contributions can be divided in three parts: (1) Fixpoint extensions
of first-order logic: we give a precise syntactic and semantic characterization
of the relationship between $\mathrm{FO(TC^1)}$ and $\mathrm{FO(LFP)}$; (2)
Automata and expressiveness on trees: we introduce a new class of parity
automata which, on trees, captures the expressive power of $\mathrm{FO(TC^1)}$
and WCL (weak chain logic). The latter logic is a variant of MSO which
quantifies over finite chains; and (3) Expressiveness modulo bisimilarity: we
show that PDL is expressively equivalent to the bisimulation-invariant fragment
of both $\mathrm{FO(TC^1)}$ and WCL. In particular, point (3) closes the open
problems of the bisimulation-invariant characterizations of PDL,
$\mathrm{FO(TC^1)}$ and WCL all at once.
