1. Method for verifying linear hybrid automaton, the method comprising: using a reachability analysis of a linear transition system (LTS) to verify a linear hybrid automata (LHA) system; generating initial abstract model based on an original Linear-Time Temporal Logic (LTL) specification; validating a counterexample using an approach of linear constraints satisfaction; identifying a fragment in the counterexample by iteratively applying the approach of linear constraints satisfaction; and refining the original LTL specification based on the fragment derived.
19. The method of claim 1 , further comprising: implementing the reachability analysis to verify that the linear hybrid automata system on a software tool that is executed on a computer system having associated microprocessor means including an arithmetic processor and associated memory means.