0
$\begingroup$

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.

$\endgroup$
3
  • $\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$ Jun 24, 2019 at 6:23
  • $\begingroup$ It's for CTL*, sorry about the confusion. Edited. $\endgroup$ Jun 25, 2019 at 7:29
  • $\begingroup$ I've added CTL* to the title. $\endgroup$ Nov 22, 2019 at 10:15

2 Answers 2

1
$\begingroup$

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

$\endgroup$
-1
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.