Safety Checking By Problem Solving

摘要

Model checking has been receiving more and more attentions recently. Many effective techniques are presented, such as those algorithms based on OBDD, SAT, and ATPG In this paper, we present a novel paradigm which proposes to do safety checking by problem solving, a seriously studied theme in artificial intelligence. We first translate the safety checking problem into a planning problem, which in turn be solved by general problem solving method. By a case study we describe the checking procedure on semaphore. Experiments on several other examples further demonstrate the validity of the proposed method.