Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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.

share|improve this question
    
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
1  
Could you tell us what are safety and liveness properties? –  Joel David Hamkins Apr 8 at 23:25
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.