Toward Formal-Methods Oecumenism?

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