2
$\begingroup$

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

$\endgroup$
2
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Thanks for your answer. I wanted to know if the formula is satisfiable. Sorry for not writing my question this way, I didn't know it's a proper word. $\endgroup$ – pblass Feb 9 at 2:05
  • 1
    $\begingroup$ Yes, the formula is satisfiable, which means that there is a model in which it is true. The formula is not valid. $\endgroup$ – Pål GD Feb 9 at 9:28
  • $\begingroup$ As I understand the question now, he is asking "Is the formula satisfiable for all choices of $\varphi$ and $\psi$?" Neither of us has demonstrated that yet. For example your trivial model fails when $\phi = \lnot p$ for some proposition $p$. $\endgroup$ – f9c69e9781fa194211448473495534 Feb 9 at 9:46
1
$\begingroup$

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

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Thanks for your detailed answer. Your general notes on LTL are really helpful, but I'm not sure if the latter part is correct answer to my question. I wanted to know if the given formula is satisfiable (sorry for not using this word, I'm new to this terminology). This generality of the formula is my problem. If I could say "let $\phi = a$" it would be easy, but I doubt I can. Please correct me if I am wrong. $\endgroup$ – pblass Feb 9 at 2:14

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.