Verification of linear hybrid automaton
AssigneeGM Global Technology Operations LLC
InventorShengbing Jiang
Life of this patent
Estimating the term…
Abstract
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.
Claims20
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.
Method for verifying linear hybrid automaton, the method comprising:
- generating an 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 in a predefined number of times;
- and
- refining the original LTL specification based on the fragment derived.
Dependencies are inferred from the claim text.