3
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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.) $\endgroup$ – Tara Brough Mar 17 '12 at 13:09
  • $\begingroup$ Thank you Tara. Your approach gave me a wider perspective. However, I wonder if there is a less-involved solution for this problem. $\endgroup$ – HJosef Mar 19 '12 at 20:33
  • 1
    $\begingroup$ 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.) $\endgroup$ – Tara Brough Mar 19 '12 at 21:51
  • 1
    $\begingroup$ Could you tell us what are safety and liveness properties? $\endgroup$ – Joel David Hamkins Apr 8 '14 at 23:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.