An Abstract Reachability Approach by Combining HOL Induction and Multiway Decision Graphs

作     者：Sa'ed Abed Otmane Ait Mohamed Ghiath Al-Sammane 

作者机构：ECE DepartmentConcordia UniversityMontrealCanada 

出 版 物：《Journal of Computer Science & Technology》 (计算机科学技术学报（英文版）)

年 卷 期：2009年第24卷第1期

页      面：76-95页

核心收录：

学科分类：08[工学] 080203[工学-机械设计及理论] 0802[工学-机械工程] 

主　　题：HOL theorem prover multiway decision graphs correctness reachability analysis 

摘      要：In this paper, we provide a necessary infrastructure to define an abstract state exploration in the HOL theorem prover. Our infrastructure is based on a deep embedding of the Multiway Decision Graphs （MDGs） theory in HOL. MDGs generalize Reduced Ordered Binary Decision Diagrams （ROBDDs） to represent and manipulate a subset of first-order logic formulae. The MDGs embedding is based on the logical formulation of an MDG as Directed Formulae （DF）. Then, the MDGs operations are defined and the correctness proof of each operation is provided. The MDG teachability algorithm is then defined as a conversion that uses our MDG theory within HOL. Finally, a set of experimentations over benchmark circuits has been conducted to ensure the applicability and to measure the performance of our approach.