Computation Tree Logic and its Temporal Opeators

Question

I've got some questions about the temporal operators in computation tree logic:

1. Does the Finally path-specific quantifier Fq mean that q has to hold in a subsequent state or is it also fulfilled when q holds in the current state?

2. Please consider the following example:

   

   What exactly is specified here? Does it mean: If q AND r holds on a path P in a graph G then q has to hold somewhere on the subsequent path of P. Or does it mean: ... q has to hold somewhere on the subsequent path of every path of G?

Answer 1

First, a small comment - the $F$ operator comes from the word "future", rather than "finally", although it is indeed very tempting to say "finally".

1. The semantics of $Fq$ with respect to a computation $\pi$ is: $$\pi\models Fq \iff \exists i\ge 0, \pi^i \models q$$ Thus, the 0th suffix is also considered, so if $q$ hold immediately, the formula is still satisfied. Observe that you can capture the notion of "strict future" with the formula $XFq$.

2. The formula states that along every path ($A$), every state $s$ satisfies ($G$) the following: if $q$ and $r$ are true in $s$, then in every path starting from $s$, $q$ eventually appears.

I think this is what you meant in your second option.

Answer 2

For the first question:
Yes. For a specific path, $Fq$ is evaluated to be true if and only if $q$ is satisfied eventually in the future. It includes the case in which $q$ is satisfied immediately in the first state (of the path).

For the second question:
First, do you mean $AG(q \land r) \Rightarrow AF(q)$?

Whatever, $G$ here is not a graph. It is another temporal modality in Computation Logic Tree (CTL). $Gq$ is evaluated to be true if and only if $q$ holds from now on forever. $AG (q \land r)$ is pronounced "invariantly $q \land r$", meaning that along all paths that start in some specified state, $q \land r$ always holds. $AF (q)$ pronounced "$q$ is inevitable", meaning that along all paths that start in some specified state, $q$ eventually holds. Informally, "invariantly" implies "inevitable". Thus, we can conclude that $AG(q \land r) \Rightarrow AF(q)$ for some specified state.