# Semantics of E and A operators in CTL*

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.

• 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*. – f9c69e9781fa194211448473495534 Jun 24 '19 at 6:23
• It's for CTL*, sorry about the confusion. Edited. – Peeyush Kushwaha Jun 25 '19 at 7:29
• I've added CTL* to the title. – 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)'$$.