The correctness of a system with respect to a desired behavior is verified by checking whether a structure that models the system satisfies a formula describing that behavior.
The fact that the system cannot reach unwanted states (safety) and that there is no possibility of leakage of information (security and privacy) are among the most interesting properties.
Continuous variables give rise to infinite models, hence the need of dealing with finite approximations which ensure holding of the considered property in the original model. But also with finite models the computational effort (state explosion) may be an obstruction to verification.