{A Parametric Analysis of the State-Explosion Problem in Model Checking}