Mu-calculi with atoms

I will show an extension of modal mu-calculus to sets with atoms, developed jointly with Mateusz Łełyk. Model checking is decidable there, and a correspondence to parity games holds. On the other hand, satisfiability becomes undecidable. I will also show expressive limitations of the atom-enriched calculus. I will conclude with an infuriating open problem.