As most of you already know, in model checking most linear-time properties are either safety properties or liveness properties. A linear time property is usually described with an omega-regular language that tells exactly which traces satisfy the property.
To check if a property is actually a safety property, one method would be to calculate the closure of the property and check whether its closure (as a set of infinite words) and the property itself (also as a set of infinite words) are equal. To calculate the closure it is important to calculate the set on finite prefixes of the omega-regular language that describes the property.
I would like to know how to calculate the finite prefixes set of an omega-regular language. The language in question is described by an omega-regular expression.
Stated differently, what are the rules to calculate the finite prefixes set? I need it because I want to determine whether this language characterizes a safety property.