We introduce an operator on classes of regular languages, the star-free closure. Our motivation is to generalize standard results of automata theory within a unified framework. Given an arbitrary input class $C$, the star-free closure operator outputs the least class closed under Boolean operations and language concatenation, and containing all languages of $C$ as well as all finite languages. We establish several equivalent characterizations of star-free closure: in terms of regular expressions, first-order logic, pure future and future-past temporal logic, and recognition by finite monoids. A key ingredient is that star-free closure coincides with another closure operator, defined in terms of regular operations where Kleene stars are allowed in restricted~contexts. A consequence of this first result is that we can decide membership of a regular language in the star-free closure of a class whose separation problem is decidable. Moreover, we prove that separation itself is decidable for the star-free closure of any finite class, and of any class of group languages having itself decidable separation (plus mild additional properties). We actually show decidability of a stronger property, called covering.

翻译：我们引入正则语言类上的一个算子——星自由闭包。其动机是在统一框架内推广自动机理论的标准结果。给定任意输入类 $C$，星自由闭包算子输出在布尔运算与语言拼接下封闭、且包含 $C$ 中所有语言及所有有限语言的最小类。我们建立了星自由闭包的若干等价刻画：基于正则表达式、一阶逻辑、纯将来时态逻辑与将来-过去时态逻辑，以及有限幺半群识别。关键要素在于，星自由闭包与另一个在克莱尼星号受限制时允许使用的正则运算所定义的闭包算子相重合。这一首要结果的一个推论是：对于可判定分离问题的类，我们能判定其星自由闭包中正则语言的成员资格。此外，我们证明任意有限类的星自由闭包、以及任意自身拥有可判定分离性（加上温和附加性质）的群语言类的星自由闭包，其分离问题均可判定。实际上，我们证明了更强性质——覆盖——的可判定性。