# 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*. Jun 24, 2019 at 6:23
• It's for CTL*, sorry about the confusion. Edited. Jun 25, 2019 at 7:29
• I've added CTL* to the title. Nov 22, 2019 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)'$$.
I think you misinterpret the expression $$\sigma(0) \cdots \sigma(i) = \sigma'(0) \cdots \sigma'(i')$$ and I agree that it is written in an unintuitive way.
The author means that $$\sigma(i) = \sigma'(0)$$ and that the final path is $$\sigma(0) \cdots \sigma(i) \; \sigma'(0) \cdots \sigma'(i').$$
The equality ensures that the path $$\sigma'$$ starts where $$\sigma$$ ends.
Are you sure there isn't a prime on the $$i$$?