Tag Archives: memoization

CTL Model Checking in Haskell: A Classic Algorithm Explained as Memoization

As an exercise, since my reading group was discussing model checking this week, I implemented the classic model checker for CTL specifications from the 1986 paper Automatic Verification of Concurrent Systems Using Temporal Logic Specifications by EM Clarke, EM Emerson, AP Sistla. The “efficient algorithm” presented in the paper is, upon reflection, merely […]