Formal checker for a state safety property:
Algorithm: 'Find reachable state space': Add successors of current set until closure.
S can be held explicitly in bit map form or symbolically as a BDD.
Variation: property to check might be a path property, so either