1
$\begingroup$

In the literature, I have only found a formal definition for safety properties in LTL. This, essentially, boils down to the following: "every trace that violates the property has a finite prefix attesting this violation". This, indeed, works nicely for LTL, which is based on traces. What about CTL?

For properties that can be equivalently expressed in LTL and in CTL, the definition safety in CTL can be given by transposing that from LTL. What about the ones that are not expressible in LTL?

For instance, AG p is clearly a safety property, when p is a state predicate. What about AG EF p? If the property is violated, then there exists a finite trace ending in a state, from which no state satisfying p is reachable.

Also, assuming there is a definition of safety in CTL, is there a syntactic characterisation of such properties?

Improve this question
$\endgroup$
9
  • $\begingroup$ What do you mean by "assuming there is a definition of safety in CTL"? Once you define safety, then you can discuss whether there is a syntactic characterization... What do you suggest as a definition? $\endgroup$
    – Shaull
    Sep 20, 2016 at 17:31
  • $\begingroup$ @Shaull: I was thinking along the lines of the above approximate definition: "every tree that violates the property has a finite sub-tree attesting the violation". $\endgroup$
    – Simon Bliudze
    Sep 20, 2016 at 18:11
  • $\begingroup$ This has actually been suggested, for example here. What kind of further syntactic characterization are you looking for? $\endgroup$
    – Shaull
    Sep 20, 2016 at 18:16
  • $\begingroup$ Thanks for the pointer! Regarding the syntactic characterisation, I am looking for something that can be checked on the CTL formula, not on the set of its models. For example, if all branch quantifiers used in the formula are universal, the temporal modalities are only G and W (weak until) and negation is only used on state predicates, then I would expect the formula to be a safety one. Is this true? Is there a weaker characterisation? $\endgroup$
    – Simon Bliudze
    Sep 20, 2016 at 18:21
  • 2
    $\begingroup$ That's what I thought in the beginning, but this does not work. Consider AF AG p. If there were an LTL equivalent, it would have to be F G p. However, this latter is not expressible in CTL. (Btw, I think these two last comments are more relevant to the other question I asked, i.e. cstheory.stackexchange.com/questions/36626/…) $\endgroup$
    – Simon Bliudze
    Sep 21, 2016 at 9:34

0

Reset to default

Your Answer

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