<p>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? </p>

<p>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?</p>

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

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

CC BY-SA 3.0
2016-09-20T17:31:34.833Z
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?
Shaull
CC BY-SA 3.0
2016-09-20T18:11:14.980Z
@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".
Simon Bliudze
CC BY-SA 3.0
2016-09-20T18:16:16.037Z
This has actually been suggested, [for example here](https://books.google.co.uk/books?id=SXRrCQAAQBAJ&pg=PA27&lpg=PA27&dq=safety+languages+trees+branching&source=bl&ots=12tHeIgY8R&sig=3-_oNV8FnpPQuoWwPtzzJqWh9AI&hl=en&sa=X&ved=0ahUKEwiY3u3_vJ7PAhWLCMAKHdDSA60Q6AEIHDAA#v=onepage&q=safety%20languages%20trees%20branching&f=false). What kind of further syntactic characterization are you looking for?
Shaull
CC BY-SA 3.0
2016-09-20T18:21:45.730Z
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?
Simon Bliudze
CC BY-SA 3.0
2016-09-20T18:28:32.377Z
It's (probably) harder to check safety than to check satisfiability (I think it's not hard to reduce the former to the latter). And satisfiability is EXPTIME complete, so you're not likely to find something simple...
Shaull
CC BY-SA 3.0
2016-09-20T19:54:00.510Z
What about sufficient, but not necessary conditions? (Like the one in my example: `AG p` with p being a state property.)
Simon Bliudze
CC BY-SA 3.0
2016-09-21T05:55:41.420Z
If all the path quantifiers are $A$ (after pushing negations to the atomic propositions) then clearly there is an LTL equivalent...
Shaull
CC BY-SA 3.0
2016-09-21T09:34:00.050Z
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. http://cstheory.stackexchange.com/questions/36626/syntactic-characterisation-of-the-intersection-of-ctl-and-ltl/36627#36627)
Simon Bliudze
CC BY-SA 3.0
2016-09-21T09:41:38.190Z
You're right. My mistake. So I don't have anything better to suggest.
Shaull
<program-verification><temporal-logic><linear-temporal-logic>
Safety properties in CTL
Simon Bliudze
# Safety properties in CTL

(Asked by: username_0 on 2016-09-20)

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?

**Tags:** program-verification, temporal-logic, linear-temporal-logic
> **Comments:**
> **username_1**: 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?  
> **username_0**: @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".  
> **username_1**: This has actually been suggested, [for example here](https://books.google.co.uk/books?id=SXRrCQAAQBAJ&pg=PA27&lpg=PA27&dq=safety+languages+trees+branching&source=bl&ots=12tHeIgY8R&sig=3-_oNV8FnpPQuoWwPtzzJqWh9AI&hl=en&sa=X&ved=0ahUKEwiY3u3_vJ7PAhWLCMAKHdDSA60Q6AEIHDAA#v=onepage&q=safety%20languages%20trees%20branching&f=false). What kind of further syntactic characterization are you looking for?  
> **username_0**: 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?  
> **username_1**: It's (probably) harder to check safety than to check satisfiability (I think it's not hard to reduce the former to the latter). And satisfiability is EXPTIME complete, so you're not likely to find something simple...  
> **username_0**: What about sufficient, but not necessary conditions? (Like the one in my example: `AG p` with p being a state property.)  
> **username_1**: If all the path quantifiers are $A$ (after pushing negations to the atomic propositions) then clearly there is an LTL equivalent...  
> **username_0**: 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. http://cstheory.stackexchange.com/questions/36626/syntactic-characterisation-of-the-intersection-of-ctl-and-ltl/36627#36627)  
> **username_1**: You're right. My mistake. So I don't have anything better to suggest.  

---

## 0 answers

