This post is a general introduction to model checking, and is written in the style of a hands-on tutorial. The intended audience of this article are programmers of functional languages, such as Haskell, not afraid of monads, yet unfamiliar with model checking or bisimulation. (Since this is a tutorial, “you” is the reader, and “we” are the reader and the author.) We explore only the most basic concepts of model checking here, all based around toy examples. Over the course of this tutorial, we will use the programming language Haskell to make the examples more concrete.
Let’s get started with some background. Suppose that we are on an assignment to program a traffic light controller in Haskell, and suppose we have never worked on this kind of application before. The first thing to do is to summarize our plan of approach:
- We first develop a small proof of concept, to show that we understand the problem domain. We are not yet implementing an efficient solution nor a fully satisfactory solution. It’s fine if we throw away all our coding work here: the main importance is getting an intuitive feeling for the domain.
- To do this, we need to gather a list of assumptions on which we will base the rest of our work. These assumptions should be reasonable, in the sense that they are acceptable for a good reason. It’s fine if we miss out the details of a real solution. It’s also fine to limit these assumptions to only small cases.
- Then we proceed with the development as a (simplified) scientific endeavor: we test out our theories (read: programs) and try hard to shoot holes in it. If we cannot find any problems, we assume that the theory (read: program) is correct until shown otherwise. We then remove assumptions and repeat.
Let’s limit our domain to one particular instance first. We describe the following scenario: we program the controller for the traffic lights at a regular two road crossing, as depicted below. Each road has two lanes and automobiles can move on one lane in one direction. We thus have four lanes in total.
The lanes are named A1, A2, B1, B2. Each lane has one traffic light: namely the light that instructs automobiles whether to go onto the crossing or not. (The traffic lights are positioned at the tip of the arrow which points to the crossing.) Let’s keep the scenario simple and not deal with the positions of automobiles. We just identify each traffic light is in a certain state, and assume that drivers follow these instructions precisely. A typical traffic light is either red (stop), orange (stop) or green (go). We have four such traffic lights. In Haskell we code:
-- TL: Traffic Light data TL = Red | Orange | Green deriving (Eq, Ord, Show) data Road = A1 | A2 | B1 | B2 deriving (Eq, Show) newtype State = State (Road -> TL)
(Haskell code: we define traffic light states and roads. The state of the traffic controller is a map of roads to traffic light states.)
Now that we have a state representation, we will identify state transitions. First, we want to identify all possible transitions. This is done quite easily using a List monad:
- Given a current state, we can pick one of the four traffic lights (A1 up to B2).
- Given the current light color, we know what possible next colors it has: green can transition to orange, orange can transition to red, and red can transition to green.
Before we give the Haskell code, it is nice to have a textual representation of State:
roads :: [Road] roads = [A1, A2, B1, B2] instance Show State where show (State color) = unwords $ map s roads where s road = show road ++ ":" ++ show (color road)
(Haskell code: roads defines a list of all roads we consider and the state can be showed on the terminal. unwords is in Prelude. Run State (\x -> Red) in GHCi and you get A1:Red A2:Red B1:Red B2:Red to see that all lights are red.)
Now for the state transition, consider the following function:
next :: TL -> TL next Red = Green next Green = Orange next Orange = Red trans :: State -> [State] trans (State f) = do road <- roads let g road' | road' == road = next (f road') – update | otherwise = f road' -- fallback return (State g)
(Haskell code: single state transition step. From a current state, we can update one of the traffic lights.)
We can supply our previous example of all-red to the transition function. We then get a list of options; each option represents a single step that can be taken. In this case, the result becomes: [A1:Green A2:Red B1:Red B2:Red,A1:Red A2:Green B1:Red B2:Red,A1:Red A2:Red B1:Green B2:Red,A1:Red A2:Red B1:Red B2:Green]. What if we want to apply the transition state twice? We simply map it over the resulting list as follows:
trans2 :: State -> [State] trans2 x = concatMap trans (trans x)
(Haskell code: applying transition function twice.)
We could equally map it three times, or an indefinite number of times. This simply generates the full state space. By easy computation we know how many different unique elements there are in our state space: 4 roads mapped to 3 colors, i.e. 34 = 81 possibilities. That’s still manageable. But consider what happens if we wanted to model only 16 more roads: 320 = around 3.5 billion possibilities = around the number of transistors in an Apple A10 processor chip. This is called a state space explosion, i.e. the number of states grows extremely fast (exponentially) with only a slight increase in input size. With four roads, however, we can still manage. The state space is best described by four simultaneous state machines:
Note that in our previous computation we did not just multiply the two sets: 3×4. There is a good reason why that calculation is wrong: it only computes the size of the pair (color, road) and not the assignment of a color to each road. A pair does not represent four independent traffic lights, no: the size of a pair computes just all possibilities of a single traffic light and a pointer to a single road. Such a (color, road)-pair cannot express that two roads have a different color at the same time.
The next thing we should discuss are safety properties. Now that we have an assignment of a color to each traffic light, can we also express what combinations are safe? That depends. We need a few more assumption here. Consider the automobile movements as depicted below:
Here, an automobile on lane A1 can turn right to B1. It can turn left to B2. It can go straight ahead, still on A1. And it can make a U-turn to lane A2. If we wish to prevent any kind of collision with this movement scheme, we assume that every traffic light requires mutual exclusion of the crossing. This means that of all four lights, at most one traffic light can be green at the same time. And what about orange, do we allow an orange and a green light? Again, that depends. In the most common interpretation, automobiles that cannot decrease velocity on time are allowed to pass orange. Thus, let’s assume that orange and green both let drivers pass. We thus have the following assumption:
H: At most one traffic light is not red.
This is called a safety predicate. Basically, that means the following Haskell code:
safeH :: State -> Bool safeH (State f) = (<= 1) $ sum $ do road <- roads return $ if f road == Red then 0 else 1
(Haskell code: a function that returns true whenever the crossing is safe according to H1. Clearly, State (\x -> Red) is safe, but State (\x -> Green) is not.)
So now we have the following ingredients: A. we have a state space, B. we have a safety predicate. Now let’s consider the state transition function again. We can make sure that the transition function is filtered and that it only includes safe states, as follows:
trans :: (State -> Bool) -> State -> [State] trans pred (State f) = filter pred $ do road <- roads let g road' | road' == road = next (f road') – update | otherwise = f road' -- fallback return (State g) transN :: (State -> Bool) -> State -> Int -> [State] transN pred init n = t n where t 0 = trans pred init t i = concatMap (trans pred) (t (i - 1))
(Haskell code: the transition function now allows filtering for only sane states. We also have a generalization of our concatMap trick of above.)
The new state space, with the safety predicate, can best be described as something that looks like the image below. Compare this to the image we saw earlier, with four independent traffic lights. Clearly, some kind of synchronization is happening now. This is depicted by the new box on top. The lines into the special box are dotted lines. These represents an internal action which models a transition that is not observable outside this system.
The diagrams we have seen can be simulated. Simulation has a very precise meaning, but the explanation given here is hopefully intuitively clear. Suppose that we play a game on top of the diagram. We place several pawns, say small coins, one on top of a single state within each traffic light. For example, we put the four coins all on top of the red state, one per traffic light. Then the game progresses as follows: we may choose to make one movement for a single coin only, and we must follow an outgoing arrow into a next state. The game we play in our minds is a simulation of the controller.
In the previous diagram, we could move the coins arbitrarily from each other. They are thus independent, as mentioned earlier. However, in this new diagram an additional game rule (or restriction, depending on your point of view) is applied: a coin may only move (via an internal action) to the synchronization state (S) when all other coins are on the red state.
So, an example game is the following.
- We start at the initial state. Say this is (red, red, red, red) for (A1, A2, B1, B2) respectively. We then choose to move the coin of A1 to the synchronization state.
- Now no longer all other coins are on the red state, so the coins on A2, B1 and B2 must wait.
- We can thus only move the coin from the synchronization state to green for A1. Again, all other coins must wait before we return to A1.
- Finally, when A1 moves from orange to red, can we make a new decision: what coin goes to synchronization state next?
Do note that the decision what coin will move is non-deterministic in both diagrams. However, non-determinism is limited in the latter case only when all coins are on the red states. Non-determinism implies that we do not know what action will be taken, but that does not matter from our perspective right now: any choice is possible and acceptable.
We still are on our way of programming a traffic light controller. We now have a clear idea in mind, namely how the system under the current assumptions is supposed to work. Can we implement a controller that actually satisfies the description given above? Yes, we can build a trivial controller: one that does nothing but sit still in the (Red, Red, Red, Red) state. It clearly is a valid controller, since it does not violate our safety predicate! But we find such a controller unreasonable; we could expect, at least, that it does something.
allRed :: State -> Bool allRed (State f) = and $ do road <- roads return $ f road == Red controller :: State -> State controller s | allRed s = State g where g x | x == A1 = Green | otherwise = Red controller (State f) | otherwise = State g where g x | x == A1 = next (f x) | otherwise = f x
(Haskell code: the first function returns true if all states are red, the controller always moves A1 to the next state.)
Now we have implemented a controller that does something. But is it a correct controller? It depends. Let’s have a look at its visited state space:
The diagram on the lower right is controller. The diagram on the upper left is the one we saw before. Now let’s consider the following thought-leap: before, we were simulating the upper left diagram in our head. Now, we have written a program, on the lower right, that also simulates the upper left diagram! Now, a natural question one can ask when simulating, is the following: is the simulation of our program complete? Does the simulation correctly represent our original diagram? To answer that question, we finally have to look at a more advanced concept of simulations: bisimulations.
Consider these questions: in the original state space diagram, we had a rule that says that only if all other coins are on the red state may we do an internal action to the synchronization state. Our implementation is correct, but only in a narrow sense: it only makes such a step when all other coins are on the red state, but the other coins are always on the red state! That seems to be fishy. What is going on here?
Also, in the original state space diagram we had more choices. Namely, once all coins are on the red state, we have a non-deterministic choice of four actions (each of the outgoing dotted arrows). The point is this: although the lower right diagram can simulate the upper left diagram, it does not hold that the upper left diagram can simulate the lower right diagram! Put differently:
controller (State (\x -> Red) simulates trans safeH (State (\x -> Red)),
trans safeH (State (\x -> Red)) does not simulate controller (State (\x -> Red).
Can we solve this? Well let’s try. Say we are playing two games, at the same time: one game takes place on the upper left diagram (the original state space of safeH) and the other game takes place on the lower right diagram (controller). If we say one game simulates the other, then: for every step we take in the one game, we can mimic it in the other. So, if we say controller simulates safeH then we mean: every state transition taken by controller can also be taken by safeH. There is one caveat: we need to ensure that every step also corresponds to the same externally observed behavior. For example, it is absurd to mimic a transition to the red state (in the specification) by a transition to the green state (in the implementation), because that constitutes a clear failure of implementation.
Here we encounter a subtlety of the differences of internal and external actions: internal actions (e.g. the synchronizer) may or may not be mimicked, but external actions (e.g. the color of a traffic light) must be mimicked. But for the sake of simplicity, we will not deal with this subtleness here.
OK, so what happens if we have two diagrams and each simulate each other? Does that solve our problem of checking whether two systems have the same model? No, again, we encounter a subtle difference. Let me illustrate that with another example of a game play on diagrams:
In this diagram we see two state spaces: on the left, we have three states (a, b, c) and on the right we have four states (a, b, another b, c). Note that these two state spaces simulate each other:
- If we put a coin on both “a” states. Whenever an action happens on the left side, we can take the action straight up to “b” on the right (so it correctly simulates). Whatever action happens on the right side, we can mimic it on the left: if we take the action straight up to “b”, then we go to “b”. If we go to the other sideways “b”, we can also mimic it to “b”.
- If we put a coin on both “c” states. Same thing applies here: all actions can be mimicked.
- The only thing that nags us is the following: we know that the left diagram is other than the right diagram, since it has one state less. But apparently, each simulate the other. We cannot find any instance of a game play where the one is not mimicked by the other!
Here comes bisimulation to the rescue. To consider these models different, we need to consider what it means that they are different. Simply mimicking actions certainly is not enough; the models need to have the same structure too! The side-track that we see in the diagram above clearly is of different structure. In the case of writing programs and state spaces, and checking whether they have the same model, it is important that we also know they have the same structure.
Consider, for example, a controller that precisely mimics our space as before, but now has a similar defect as in the last example:
For whatever reason, our implementation contains a bug. Suppose that there is a very small chance that from the green state in B2, we end up in the dead-end orange. This non-deterministic choice is modelled, as can be seen in the lower right part of the diagram. Note that the specification simulates the implementation here, and also the implementation simulates the specification. Even if we end up in that dead-end orange state, we can still mimic it by going to orange in the specification.
Bisimulation solves this mismatch of structure. It adds another rule: at any time, we may swap the two models. So in the previous case, if we ever end up in the dead-end orange state, we simply swap the two models. Then we are back in the specification, and we can expect from the dead-end that it also mimics the transition to red. In this case it cannot: so the bisimulation fails. Now we can see the difference in structure, hence detect these kinds of differences in models.
This concludes this post. You can still continue to work on the traffic controller case, if that has your interest. There is still clearly a lot of work left before it becomes an actual, real, traffic controller. But as long as the main idea of this post remains clear:
- If you first specify your intended state space,
- And you define properties that narrow the state space down to a specification,
- Then you can work on the implementation,
- And use model checking techniques to verify that the models of your specification and your implementation match in behavior and structure.
One important technique in model checking is bisimulation, that not only expects the implementation and specification to have the same externally observable effects. For bisimulation, it is moreover required that the two models have the same structure. E.g. one model that suddenly stops doing anything useful, or has a code path in which suddenly only say 50% of all functionality works, is still correct in one sense (just as the trivial controller was correct). But a good implementation mimics not only all observable effects, but does so with the same structure as the specification.