Mathematical Pamphlet
Mathematics, Haskell, and little bit of Linux
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 a memoized traversal of the state machine, so I combined it with
a modified version of
* Monadic Memoization Mixins
by D
Brown, WR Cook
which actually eliminated an auxilliary function from the algorithm,
yielding an efficiently-executable 20-line Haskell specification of the
meaning of CTL (which is probably clearer than my English prose
explanation, and certainly more fun to play with).
redyellowgreen.png
This post is, as usual, literate Haskell. Load it up in GHCi,
Haskell-mode, or compile it with |ghc --make| and try it out. Maybe you
can convince my state space exploration not to terminate :-)
> {-# LANGUAGE TypeOperators,ScopedTypeVariables #-}
> module CTLModelChecker where -- rhz added this line 8/5/08
> import qualified Data.Map as M
> import qualified Data.Set as S
> import Data.List
> import Control.Monad
> import Control.Monad.State hiding (fix)
Memoization Mixins
Here is the easy example from the Brown-Cook paper, before getting on to
model checking.
To enable functional mixins, we write our functions using open
recursion. Instead of a function of type |a -> b| we write one of type
|Gen (a -> b)| and then later "tie the knot" with |fix| (reproduced here
for reference)
> type Gen a = (a -> a)
> fix :: Gen a -> a
> fix f = f (fix f)
The classic example they start with is calculating the nth fibonacci
number, but don't stop reading just because this example is simple! It
is just to illustrate the technique.
> fib :: Int -> Int
> fib 0 = 0
> fib 1 = 1
> fib (n+2) = fib n + fib (n+1)
By the time you get to |fib 30| it takes a dozen or seconds to return on
my poor old computer. Rewrittin in open recursion as
> gFib :: Gen (Int -> Int)
> gFib recurse 0 = 0
> gFib recurse 1 = 1
> gFib recurse (n+2) = recurse n + recurse (n+1)
> fib' = fix gFib
This |fib'| has essentially the same performance, up to constant
factors: slow.
To enable us to store the memoization table in something like a |State|,
we parameterize over an underlying monad. A beautiful technique in its
own right, if you ask me. I agree with the authors that open recursion
and monadification are important and powerful enough to deserve language
support; you probably will think |gmFib| below looks a bit crufty.
> gmFib :: Monad m => Gen (Int -> m Int)
> gmFib recurse 0 = return 0
> gmFib recurse 1 = return 1
> gmFib recurse (n+2) = do a <- recurse n
> b <- recurse (n+1)
> return (a + b)
And now we can mix in |memoize|
> type Memoized a b = State (M.Map a b)
> memoize :: Ord a => Gen (a -> Memoized a b b)
> memoize self x = do memo <- check x
> case memo of
> Just y -> return y
> Nothing -> do y <- self x
> store x y
> return y
> check :: Ord a => a -> Memoized a b (Maybe b)
> check x = do memotable <- get
> return (M.lookup x memotable)
> store :: Ord a => a -> b -> Memoized a b ()
> store x y = do memotable <- get
> put (M.insert x y memotable)
Here's the final fib, which returns instantly up to at least |10000|.
> fib'' n = evalState (fix (gmFib . memoize) n) M.empty
Computation Tree Logic (CTL)
The language for which Clarke et al give a graph-based algorithm is
called CTL; nowadays people are interested in a bunch of variants like
CTL* and ACTL. I'm not a model-checking researcher so I don't really
know the subtleties of their differences. CTL is a logic for specifying
certain restricted kinds of predicates over the possible traces of a
state machine, for today a finite state machine.
Let's just look at the Haskell definition:
> data CTL p = TT | FF
> | Atomic p
> | Not (CTL p)
> | And (CTL p) (CTL p)
> | AllSucc (CTL p)
> | ExSucc (CTL p)
> | AllUntil (CTL p) (CTL p)
> | ExUntil (CTL p) (CTL p)
> deriving (Eq,Ord)
Some of these are simply your usual logic
* |TT| holds of any state
* |FF| never holds
* |Atomic p| is some atomic proposition over a state, like
inequality over program variables, etc.
* |Not| and |And| have their expected meanings
The successor constructions let you talk about "the next" state:
* |AllSucc f| (respectively |ExSucc|) holds of a state |s| when the
formula |f| holds for all (respectively some) successor states.
The interesting ones though, are "Always Until" and "Exists Until":
* |AllUntil f1 f2| holds of a state |s| when for /all/ prefixes of
any trace starting at |s| you eventually reach a state satisfying
|f2|, and everywhere along the way |f1| holds.
* |ExUntil| is the existential version of that.
We can then define some more predicates like "forever in the future" and
"eventually"
> allFuture f = AllUntil TT f
> existsFuture f = ExUntil TT f
> allGlobal f = Not(existsFuture(Not f))
> existsGlobal f = Not(allFuture(Not f))
Now, to apply a formula to a state machine, first I need the state
machine. I'll just represent it by its successor function.
> type Succ st = st -> [st]
And we need some interpretation of atomic formulas as predicates over states
> type Interp p st = p -> st -> Bool
And since I'm using a monadified form of computation, I will lift a
bunch of operations into monads to make everything readable.
> andThen,orElse :: Monad m => m Bool -> m Bool -> m Bool
> andThen = liftM2 (&&)
> orElse = liftM2 (||)
> notM :: Monad m => m Bool -> m Bool
> notM = liftM not
> anyM,allM :: Monad m => (s -> m Bool) -> [s] -> m Bool
> allM f = liftM and . mapM f
> anyM f = liftM or . mapM f
The Model-Checking Algorithm
In the Clarke et al paper, the algorithm is expressed by induction on
the formula |f| you want to check: First, label your state-space graph
with all the atomic formula that hold at each state. Then, label with
each the compound formula of height two that holds. Etc, etc, you are
guaranteed that the graph is already labeled with each subformula by the
time it becomes necessary.
Like dynamic programming, this is simply a complicated way of expressing
memoization. In fact, they even use a depth-first search helper function
that is completely eliminated by expressing it as a memoized function.
This code is considerably shorter and, I think, clearer than the
pseudocode in the paper, modulo the overhead of "mixing in" and "tying
the knot".
Today we have fancy algorithms involving BDDs and abstraction, so I'm
not claiming anything /useful/ except pedagogically. I do wonder,
though, if this code gains something through laziness. It certainly
traverses the state space fewer times (but I'm sure an implementation of
their algorithm would do similar optimizations).
> checkCTL :: forall p st . (Ord p, Ord st) =>
> Interp p st -> Succ st -> st -> CTL p -> Bool
> checkCTL interp succ init f =
> evalState (fix (gCheckCTL . cyclicMemoize2 False) f init) M.empty
> where
> gCheckCTL :: Monad m => Gen (CTL p -> st -> m Bool)
> gCheckCTL recurse f s = checkFormula f
> where checkFormula TT = return True
> checkFormula FF = return False
> checkFormula (Atomic p) = return (interp p s)
> checkFormula (Not f1) = notM (recurse f1 s)
> checkFormula (And f1 f2) = recurse f1 s `andThen` recurse f2 s
> checkFormula (AllSucc f1) = allM (recurse f1) (succ s)
> checkFormula (ExSucc f1) = anyM (recurse f1) (succ s)
> checkFormula (AllUntil f1 f2) = recurse f2 s `orElse`
> (recurse f1 s `andThen` allM (recurse f) (succ s))
> checkFormula (ExUntil f1 f2) = recurse f2 s `orElse`
> (recurse f1 s `andThen` anyM (recurse f) (succ s))
You may also notice that I cheated a little, perhaps. I have used
|cyclicMemoize2| instead of |memoize|:
> cyclicMemoize2 :: (Ord a, Ord b) => c -> Gen (a -> b -> Memoized (a,b) c c)
> cyclicMemoize2 backEdge self x y = do memo <- check (x,y)
> case memo of
> Just z -> return z
> Nothing -> do store (x,y) backEdge
> z <- self x y
> store (x,y) z
> return z
One reason is simply that I need a curry/uncurry wrapper for my two
argument monadified function. The deeper thing is that |cyclicMemoize2
False| inserts a fake memoization entry while a computation is
progressing. If there is ever a "back edge" in the search, it will
return this dummy entry. For CTL, the auxilliary depth-first search used
in the paper for |AllUntil| returns |False| in these cases, so I seed
the memo table accordingly. This is because by the time you have
recursed around a cycle, that means that the |f2| you are searching for
did not occur on the cycle, so it never will.
To play with it, I've only made a couple of examples involving stop
lights (of occasionally curious colors). I'd love more, and you'll
undoubtedly find bugs if you actually run something significant.
> ex1interp p s = (p == s)
> ex1succ "Red" = ["Green"]
> ex1succ "Green" = ["Yellow"]
> ex1succ "Yellow" = ["Red"]
> ex2succ "Red" = ["Green"]
> ex2succ "Green" = ["Yellow", "Orange"]
> ex2succ "Orange" = ["Red"]
> ex2succ "Yellow" = ["Red"]
But it looks kind of OK,
*Main> let ch2 = checkCTL ex1interp ex2succ
*Main> let ch1 = checkCTL ex1interp ex1succ
*Main> ch1 "Red" (existsFuture (Atomic "Red"))
True
*Main> ch1 "Red" (existsFuture (Atomic "Blue"))
False
*Main> ch2 "Green" (ExUntil TT (Atomic "Red"))
True
*Main> ch2 "Green" (ExUntil (Atomic "Green") (Atomic "Orange"))
True
*Main> ch1 "Green" (Not (AllUntil (Not (Atomic "Yellow")) (Atomic "Red")))
True
*Main> ch1 "Green" (Not (ExUntil (Not (Atomic "Yellow")) (Atomic "Red")))
True
*Main> ch2 "Green" (Not (ExUntil (Not (Atomic "Yellow")) (Atomic "Red")))
False
Quite fun!
redyelloworangegreen.png
Filed under: Haskell
, Mathematics
, Reading
by Kenn
Leave a Reply
You must be logged in
to post a comment.
« Using HaXml to make a PDF slideshow from an Inkscape SVG
*
*
Categories
o Haskell (7)
o LaTeX (4)
o Linux (6)
o Mathematics
(9)
o Reading (2)
*
Archives
o May 2008
o April 2008
o March 2008
o December 2007
o November 2007
o March 2007
o February 2007
o June 2006
o March 2006
o January 2006
*
Blogroll
o A Neighborhood of Infinity
o Lambda the Ultimate
o Michi's blog
o The Comonad.Reader
*
Meta
o Register
o Login
o Entries RSS
o Comments RSS
o Valid XHTML
Mathematical Pamphlet is proudly powered by WordPress
and WPDesigner .