Question

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?

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top