LCF-style Platform based on Multiway Decision Graphs

AbstractThe combination of state exploration approach (mainly model checking) and deductive reasoning approach (theorem proving) promises to overcome the limitation and to enhance the capabilities of each. In this paper, we are interested in defining a platform for Multiway Decision Graphs (MDGs) in LCF-style theorem prover. We define a platform to represent the MDG operations: conjunction, disjunction, relational product and prune-by-subsumption as a set of inference rules. Based on this platform, the reachability analysis is implemented as a conversion that uses the MDG theory within the HOL theorem prover. Finally, we present some experimental results to show the performance of the MDG operations of our platform