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

In this paper, we provide a necessary infrastructure todefine an abstract state exploration in the HOL theorem prover. Ourinfrastructure is based on a deep embedding of the Multiway DecisionGraphs (MDGs) theory in HOL. MDGs generalizeReduced Ordered Binary Decision Diagrams (ROBDDs) to represent andmanipulate a subset of first-order logic formulae. The MDGs embedding is based on thelogical formulation of an MDG as Directed Formulae (DF). Then, theMDGs operations are defined and the correctness proof of each operationis provided. The MDG reachability algorithm is then defined as a conversion that uses ourMDG theory within HOL. Finally, a set of experimentations overbenchmark circuits has been conducted to ensure the applicability andto measure the performance of our approach.