Have used open-sourced QuickCheck equivalent for Erlang, called PropEr. Great exercise in abstract thinking. Although testing stateful machines in scenarios where time matters turned out to be very hard.
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):
