This paper analyzes the computational complexity of the model checking problem for Higher Order Fixpoint Logic - the modal μ-calculus enriched with a typed A-calculus. It is hard for every level of the elementary time/space hierarchy and in elementary time/space when restricted to formulas of bounded type order.
['Martin Lange', 'Rafał Somla']
The complexity of model checking higher order fixpoint logic