On projective and separable properties

AbstractA language L over the Cartesian product of component alphabets is called projective if it is closed under projections, i.e., together with each word α ∈ L, it contains all the words that have the same projections up to stuttering as α. We prove that the projective languages are precisely the languages obtained using parallel composition and intersection from stuttering-closed component languages in each of the following classes of languages: regular, star-free regular, ω-regular and star-free ω-regular. Languages of these classes can also be seen as properties of various temporal logics which are used to specify properties of concurrent systems. In particular, the star-free ω-regular languages coincide with properties expressed using Propositional Linear Temporal Logic. Some uses of projective properties for specification and verification of programs are studied