Reachability Analysis Of Linear Hybrid Automata By Using Counterexample Fragment Based Abstraction Refinement

We study the reachability problem of linear hybrid automata. We introduce the notion of linear transition systems that are purely discrete transition systems and do not involve any continuous time dynamics by differential equations. We prove that the reachability problem for linear hybrid automata is equivalent to the reachability problem for linear transition systems. We provide an approach for the reachability analysis of linear transition systems by using counterexample fragment based abstraction refinement. The counterexample validation problem is reduced to the linear constraint satisfaction problem and can be solved by using methods like linear programming. An algorithm of good complexity is provided for the counterexample fragment identification. A new approach for the abstraction refinement is provided based on the identified counterexample fragment and it does not require any computation or representation of reachable state sets in the abstract model, which makes the approach very promising for systems with large number of variables.