1
$\begingroup$

i'm trying to prove every trace over PROP = {p} is a model of the formula. I am very stuck in figuring out a model pi that satisfies this formula, can anyone point me in the right direction?

$\endgroup$

3 Answers 3

2
$\begingroup$

The LTL formula for the given problem could be: $G(F(p)) \lor G(F(\lnot p))$. Consider a $\omega$-word $w = w_1w_2w_3 \ldots$ over $\{\{\}, \{p\}\}$:

Let $w_i = w_iw_{i+1}\ldots$ \begin{align*} & \; \; \; \; \; \; \; \; \; w \not\models G(F(p))\\ &\implies \exists i . w_i \not\models F(p)\\ &\implies \exists i. \forall j \geq i . w_j \models \lnot p\\ &\implies \exists i. \forall j \geq i . w_j \models F(\lnot p)\\ &\implies \exists i. w_i \models G(F(\lnot p))\\ &\implies w \models G(F(p)) \lor G(F(\lnot p)) \end{align*}

Therefore, $G(F(p)) \lor G(F(\lnot p))$ is valid.

Note that this doesn't mean that $G(F(p)) \land G(F(\lnot p))$ is not satisfiable. For example, consider the word $w=\{p\}\{\}\{p\}\{\}\{p\}\{\}\ldots$

$\endgroup$
7
  • $\begingroup$ You're using $w_i$ to mean two different things. $\endgroup$ Commented May 22, 2020 at 7:48
  • $\begingroup$ @YuvalFilmus By convention $w_i \models \psi$ means the first position of $w_i$ satisfies $\psi$. So, can you elaborate why you think I meant two different things by $w_i$... $\endgroup$
    – prime_hit
    Commented May 22, 2020 at 7:51
  • $\begingroup$ You wrote $w_i = w_i w_{i+1} \dots$ $\endgroup$ Commented May 22, 2020 at 7:51
  • $\begingroup$ I am still missing where did I use anything other than $w_i = w_iw_{i+1}\ldots$... $\endgroup$
    – prime_hit
    Commented May 22, 2020 at 7:53
  • 1
    $\begingroup$ My only complaint is that $w_i$ signifies both an $\omega$-word and a single state. If this is common in the relevant community, then that's fine. $\endgroup$ Commented May 22, 2020 at 7:59
0
$\begingroup$

Consider a model $\pi$. Let $T$ be the set of times at which $p$ holds. If $T$ is infinite, then "infinitely often $p$" holds. If $\overline{T}$ is infinite, then "infinitely often $\lnot p$" holds. One of these two must hold, since there are infinitely many times.

$\endgroup$
0
$\begingroup$

You can use logical equivalences to show this is a valid LTL formula over models with the proposition $p \in \mathrm{Prop}$.

$$\begin{aligned} &\mathsf{G}\mathsf{F} p \vee \mathsf{G}\mathsf{F}\neg{}p\\ &= \langle \mathsf{GF}\varphi \vee \mathsf{GF}\psi \equiv \mathsf{G}(\mathsf{F}\varphi \vee \mathsf{F}\psi) \rangle\\ &\mathsf{G}(\mathsf{F} p \vee \mathsf{F}\neg{}p)\\ &= \langle \mathsf{F}\varphi \vee \mathsf{F}\psi \equiv \mathsf{F}(\varphi \vee \psi) \rangle\\ &\mathsf{G}\mathsf{F}( p \vee \neg{}p)\\ &= \langle\text{excluded middle} + p \in \mathrm{Prop} \rangle\\ &\mathsf{G}\mathsf{F}\top\\ &= \langle \mathsf{F}\top \equiv \top \rangle\\ &\mathsf{G}\top\\ &= \langle \mathsf{G}\top \equiv \top \rangle\\ &\top \end{aligned}$$

Most of the above equivalences are fairly easy to show by unfolding the semantics. The only annoying part is showing the $\mathsf{G}(\mathsf{F} \varphi \vee \mathsf{F}\psi) \Rightarrow \mathsf{G}\mathsf{F} \varphi \vee \mathsf{G}\mathsf{F}\psi$ direction of $\mathsf{G}\mathsf{F} \varphi \vee \mathsf{G}\mathsf{F}\psi \equiv \mathsf{G}(\mathsf{F} \varphi \vee \mathsf{F}\psi)$.

(see also A Calculational Deductive System for Linear Temporal Logic for a nice list of LTL theorems)

$\endgroup$

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.