If you are looking for a (hard) open problem to work on, then this is one that you might want to pit your wits against. For the moment, the best result I am aware of on the characterization of the structural complexity of the model checking problem for the mu-calculus is by Marcin Jurdzinski. In this paper, Marcin showed that the problem is in the intersection of UP and coUP.
UP is the class of decision problems solvable by an NP machine such that
- If the answer is 'yes,' exactly one computation path accepts.
- If the answer is 'no,' all computation paths reject.