1

Hello,

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.

flag
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 2012 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 2012 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 2012 at 21:51

Your Answer

Get an OpenID
or

Browse other questions tagged or ask your own question.