{logic.modelChecking} CTL

Here yet another nice introduction to model checking:
http://www.cs.utexas.edu/users/wahl/intro-modelChecking.pdf

CTL (Computational Tree Logic) is a branching-time logic. All of our daily actions can actually satisfy a correctness statement in CTL. For example,

AG ~(arrogance) means "avoid arrogance";
AG (self-esteem) means "maintain self-esteem";
EG ~(arrogance) means "try to avoid arrogance";
EG (self-esteem) means "try to maintain self-esteem";
AF (financial independence) means "reach financial independence"; and
EF (Damavand peak) means "try to reach Damavand peak".