Stefan Dziembowski, Marcin Jurdzi{\'n}ski, and Damian Niwi{\'n}ski
``On the Expression Complexity of the Modal Mu-Calculus Model Checking''

Abstract:

We prove that checking validity of the modal mu-calculus formulas
in a fixed model (expression complexity) is PTIME-hard.
The result holds in fact for the alternation free fragment of the
modal mu-calculus and a 2-state labelled transition system.