Algebraic Model Checking

Three algebraic approaches to model checking are presented and compared with each other with respect to their range of applications and their degree of automation. They have been implemented and tested in our Haskell-based formal-reasoning and -presentation system Expander2. Besides realizing and integrating state-of-the-art proof and computation rules the system admits the co/algebraic specification of the models to be checked in terms of rewrite rules and functional-logic programs. It also offers flexible features for visualizing and even animating models and computations. This paper does not present purely theoretical work. Due to the increasing abstraction potential of programming languages like Haskell, traditional gaps between specification formalisms and their executable implementations as well as between systems developed in different communities are going to vanish. The topics discussed in this article and the way of their presentation reflect this fact