[Solved]: CTL vs LTL - when a formula satisfy a model

Problem Detail: 

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?

Asked By : Fabrizio Duroni

Answered By : hengxin

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.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/37498

 Ask a Question

 Download Related Notes/Documents