As I understand it, most property testing tools operate at the level of functions. Given a set of arguments, such tools will generate random input and test output against some invariant.
I have read that ScalaCheck is now starting to include generation of events to test a statefull system. However, I can't find great deal of information on it. Is this becoming popular in rest of the *check ecosystem as well (fscheck, quickcheck, other variations)?
What you call "generation of events" to my knowledge originates in "Testing Monadic Code with QuickCheck", by Koen Claessen and John Hughes. The example they give is testing a queue. The approach that is used is always similar - as comments say, since "basic" quickcheck (I'll use lowercase quickcheck to describe the family of QuickCheck ports on various platforms) assumes it generates immutable data, at first sight it's not easy to use quickcheck to test a side-effecting, stateful system.
Until you realize that a stateful system gets to a certain state by executing a sequence of state transitions (these are variously called commands, actions, events etc). And this sequence can be represented perfectly as an immutable list of immutable transitions! Typically then each transition is executed on the real system under test, and a model of its state. Then after each transition the model state is compared with the real state.
To see how this plays out in Quvik QuickCheck (for Erlang) for example you can read "Testing Telecoms Software with Quviq QuickCheck" by Thomas Arts, John Hughes, Joakim Johansson and Ulf Wiger.
I do believe most quickchecks, including QuickCheck itself, have a layer on top of the basic quickcheck functionality that allows you to generate a sequence of state transitions, typically using a state machine like approach with pre-and postconditions etc.
I don't think this is particularly new, but probably a bit under-emphasized.
For example, FsCheck has had model based testing for years (dislosure: I am FsCheck's main contirbutor). I think the same is true for ScalaCheck. Quvik QuickCheck's is likely the most advanced implementation (certainly with the most advanced applications).