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

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.