LTL Logic Finally, Globally and Until to irreflexive Version

Question

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$

Answer 1

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".