  We introduce PHFL, a probabilistic extension of higher-order fixpoint logic,
which can also be regarded as a higher-order extension of probabilistic
temporal logics such as PCTL and the $\mu^p$-calculus. We show that PHFL is
strictly more expressive than the $\mu^p$-calculus, and that the PHFL
model-checking problem for finite Markov chains is undecidable even for the
$\mu$-only, order-1 fragment of PHFL. Furthermore the full PHFL is far more
expressive: we give a translation from Lubarsky's $\mu$-arithmetic to PHFL,
which implies that PHFL model checking is $\Pi^1_1$-hard and $\Sigma^1_1$-hard.
As a positive result, we characterize a decidable fragment of the PHFL
model-checking problems using a novel type system.
