In this paper we present algorithms for model checking CTL over systems specified as Petri nets. We present sequential as well as distributed model checking algorithms. The algorithms rely on an explicit representation of the system state space, but do not require the transition relation to be available; it is recomputed whenever required. This approach allows us to model check very large systems, with hundreds of millions of states, in a fast and efficient way. Furthermore, our distributed algorithms show efficiencies in the range of 80 to 100%.