Time is fun. You have to essentially mock it. Write a system in which you can control how time advances and then define your postconditions in the stateful system such that time is not violated. I have an approach here, taken for the 'fuse' project in Erlang (Using the commercial version of Quviq QuickCheck):

https://github.com/jlouis/fuse/tree/master/eqc_test