Hal (and other interested parties): I used Haskell to implement a model checker for a group of logics of time and knowledge. In practice these are a bunch of extensions to the classic CTL algorithms implemented in SMV [1].
The program itself (in terms of LOC) looks mostly like a compiler, and so the standard arguments apply. However, Haskell is absolutely perfect for implementing the SMV algorithms (and our variants) as they are cast in terms of fixpoints of boolean functionals. Moreover performance isn't an issue as a C library does the heavy lifting. (The program uses BDDs at the moment.) WRT Haskell, the only worry I had was that the program might leak space in difficult-to-resolve ways, and the usual problem of BDD variable ordering being difficult to control. cheers Peter. [1] SMV itself is actually a LISP program written in C. (I think this is self-evident from even a cursory glance, but the real giveaway is their AST: who else, apart from a seasoned LISP hacker, would use CONS cells for everything?) _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
