I'm especially interested in their use in model checking applications. I have Open, Closed and Mixed Networks of Queues with Different Classes of Customers by Baskett et al. Any other suggestions for reading material? Thanks.
There is this unpublished book by Aldous and Fill, two experts in the field. You'll find walks on product of chains there.