2
$\begingroup$

I'm trying to understand the difference between LTL and CTL. In particular, i'm trying to understand when a model (a transition system eg. Kripke structure) satisfy a formula. This is my point of view:

  • a model satisfy an LTL formula if an only if all its path starting from its initial state satisfy the formula
  • a model satisfy a CTL formula if and only if all of its state satisfy the formula. So i have to check that it is valid for all the path (or for some path if there's a E quantifier) starting from each state. -

Is it correct? can someone help me?

$\endgroup$
5
$\begingroup$

For what it concerns LTL, your understanding is almost correct except that there may be more than one initial states in a transition system.

An LTL formula $\varphi$ holds in state $s$ of a transition system $TS$ if all paths starting in $s$ satisfy $\varphi$.

The transition system $TS$ satisfies an LTL formula $\varphi$ if if all initial paths of $TS$, paths starting in an initial state $s_0 \in I$, satisfy $\varphi$.


For what it concerns CTL, we have

The transition system $TS$ satisfies an CTL formula $\Phi$ if and only if $\Phi$ holds in all initial states of $TS$.

Note that, similar to the case in LTL, we are only concerned with the initial states of $TS$ in the semantics of CTL. However, this does not imply that you don't need to check other states of $TS$ against a specific CTL formula $\Phi$. This is both $\Phi$-dependent and checking algorithm-dependent.

For example, the well-known checking algorithm (see the lecture note) is a global model-checking procedure, meaning that it does check for any state $s$ in $TS$ whether $s \models \Phi$, and not just for the initial states. This is because the algorithm is computing fixed points recursively: The result of $s \models \Phi$ may rely on each of $s' \models \Phi$, where $s' \in \text{Post}(s)$ is a direct successor of $s$ in $TS$.

Furthermore, it also checks for any state $s$ whether $s \models \Phi_{sub}$, where $\Phi_{sub}$ is any subformula of $\Phi$, by backward search.

$\endgroup$
  • 1
    $\begingroup$ While everything you wrote is correct (upvoted), note that $LTL$ is actually interpreted over computations, and the universal extension to transition systems is arbitrary. In many scenarios (such as robotics) researchers are interested in an existential extension, so we're asking whether there exists a path satisfying the formula. These two interpretations are known as $\forall LTL$ and $\exists LTL$. $\endgroup$ – Shaull Jan 23 '15 at 8:42
  • $\begingroup$ @hengxin thank you. I get confused reading this cs.utexas.edu/users/moore/acl2/seminar/2010.05-19-krug/…. Slide 30 says "A model, or Kripke structure, satisfies a CTL formula, when all its states do". Maybe this slide means exactly what you was saying: the validity of a formula in a state can rely on its validity in another one. e.g. TS ⊨ AGAFΦ require you to check on every state that all its paths can reach a state that satisfy Φ (so you have to check which state satisfy AFΦ and be sure that there's one of them on every path from any state). Do you agree with me? $\endgroup$ – Fabrizio Duroni Jan 23 '15 at 23:11
  • $\begingroup$ @FabrizioDuroni I tend to regard the statement ... when all its states do is a literal typo in the lecture note: In its formal description $(M \models \phi) \iff \forall s \in I, (M,s \models \phi)$, it only requires satisfiability on $s \in I$. $\endgroup$ – hengxin Jan 24 '15 at 8:01

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.