Model checking ASM: the MDG approach

Abstract State Machines (ASM) is a powerful means for modelling and analysing various kinds of system, software as well as hardware systems. Our aim is to support the ASM method with tools for analysis. For this concern we use the ASM Workbench as a core tool. In this work we introduce an interface from the ASM Workbench to the MDG package. This package provides basic functionality and algorithms for Multiway Decision Diagrams (MDG) that are sufficient to develop a model checker for our needs. These needs are determined by our experience in model checking ASM on various examples so far. Our claim is that the use of MDG is very well suited for model checking ASM