1. A computerized system comprising: a processor; a first interface configured to obtain a constraint; a second interface configured to obtain a first model, the first model is configured to be utilized in model checking, the first model comprising an at least one finite path in respect to the constraint obtained by said first interface; and a finite path removal module configured to generate a second model substantially equivalent to the first model obtained by said second interface, the second model excludes a portion of the at least one finite path, the second model is configured to be utilized in model checking.