摘要：We introduce an extension of modal mu-calculus to sets with atoms and study its basic properties. Model checking is decidable on orbit-finite structures, and a correspondence to parity games holds. On the other hand, satisfiability becomes undecidable. We also show some limitations to the expressiveness of the calculus and argue that a naive way to remove these limitations results in a logic whose model checking is undecidable.
