I prototyped this using computational tree logic (CTL). You can express the non existence of trap states and reachability of all states quite nicely and fully explore the state space symbolically. The drawback is you can't really do numbers in it.