0
$\begingroup$

I know LT Properties can be classified with classes Invariants, Safety Properties, Liveness Properties as in https://en.wikipedia.org/wiki/Linear_time_property. My question is, does this cover all possible LT properties and if so is there a proof to show that any property must be a member of one of these classes , and if not is there a counterexample.

$\endgroup$

1 Answer 1

1
$\begingroup$

As Wikipedia says,

not every property is a safety property or a liveness property (consider "a occurs exactly once")

The parenthetical gives an example of a property that is not a safety property, not a liveness property, and not an invariant.

$\endgroup$
6
  • $\begingroup$ Why is the 'occurs only once' not a safety property. My definition of safety property is that every trace not in the property has a bad prefix. So for example if it said "a occurs only once" then would it be the case that the trace that has no 'a' in it at all , say b^w, for that is it to say this has no bad prefix because any finite prefix will have no 'a' in it but this can be extended to something in the property easily. Have I got the right idea $\endgroup$
    – revision
    Commented Apr 30 at 13:40
  • $\begingroup$ @revision, Please check the quote more carefully. I wrote 'occurs exactly once', not 'occurs only once'. 'occurs exactly once' is not a safety property. $\endgroup$
    – D.W.
    Commented Apr 30 at 22:21
  • $\begingroup$ sorry for my misunderstanding but what is the difference between the two. If something occurs only once is that not the same thing as it occurs exactly once. Furthermore could you give a hint as to why "occurs exactly once" is not a safety property or point me to a resource. Thanks $\endgroup$
    – revision
    Commented May 1 at 23:00
  • 1
    $\begingroup$ @revision, Let $n$ count the number of times that $a$ occurs. 'occurs only once' might be interpreted as $n\le 1$, 'occurs exactly once' is $n=1$. '$a$ occurs exactly once' is not a safety property. $\endgroup$
    – D.W.
    Commented May 1 at 23:03
  • 1
    $\begingroup$ @revision, That's a separate question that is an exercise with the definition of safety property. I suggest spending some time working through some examples of safety properties and non-safety properties and how the definition applies, get some practice with that, and if you're stuck in your self-study, use that to ask a new question (with appropriate motivation and context). $\endgroup$
    – D.W.
    Commented May 2 at 16:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.