Exploration Algorithms Of Abstraction Frontier On Craig Interpolation

Craig interpolation is an efficient method used to refine abstraction in model checking.However,the performance of model checkers varies from interpolations,some of which lead to divergence whilst others contribute to convergence.To obtain the interpolations that promote the rapid convergence of model checkers,the technique of interpolation abstraction emerges.Based on it,interpolation solving problem can be transferred into the exploration problem of abstraction frontier in abstraction lattices.In this thesis,the author improves the existing algorithm and presents two new heuristic exploration algorithms so as to make the exploration of abstraction frontier more efficient and accurate.The basic idea of the algorithm proposed by J.Leroux and P.Ruemmer is as follows:based on depth-first search and binary search,the exploration starts from feasible elements and ends with so-called abstraction frontier element whose direct successors are all infeasible.However,due to its relatively large order relation,when system scale is enlarged,the exploration paths are accordingly elongated and the traversed elements are greatly increased,which will reduce the exploration efficiency.Concerning it,the author proposes an exploration algorithm of abstraction frontier based on breadth-first search.This exploration starts from the top of lattice,proceeds from up to down layer by layer and deletes all predecessors of explored feasible elements,so as to cut down the exploration space sharply.Additionally,in this thesis,the author proves termination and correctness,as well as,analyzes efficiency of the algorithm qualitatively and quantitatively and demonstrates that this new algorithm is comparatively efficient comparing to the original one by concrete examples.In order to refine abstraction frontier and make the quality of elements in it better,that is,to improve the rapid convergence of model checkers,this thesis introduces anti-monotonic evaluation function into exploration algorithm of abstraction frontier based on breadth-first search,puts forward a new refinement exploration algorithm of abstraction frontier with evaluation function and proves its termination and the correctness.Furthermore,the author analyzes its efficiency qualitatively and quantitatively and illustrates the executing process through concrete examples.Not only does the algorithm refine abstraction frontier,but it also contributes to reducing the exploration space and improving the algorithm efficiency.