my professor said that we can transform the reflexive Finally, Globally and Until into irreflexive Finally, Globally, Until.

Can someone explain me this?

For irreflexive Finally we have $w \models F^+ \varphi$ if $\exists i >= 1: w^{(i)} \models \varphi$ For irreflexive Globally we have $w \models G^+ \varphi$ if $\forall i >= 1: w^{(i)} \models \varphi$ For irreflexive Finally we have $w \models \varphi_1 U^+ \varphi_2$ if $\exists i >= 1: w^{(i)} \models \varphi_2$ and $\forall j, 1 \leq j < i w^{(i)} \models \varphi_1$

  • 1
    $\begingroup$ Are you allowed to use the next operator $X$? $\endgroup$ Nov 28 '19 at 6:32
  • $\begingroup$ Yeah thought about that. Actually i have $X$F = F, irreflexive $\endgroup$
    – comrade
    Nov 28 '19 at 6:38
  • $\begingroup$ But is it a right notation? I know i have just to set the i +1 . If i do it this way how am i able to do it backwards like F= ......F, irr ? In maths i can divide by $X$ but what's the complement for ltl to do that $\endgroup$
    – comrade
    Nov 28 '19 at 6:40
  • $\begingroup$ is $\neg X$ equal to -1 ? haha $\endgroup$
    – comrade
    Nov 28 '19 at 6:42

Sorry, I misread your question at first as wanting to express the irreflexive variant using the reflexive variant (which could be done with the next operator). You don't actually need the next for the other direction.

I'm making the following assumption: By $w^{(i)}$ you mean the suffix of $w$ starting at the $i$ symbol, so for $w = w_0 w_1 w_2 \dots$, you have $w^{(i)} = w_i w_{i+1} w_{i+2} ...$

Then for all $w \in L$, you have:

  1. $w \models F\varphi \Leftrightarrow w \models \varphi \lor F^+ \varphi$.

  2. $w \models G \varphi \Leftrightarrow w \models \varphi \land G^+ \varphi$.

  3. $w \models \varphi_1 U \varphi_2 \Leftrightarrow w \models \varphi_2 \lor (\varphi_1 \land (\varphi_1 U^+ \varphi_2))$.

If you want to show this formally, it follows directly from the definitions:

For 1. you have:

$\begin{align*}w \models F \varphi &\Leftrightarrow \exists i \geq 0: w^{(i)} \models \varphi \\ &\Leftrightarrow \exists i > 0: w^{(i)} \models \varphi \quad \text{ or } \quad w^{(0)} \models \varphi \\ &\Leftrightarrow w \models F^+\varphi \text{ or } w \models \varphi \\ &\Leftrightarrow w \models \varphi \lor F^+\varphi \end{align*}$

The argument for 2. is symmetric to 1.

For 3. you have (pay attention to $\leq$ vs $<$):

$\begin{align*}w \models \varphi_1 U \varphi_2 \Leftrightarrow & \exists i \geq 0 \forall 0 \leq j < i: w^{(j)} \models \varphi_1, w^{(i)} \models \varphi_2 \\ \Leftrightarrow & \exists i > 0 \forall0 \leq j < i: w^{(j)} \models \varphi_1 , w^{(i)} \models \varphi_2 \quad \text{ or } \quad w^{(0)} \models \varphi_2\\ \Leftrightarrow (& \exists i > 0 \forall0 < j < i: w^{(j)} \models \varphi_1 , w^{(i)} \models \varphi_2 \quad \text{ and } \quad w^{(0)} \models \varphi_1) \quad \text{ or } \quad w^{(0)} \models \varphi_2 \\ \Leftrightarrow (&w \models \varphi_1 U^+ \varphi_2 \quad \text{ and } \quad w \models \varphi_1 )\quad \text{ or } \quad w \models \varphi_2 \\ \Leftrightarrow & w \models \varphi_2 \lor (\varphi_1 \land (\varphi_1 U^+ \varphi_2))\end{align*}$

If you would have wanted to do the other direction, as I thought initially:

  1. $w \models F^+ \varphi \Leftrightarrow w \models XF \varphi$

  2. $w \models G^+ \varphi \Leftrightarrow w \models XG \varphi$

  3. $w \models \varphi_1 U^+ \varphi_2 \Leftrightarrow w \models X(\varphi_1 U \varphi_2)$.

To show this formally, the argument would be similar to before.

When you combine both directions, this transformation is sometimes referred to as "unrolling", i.e. expanding $F \varphi \equiv \varphi \lor X F\varphi \equiv \varphi \lor X \varphi \lor XXF \varphi \equiv ...$ and $G \varphi \equiv \varphi \land XG \varphi \equiv \varphi \land X \varphi \land XXG \varphi \equiv ...$ etc.

Regarding your comment (not 100% sure if you were joking): $\lnot X$ is not $-1$ or "going backwards". You have $w \models \lnot X \varphi \Leftrightarrow w^{(1)} \not \models \varphi$. In other words, if you think in terms of Kripke structures and of $w$ as the vertex-label sequence of a path in this transition system, then $\lnot X \varphi$ means "in the next state, $\varphi$ does not hold".


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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