Safety VS. Liveliness Property

Question

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.

2. 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<n+1$ 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!

Answer 1

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.