> It's the logic of state developing over time.
You may already be aware of this, but that various kinds of temporal logic allows one to capture very complex predicates for the evolution of state machine (much like your person with a dollar).
If you have a familiarity with state machines (here Kripke systems) it might be approachable.
Some useful links:
1. https://www.cs.cmu.edu/~emc/15414-s14/lecture/ModelChecking....