5. The method of claim 3 , further comprising: checking the feasibility of the counterexample in the LTS to determine whether a corresponding run exists in the LTS for the counterexample.
5. The method of claim 3 , further comprising: checking the feasibility of the counterexample in the LTS to determine whether a corresponding run exists in the LTS for the counterexample. 6. The method of claim 5 , further comprising: generating a linear constraint satisfaction problem for checking if a corresponding run exists in the LTS; solving the linear constraint satisfaction problem to determine if a run of bad location sets exists in the LTS for the counterexample; and using the run as a concrete counterexample if the bad location sets is reachable in the run of the LTS, wherein the run of bad location sets is reachable in the LTS if the LTL specification is not satisfied.