Model for formula $\Box (\psi \vee \phi) \Rightarrow (\Box \psi) \vee (\Box \phi)$

Question

I am new to LTL and I am trying to understand how it works. My question is: is there such $\sigma$ that:

$ \sigma \models [\Box (\psi \vee \phi) \Rightarrow (\Box \psi) \vee (\Box \phi)]$

I know that:

$\sigma \models \Box \psi: \forall k \, [(\sigma, k) \models \psi] \\ \sigma \models [\psi \Rightarrow \phi]: (\sigma \models \neg \psi) \vee (\sigma \models \phi) \\ \sigma \models \Box \psi \iff \sigma \models \neg\Diamond \neg \psi$

So

$\sigma \models [\Box (\psi \vee \phi) \Rightarrow (\Box \psi) \vee (\Box \phi)] \iff \\(\sigma \models \Diamond (\neg\psi \land \neg\phi)) \vee [(\sigma \models (\Box \psi)) \vee (\sigma \models (\Box \phi))]$

I would say there is such $\sigma$ since I don't see any contrarguments but I'm not sure if I can say anything about $\psi$ or $\phi$ except that both are formulas (so I don't know how to show any specific example).

Answer 1

If you're just asking for any model satisfying the formula, you simply try to make one of these the case

1. The left hand side false
2. The right hand side true

Let's just pick number 2. You have to make a model (with a state $\sigma$) where $\Box \psi \lor \Box \phi$ is the case. Even easier is $\Box \phi$.

Create a (trivial) model where every state $\sigma$ has $\sigma \models p$ for all propositions $p$.

---

If you want to see if the formula is valid then the answer is no. You should now be able to create a model that falsifies the formula.

Answer 2

General notes on LTL

Intuitively, LTL formulas are statements about infinite sequences (or "infinite words"). First, you have to understand what these sequences consist of.

In the usual definition of LTL, you start with a set of atomic propositions $AP$. For example $AP = \{a,b\}$. These atomic propositions then act as the base elements of your LTL formulas, so you could have an LTL formula $\varphi = a$ or $\psi = a \land \lnot b$ and so on. Then you can add the temporal operators, so you could also have LTL formulas like $\varphi' = \Box a$ or $\psi' = a \land \Diamond \lnot b$ and so on.

For the semantics of LTL, we then consider infinite words over the power set of $AP$. So for $AP = \{a,b\}$ we are looking at infinite words where each symbol is one of $\emptyset$, $\{a\}$, $\{b\}$ or $\{a,b\}$. For example we could have a word $\sigma = \{a,b\}\{a\}\{a\}\{a\}...$, where the first symbol is $\{a,b\}$, and all following symbols are $\{a\}$.

You would then define the meaning of an LTL formula $\varphi = a$ to be such that a word $\sigma$ satisfies $\varphi$ iff $a \in \sigma(0)$. Put differently, an LTL formula $\varphi$ consisting of a single atomic proposition is satisfied by a word $\sigma$ iff the set of atomic propositions that is the first symbol of $\sigma$ contains $\varphi$. We denote this by $\sigma \models \varphi$. So for $\sigma = \{a,b\}\{a\}\{a\}\{a\}...$, you have $\sigma \models a$, because $a \in \{a,b\}$.

You would then expand the definition to the other operators, so for example you would say the meaning of $\varphi = \Box \psi$ is such that a word $\sigma$ satisfies $\varphi$ iff every infinite suffix of $\sigma$ (in your notation for every $k \in \mathbb N$ the word $(\sigma,k) = \sigma(k) \sigma(k+1) \sigma(k+2)...$ ) satisfies $\psi$. So using the same $\sigma$ as before, we would have $\sigma \not \models \Box b$, as the suffix $\sigma(1)\sigma(2)\sigma(3)... = \{a\}\{a\}\{a\}...$ does not satisfy $b$, since $b \notin \{a\}$.

Using a more practical example: Suppose you want to model a robot that has an arm with a grabber for picking things up from the ground. You could have $AP = \{\text{arm_down}, \text{grabber_closed}\}$. Then a word $\sigma$ represents a specific behaviour of the robot (assuming it runs infinitely). So for example $\sigma = \emptyset \{\text{arm_down}\}\{\text{arm_down,grabber_closed}\}\{\text{grabber_closed}\}\{\text{grabber_closed}\}...$ represents the robot behavior of the robot picking something up from the ground and then holding it indefinitely:

1. Arm is up and grabber open.
2. Arm is now down.
3. Arm is down and grabber has closed.
4. Arm is up and grabber closed.
5. ...

An LTL formula would then make a statement about the behavior of a robot. For example $\varphi = \Box \Diamond \lnot\text{arm_down}$ would mean "it is always true that eventually the robot arm is not down" or in other words "if the arm moves down it has to move up again at some point".

Regarding your question

As I understand your question, you are asking "are there $\varphi$ and $\psi$, such that there is a $\sigma$ which satisfies $\Box (\varphi \lor \psi) \Rightarrow (\Box \varphi) \lor (\Box \psi)$?".

The answer to that would be yes, you could for example take $AP = \{a,b\}$ and $\varphi = a$, $\psi = b$.

Then the word $\sigma = \emptyset \emptyset \emptyset ...$ satisfies your formula, as the left-hand side of the implication is not satisfied ($\sigma \not \models \Box (a \lor b)$, because not every symbol of $\sigma$ contains $a$ or $b$).

Alternatively, $\sigma' = \{a\}\{a\}\{a\}...$ also satisfies your formula, as it satisfies the right-hand side of the implication ($\sigma' \models \Box a$, because every symbol of $\sigma'$ contains $a$).

You could then also ask the related question of whether for that choice of $\varphi$ and $\psi$ the formula is valid, meaning that all words satisfy it. This is not the case, consider for example $\sigma'' = \{a\}\{b\}\{a\}\{b\}...$ Then $\sigma'' \models \Box(a \lor b)$, as every symbol of $\sigma''$ contains $a$ or $b$. But $\sigma'' \not \models (\Box a) \lor (\Box b)$, because neither does every symbol of $\sigma''$ contain $a$ nor does every symbol of $\sigma''$ contain $b$.

You could also ask the related question of whether there are $\varphi$ and $\psi$ such that your formula becomes valid. The answer to that would be yes. Consider $\varphi = \psi = a \land \lnot a$ (meaning both $\varphi$ and $\psi$ are unsatisfiable). Then every word $\sigma$ satisfies your formula, as for every word the left-hand side of the implication is false: $\sigma \not \models \Box(\varphi \lor \psi)$, because $\varphi \lor \psi$ can be satisfied by no symbol of $\sigma$.