A parametric analysis of the state-explosion problem in model checking