Relaxation Refinement: A New Method to Generate Heuristic Functions

摘要: In artificial intelligence, a relaxation of problem is an overapproximation whose solution in every state explicit search provides heuristic distance estimate. The guides the exploration, potentially shortening by exponentially many states. big question how good for at hand should be derived. model checking, overapproximations are called abstractions , and abstraction refinement powerful method developed to derive approximations that sufficiently precise verifying system hand. our work, we bring these two paradigms together. We pioneer application (predicate) generation functions intelligently adapted investigate process generating differ from used verification context. do so context DMC timed automata. obtain variety interesting insights about this approach.