About SEG
SEG News
SEG Seminar
Internal Site
Hot Link
Contact SEG

报告一:Deriving Unbounded Proof of Linear Hybrid Automata From Bounded Verification


简介:This talk presents a technique that can derive, in some cases, a proof of unbounded reachability argument of Linear Hybrid Automata (LHA) from a Bounded Model Checking (BMC) result. During BMC checking of LHA, typical procedures can discover sets of unsatisfiable constraint cores, a.k.a. UC or IIS, in the constraint set according to the BMC problem. Currently, such unsatisfiable constraints are only fed back to the constraint set to accelerate the BMC solving. In this talk, we propose that such unsatisfiable constraint core can be utilized to give general unbounded verification result of the model. We propose to map the unsatisfiable constraint cores back into path segments, which are not feasible, in the graph structure of the LHA model. Clearly, if all the potential paths which can reach the target location in the graph structure have to go through such infeasible path segment, the target location is not reachable in general, not only in the bound.


To solve such problem, we propose to encode the infeasible path segments as LTL formulas, and present the graph structure of an LHA as a transition system. Then, we can take advantage of mature LTL model checking technique to verify whether there exists a candidate path which can reach the target according to the LTL formulas. We implement this technique into a new version of BACH, the experiments show that the performance of our tool outperforms the-state-of-the-art competitors, significantly.