Question about $\omega$-regular languages

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.

• I think it's easy, given a Büchi automaton, to describe the finite prefixes of words accepted by the automaton. So perhaps you could first find a Büchi automaton accepting your language? (I think it's straightforward to do that from the $\omega$-regular expression.) – Tara Brough Mar 17 '12 at 13:09
• Thank you Tara. Your approach gave me a wider perspective. However, I wonder if there is a less-involved solution for this problem. – HJosef Mar 19 '12 at 20:33
• If I could see the specific example you are looking at, I might have more to say. In complete generality I could only suggest the approach I would probably take. (I don't know much about $\omega$-regular languages, but in general I prefer working with automata to other representations of languages.) – Tara Brough Mar 19 '12 at 21:51
• Could you tell us what are safety and liveness properties? – Joel David Hamkins Apr 8 '14 at 23:25