I'm referring to a book where E and A were defined in text as follows

The formula $A \phi$ states that all the executions out of the current state satisfy property $\phi$ whereas $E\phi$ states that from the current state, there exists and execution satisfying $\phi$

And formally, they were defined as

$\sigma, i \models E\phi $ iff there exists as $\sigma'$ such that $\sigma(0)\ldots\sigma(i) = \sigma'(0)\ldots\sigma'(i)$ and $\sigma', i \models phi$ $\sigma, i \models A\phi $ iff for all $\sigma'$ such that $\sigma(0)\ldots\sigma(i) = \sigma'(0)\ldots\sigma'(i)$, we have $\sigma', i \models phi$

$\sigma(i)$ was previously defined to be the ith state of an execution $\sigma$.

Here's where my confusion lies. Doesn't $\sigma(0)\ldots\sigma(i) = \sigma'(0)\ldots\sigma'(i)$ imply that the executions $\sigma$ and $\sigma'$ have both the same start and end state, therefore $\sigma', i \models \phi$ is same as $\sigma, i \models \phi$? That seems to be wrong.

  • $\begingroup$ For those that do not have access to the full book, can you clarify which logic the definition is about? The question is tagged with "linear-temporal-logic", but the definition looks more like a branching-time logic to me. From the preview of your book, it seems the chapter on "Temporal Logic" deals with CTL*. $\endgroup$ – f9c69e9781fa194211448473495534 Jun 24 '19 at 6:23
  • $\begingroup$ It's for CTL*, sorry about the confusion. Edited. $\endgroup$ – Peeyush Kushwaha Jun 25 '19 at 7:29
  • $\begingroup$ I've added CTL* to the title. $\endgroup$ – reinierpost Nov 22 '19 at 10:15

I believe it means that $\sigma,\sigma$ should share the same prefix up to position $i$. Then the quantification ranges over all possible extensions of this prefix from state $\sigma(i) = \sigma(i)'$.

| cite | improve this answer | |

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.