A Classic Open Problem

I just attended Jan Friso Groote's second talk during his inspirational visit to Reykjavík University. In this talk, entitled On using and proving modal formulas for analyzing processes, Jan Friso used some mCRL2 models of strategic games he developed during his stay to motivate the use of the modal mu-calculus (with data) to express properties of processes. He also showed how to do model checking for the modal mu-calculus via Gaussian elimination, and mentioned the tantalizing open problem of whether model checking for the modal mu-calculus is in P.

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.