<p>To answer your second question: there is one property that is both safety and liveness: True. With this exception, however, it is fair to say that a property is either safety or liveness or neither. "Most" properties (like yours) are actually neither, but every property can be represented by the intersection of a safety and a liveness property. </p>

<p>I think your property could be represented by the intersection (conjunction) of the following two properties in LTL notation:</p>

<p>Safety: G(x -> (a W y))</p>

<p>and </p>

<p>Liveness: G(x -> F y)</p>

CC BY-SA 3.0
2015-02-07T10:21:41.290Z
Why is this G(x -> (a W y)) safety? you can reach the bad state (y never happend)
Nk SP
CC BY-SA 3.0
2015-06-11T18:41:07.577Z
W = weak until operator
0 _
CC BY-SA 3.0
2015-06-12T21:10:00.273Z
The fact that "y never happened" is not a bad state but an infinite trace - and it is handled in the liveness part (the second formula).
Markus
CC BY-SA 3.0
2015-02-07T10:00:46.020Z
2015-02-07T10:00:46.020Z
Markus
<p>Your first question is answered in this paper: <a href="https://www.cs.cornell.edu/fbs/publications/RecSafeLive.pdf" rel="noreferrer">https://www.cs.cornell.edu/fbs/publications/RecSafeLive.pdf</a>
Given an LTL formula, translate it into a B&uuml;chi automaton, and remove states that have no path to an accepting state. Then, change all states to be accepting. If the language of the automaton does not change, then the property is a safety property. If the language of the automaton becomes $\Sigma^\omega$, then it is a liveness property.</p>

CC BY-SA 3.0
2015-02-06T21:48:52.360Z
2015-02-06T23:37:20.357Z
2015-02-06T23:37:20.357Z
Guy
<p>How can I check if an LTL (Linear Temporal Logic) property is safety or liveness? Is it right to say that a property is safety OR liveness (or neither)?</p>

<p>How can I evaluate this:<br></p>

<pre><code>G(x -&gt; (a U y) )
</code></pre>

<model-checking><temporal-logic><linear-temporal-logic><mu-calculus>
LTL property - safety or liveness?
Nk SP
# LTL property - safety or liveness?

(Asked by: username_0 on 2015-02-06)

How can I check if an LTL (Linear Temporal Logic) property is safety or liveness? Is it right to say that a property is safety OR liveness (or neither)?
How can I evaluate this:
G(x -> (a U y) )

**Tags:** model-checking, temporal-logic, linear-temporal-logic, mu-calculus


---

## 2 answers

### Answer by username_1 on 2015-02-07. Score: 1 | Accepted answer

To answer your second question: there is one property that is both safety and liveness: True. With this exception, however, it is fair to say that a property is either safety or liveness or neither. "Most" properties (like yours) are actually neither, but every property can be represented by the intersection of a safety and a liveness property.

I think your property could be represented by the intersection (conjunction) of the following two properties in LTL notation:

Safety: G(x -> (a W y))

and

Liveness: G(x -> F y)

> **Comments:**
> **username_0**: Why is this G(x -> (a W y)) safety? you can reach the bad state (y never happend)  
> **username_2**: W = weak until operator  
> **username_1**: The fact that "y never happened" is not a bad state but an infinite trace - and it is handled in the liveness part (the second formula).  

---

### Answer by username_3 on 2015-02-06. Score: 5

Your first question is answered in this paper: <https://www.cs.cornell.edu/fbs/publications/RecSafeLive.pdf>
Given an LTL formula, translate it into a Büchi automaton, and remove states that have no path to an accepting state. Then, change all states to be accepting. If the language of the automaton does not change, then the property is a safety property. If the language of the automaton becomes $\Sigma^\omega$, then it is a liveness property.


---

