Yesterday, I handed in an extended essay that I've been working on since last summer on the subject of probabilistic model checking. I've blogged a bit about it before, but I thought it might be nice to write about what I mean when I talk about model checking and why I think it's cool and worth studying.
Model checking techniques were originally developed by computer scientists to help with the design of systems (especially hardware systems, although they are increasingly useful for software as well). One of the really cool things about it, though, is that it is almost directly applicable to research in all sorts of other fields (albeit not always for the same purpose).
What is model checking?
Broadly speaking, 'model checking' refers to a range of techniques used to study systems. If you think about it for long enough, though, anything can be seen as a kind of system, from my laptop to my immune system or the solar system. That can make it difficult to develop general techniques for analysing systems! After all, my laptop and my immune system don't look very similar. But if there's one thing computer scientists love doing, it's developing general techniques for everything.
A lot of computer science comes down to two things: abstraction, and algorithms1. So, the first thing we do is abstract everything. We take our system, and turn it into an abstract model. You're creating a probabilistic security protocol? That might turn out to be a Markov chain. Studying the human impact on the behaviour of bottlenose dolphins? There's a Markov chain for that, too. (Seriously). We turn our big, messy, real-world system into a rigorously defined mathematical model that we know how to reason about already.
Here's a Markov chain. Not as cute as the dolphin, but easier to plug in to an algorithm!
Next, we think about what properties of the system we would like to study. When we do model checking, we check specific facts about the systems we're looking at. Model checking can try to answer questions like 'will the brake engage within 0.2 seconds after I press the pedal?', but it can't answer questions like 'does my system contain bugs, and if so, what are they?'2.
We take the properties we want to check, and abstract them by turning them into logical formulas. There are loads of different kinds of logic (if you've taken a knowledge representation course you've probably encountered more logics than you ever wanted to know about), and different logics can specify different kinds of properties, or properties of different kinds of systems. But ultimately it comes down to writing a formula which can be applied to the model of the system we created earlier, such that the formula will be satisfied if and only if the property is true for the system we're studying3.
Why is it cool?
OK, so we've reduced the huge problem of answering questions about systems to logical satisfiability. What was the point?
In computer science
Model checking is really useful for designing certain systems. It's probably not worth bothering to apply model checking to your program to generate ASCII art of cats. But if you're designing and manufacturing millions of incredibly complicated and expensive computer chips, techniques from model checking can help make sure you're not going to get hundreds of thousands of customers demanding refunds because your chip crashes whenever the user divides by a certain number. Likewise, if your software is going to be on a spacecraft being sent to the edge of the solar system, model checking can give you some level of assurance that you're not going to get a blue screen of death somewhere on the way (it might be hard to push a patch for it... I hear there are barely any decent WiFi hotspots around Neptune). Likewise, model checking a dam-management system or some medical hardware might save the lives of people who depend on those systems.
Beyond computer science
But computer scientists have been talking about model checking for decades. What's really cool is that scientists are starting to use model checking to study other kinds of systems.
For example, suppose a biologist is studying how enzyme levels vary in lung cells in certain conditions. In this case, they're not designing a system -- the system already exists in your body. However, a useful thing to do is to design mathematical or computational models of the system, which capture the behaviour being studied. In order for the model to be useful, it needs to have certain properties in common with the system being modelled. That's where model checking comes in! Instead of checking that we've designed the system correctly, we can use model checking techniques to verify that the observed behaviour of a real system is reflected in our model of it. So we turn our lung cells into Markov chains and use model checking to verify that they still behave the way they do in the body. Then the scientists can use the Markov chains to study the properties of those lung cells without having to muck around with quite so many actual lungs!
This has the potential to be applied anywhere that these kinds of models are used (and they're used nearly everywhere). I think it's really cool that techniques developed to study computer systems can be applied almost directly to all kinds of other systems! It really highlights the mathematical nature of theoretical computer science, and the power of those two principles: abstraction and algorithms.
If you're interested in more technical details of how model checking is done, check out this blog post I wrote a little while ago!
I feel like I heard a quote about how computer science all boils down to abstraction and algorithms somewhere, but I can't remember where. Please get in touch if you know the source! ↩
Model checking is just one branch of a bigger field known as formal verification. Other verification techniques can answer more general questions. But someone will always have to specify one way or another what looks like desired behaviour and what looks like a bug. One person's bug might be exactly what another person was going for, so it's hard for an algorithm to distinguish between them without some guidance! ↩
You might think that 'model checking' is called that because we check properties of models of systems, but in fact the name comes from the fact that we check whether the system is a 'model' for the logical formula specifying the property we're checking. This is just a confusing piece of terminology from logic meaning that the system satisfies the formula! ↩