This year, I’m doing research with my professor on model checking and verification. More specifically, analyzing an open problem by Thomas Schelling. The open problem is to do come up with a more formal analysis and precise formulation of certain criteria that the Schelling model tries to fulfill. To put it in simple terms, the Schelling model is about racial segregation and whether people of different types will mix evenly if they even have a slight preference for their own race.

But first, we need to think broader. In the broader perspective, having a more precise formulation is really important. That’s because there are many systems that are probabilistic, and being able to describe them precisely helps other stakeholders involved to make more informed decisions. For example, the software glitches in Toyota Prius caused 185,000 cars to be recalled when good model checking could be used to make sure the system doesn’t mess up.

The best thing I’ve read was the comparison between model checking and testing. Testing is to verify the presence of errors, and not their absence. More precisely, when we test, there are errors that we may not be able to catch (because it requires prior knowledge of what errors could happen), and that requires model checking to first consider all possible ways the system could end up in, and formally ensure that it fulfills the specifications of its task to the degree we want it to. This is really hard to do mechanically and so we rely on math to rigorously verify the models we use.

Now what entails model checking? First, coming up with a way to model a certain problem. There are many techniques to approach this, but the one I’m trying out is transition systems, or how a system would progress from one point to another, considering all the possible states a system could move into. Next is to come up with certain properties that I want the model to fulfill. There are several terminology for properties, for example, one basic property being reachability. What is the probability of an algorithm terminating successfully / error occurring during execution? Another property is long-run behavior for example. Does a system oscillate between two states in the long run, or is there a limit to changes made to the system?

And so there are a few ways to go about doing this. To compute reachability properties, compute as a sum of probabilities if the system is finite. If infinite, then you can’t compute (cause the computer will just go on and on forever). Instead, derive a linear equation system that best fits the reality. From there, solve for all the states simultaneously. There’s also the method of expressing reachability probabilities as a least fixed point, solved using the power method. To compute precisely, long run behavior, by computing the solutions to the linear system, you can find out whether there is a limit, whether it depends on an initial distribution or state, and other properties of the system in the long run. I can see its usefulness in understanding a model more precisely.

To do all of this, there is a software that I’m learning to work with, called PRISM. It’s a model checker software that you have to code in order to describe the states of the system as well as the behavior of its evolution. But before I even get into the workings of PRISM, my job this coming week is to dive into the habit of modeling phenomena and being able to formulate them precisely. Also, to come up with a few properties I want to check regarding the models. As I continue doing my research, I’ll keep track of my progress here, so stay tuned!