一句话：研究带原子的模态 μ-演算扩展：轨道有限结构上模型检测可判定且对应奇偶博弈，但可满足性不可判定。
本文研究将模态 μ-演算扩展到带原子集合的设定，并考察其基本性质。作者定义标量与向量两种带原子 μ-演算语法，分析其模型检测、博弈对应与可满足性。关键结果是：在轨道有限结构上模型检测可判定，且与奇偶博弈的对应关系成立；但可满足性问题不可判定。作者进一步刻画原子增强 μ-演算的表达力限制，说明其表达力取决于所用原子结构以及基本语法与向量语法之间的选择。
We study an extension of modal $\mu$-calculus to sets with atoms and we 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 expressive limitations of atom-enriched $\mu$-calculi, and explain how their expressive power depends on the structure of atoms used, and on the choice between basic or vectorial syntax.