| 摘要 |
The present invention provides a method for verification of linear hybrid automaton by generation an initial abstract model based on an original Linear-Time Temporal Logic (LTL) specification, validating a counterexample using an approach of linear constraints, identifying a fragment in the counterexample by iteratively applying an approach of linear constraints satisfaction in a limited number of times, and refining the original LTL specification based on the fragment derived.
|
