The parallelization of binary decision diagram operations for model checking