2
$\begingroup$

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<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!

$\endgroup$

1 Answer 1

0
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ How can $F(P1C \lor P2C)$ "become true in the future" when it did not hold at $\sigma,i$? $\endgroup$
    – Kai
    Jan 3, 2023 at 11:17
  • $\begingroup$ @Kai If $\sigma, i+1\Vdash P1C \vee P2C$ for example... $\endgroup$
    – davinci_07
    Jan 3, 2023 at 16:55
  • $\begingroup$ No. Check the semantics of $F$ please. $\endgroup$
    – Kai
    Jan 4, 2023 at 0:19
  • $\begingroup$ @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. $\endgroup$
    – davinci_07
    Jan 4, 2023 at 11:17

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.