PDL Is the Bisimulation-Invariant Fragment of Weak Chain Logic

We introduce a new class of parity automata which, on trees, captures the expressive power of weak chain logic. This logic is a variant of monadic second-order logic which quantifies over finite chains. Using this new tool, we show that the bisimulation-invariant fragment of weak chain logic is equivalent to propositional dynamic logic.