1
$\begingroup$

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:

    enter image description here

    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?

$\endgroup$
3
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ That was exactly what I meant in my second question. Thanks a lot. $\endgroup$ – 0xbadf00d Dec 31 '13 at 21:07
1
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ I think the order of parenthesis in the OP's formula is different. It is not $AG(q\wedge r)\implies AFq$, but $AG((q\wedge r)\implies AF(q))$. $\endgroup$ – Shaull Dec 31 '13 at 8:32

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.