ON PROJECTIVE AND SEPARABLE PROPERTIES

A language L over the Cartesian product of component alphabets is call ed projective if it is closed under projections, i.e., together with e ach word alpha is an element of L, it contains all the words that have the same projections up to stuttering as cc. We prove that the projec tive languages are precisely the languages obtained using parallel com position and intersection from stuttering-closed component languages i n each of the following classes of languages: regular, star-free regul ar, omega-regular and star-free omega-regular. Languages of these clas ses can also be seen as properties of various temporal logics which ar e used to specify properties of concurrent systems. In particular, the star-free omega-regular languages coincide with properties expressed using Propositional Linear Temporal Logic. Some uses of projective pro perties for specification and verification of programs are studied.