1: \begin{abstract}

2:   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 \Cs, the star-free closure operator outputs the least class closed under Boolean operations and language concatenation, and containing all languages of \Cs 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.

3: 

4:   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.

5: \end{abstract}

6: