# Safety VS. Liveliness Property

I have to prove whether a certain property is safety or liveliness. The property represents the absence of deadlock so I expected it to be a safety property from what I read online.

The issue is that I seem to show that it is both, but this is impossible as the only property that is both safety and liveliness would be $$\left(2^{\Xi}\right)^{\omega}$$, where $$\Xi$$ is the set of propositional symbols. I would like to understand where the mistake is, and naturally if any of the solutions would be correct. Also, I would like to do it in a formal way instead of using the "something bad never happens" intuitive idea.

The property in question is: $$\mathsf{G}((P1E \wedge P2E) \rightarrow (\mathsf{F}\, (P1C \vee P2C)))$$

1. The definition I have for safety property goes as follows:

An LT property $$P_{safe}$$ over $$\Xi$$ is called a safety property if for all words $$\sigma \in\left(2^{\Xi}\right)^{\omega} \setminus P_{safe}$$ there exists a finite prefix $$\hat\sigma$$ of $$\sigma$$ such that $$P_{safe} \cap \{\sigma^\prime\in \left(2^{\Xi}\right)^{\omega}\; |\; \hat\sigma \textrm{ is a finite prefix of }\sigma^\prime \} = \emptyset$$

What I tried to do is as follows:

Let $$\sigma\in \left(2^{\Xi} \right)^{\omega}$$ be an arbitrary word such that $$\sigma\not \Vdash \mathsf{G}((P1E \wedge P2E) \rightarrow (\mathsf{F}\, (P1C \vee P2C)))$$, then there exists $$i\geq 0$$ such that $$\sigma, i\,\not \Vdash (P1E \wedge P2E) \rightarrow (\mathsf{F}\, (P1C \vee P2C))$$. Let $$\hat\sigma=\sigma[..i]$$, this is a bad prefix of $$\sigma$$, and for any word $$\sigma^\prime\in \left(2^{\Xi} \right)^{\omega}$$ such that $$\hat\sigma$$ is a prefix of $$\sigma^\prime$$, we have that $$\sigma^\prime,i \not \Vdash(P1E \wedge P2E) \rightarrow (\mathsf{F}\, (P1C \vee P2C))$$, thus: $$\sigma^\prime\not \Vdash \mathsf{G}((P1E \wedge P2E) \rightarrow (\mathsf{F}\, ( P1C \vee P2C)))$$. We conclude it is a safety property.

1. The definition I have for liveliness property goes as follows:

An LT property $$P_{live}$$ over $$\Xi$$ is called a liveness property if $$pref(P_{live}) = \left(2^{\Xi} \right)^{*}$$.

So, I can't see why I can't prove it is a liveliness property as:

Take $$\hat\sigma\in\left(2^{\Xi} \right)^{*}$$ of length $$n+1$$, $$\hat\sigma=v_0...v_n$$, let $$\sigma=\hat\sigma.P1C.\varnothing^{\omega}$$ .

For all $$i> n$$, we have that $$\sigma,i \not \Vdash P1E \wedge P2E$$ thus $$\sigma,i \Vdash (P1E \wedge P2E) \rightarrow (\mathsf{F}\, (P1C \vee P2C))$$.

For all $$i\leq n$$, we have $$i and $$\sigma, n+1 \Vdash P1C$$ thus $$\sigma, i\Vdash \mathsf{F}(P1C \vee P2C)$$, hence $$\sigma,i \Vdash (P1E \wedge P2E) \rightarrow (\mathsf{F}\, (P1C \vee P2C))$$.

Therefore we have that $$\forall i\geq 0, \;\; \sigma, i\Vdash (P1E \wedge P2E) \rightarrow (\mathsf{F}\, (P1C \vee P2C))$$. Thus:

$$\sigma \Vdash \mathsf{G}((P1E \wedge P2E) \rightarrow (\mathsf{F}\, (P1C \vee P2C)))$$

Hence, it is a liveliness property.

Note: This is my first time posting in this community so any comments are appreciated. Also if it were better to post this in the math.stack, let me know!

I found the error on the safety proof.

Let $$\hat\sigma=\sigma[..i]$$, this is a bad prefix for our property.

This is of course wrong. If the property is not satisfied, i.e., $$\sigma \not\Vdash \mathsf{G}((P1E \wedge P2E) \rightarrow (\mathsf{F}\, (P1C \vee P2C)))$$ then indeed there is as $$i\geq 0$$ such that $$\sigma, i\not \Vdash ((P1E \wedge P2E) \rightarrow (\mathsf{F}\, (P1C \vee P2C))$$, that is:

$$\sigma, i\Vdash P1E \,\wedge\, P2E \;\;\textrm{ and } \sigma, i\not\Vdash \mathsf{F}\, (P1C \vee P2C)$$

The thing is that just because we have $$\sigma, i\not\Vdash \mathsf{F}\, (P1C \vee P2C)$$, it does not mean that it cannot become true in the future, therefore we cannot state that $$\hat\sigma$$ is a bad prefix for the property, as a word $$\sigma^\prime$$ with prefix $$\hat\sigma$$ can still be extended in order to satisfy the property.

Hence, this was wrong and it is indeed a liveliness property.

• How can $F(P1C \lor P2C)$ "become true in the future" when it did not hold at $\sigma,i$?
– Kai
Commented Jan 3, 2023 at 11:17
• @Kai If $\sigma, i+1\Vdash P1C \vee P2C$ for example... Commented Jan 3, 2023 at 16:55
• No. Check the semantics of $F$ please.
– Kai
Commented Jan 4, 2023 at 0:19
• @Kai listen, firstly I think that if you’re comenting on someone’s post that there’s a mistake, you should actually try to help them with that. Also, this was discussed in a class and our Professor explained to us it was a liveliness property with the justification I just gave. At last, from what I’ve learned, $\sigma, i\Vdash \mathsf{F}\varphi$ if there is some $j\geq i$ such that $\sigma,j\Vdash \varphi$, so I don’t see why what I said can be wrong. Commented Jan 4, 2023 at 11:17