A Simple CTL Model Checker in Haskell

Here is a simple Haskell implementation of the model checking algorithm outlined in these slides. It does not use any fancy tricks (like BDDs) to make it efficient, so it will probably only work on toy examples.

• testmc.hs: a main module for testing the model checker. To run all the tests, do runghc testmc.hs.
• MC.hs: the model checker
• Model.hs: representation of models
• CTL.hs: representation of CTL formulas
• Extra.hs: auxiliary functions

A package with the above files for download: mc.tar.gz