Model checking is rather poor when properties deal not with causality of events but with data types or recursive constructs. In that area, algebraic methods, even if they're more complex to grasp, are much more appropriate and efficient. And it's true that, with Petri nets, you can do both model checking and a sort of parameterized analysis. But, if model checking remains as efficient as what you can get from a Promela program, the model itself only offers basic constructs to handle parallelism. This is also true with parameterized proofs using Petri net invariants