How to approach modeling time?

See Lamport's paper Real Time is Really Simple: https://www.microsoft.com/en-us/research/publication/real-time-is-really-simple/

Basic idea: instead of having a monotonically-increasing time variable, you keep track of a set of upper-bound timers (action must happen before timer reaches zero) and lower-bound timers (action cannot happen until timer reaches zero) that always initialize to some finite value then tick down to zero instead of tracking an infinitely-increasing clock time.

Source: https://groups.google.com/g/tlaplus/c/IGbAcSOUUes