  Higher-order modal fixpoint logic (HFL) is a higher-order extension of the
modal mu-calculus, and strictly more expressive than the modal mu-calculus. It
has recently been shown that various program verification problems can
naturally be reduced to HFL model checking: the problem of whether a given
finite state system satisfies a given HFL formula. In this paper, we propose a
novel algorithm for HFL model checking: it is the first practical algorithm in
that it runs fast for typical inputs, despite the hyper-exponential worst-case
complexity of the HFL model checking problem. Our algorithm is based on
Kobayashi et al.'s type-based characterization of HFL model checking, and was
inspired by a saturation-based algorithm for HORS model checking, another
higher-order extension of model checking. We prove the correctness of the
algorithm and report on an implementation and experimental results.
