The power of prophecy: the computer science

You have seen the trick. Now find out about the computer science behind it.

To prove that our magic trick worked, we first created a mathematical model of the system. In this case the model used is very simple - it just consists of the variables, X and Y, to represent how many cards are in different places. What does it mean to say: "the trick worked"? Essentially, it just means that after the steps are done, a desired property holds of the model. Here the desired property is that the cards left in our hand match the target number predicted.

As programs are similar to self-working tricks, we can prove that a program works in the same way. We create a mathematical model of it. We then write a specification of what the model should do - the property to check. Finally, we prove that the specification does hold of the model.

In fact all our 'Prove it works' sections have been doing this for our tricks, though we have used informal reasoning rather than mathematical notation. Logic and algebra have the advantage of being more precise so we are less likely to make a mistake due to fuzzy thinking.

Our model of the system doesn't just have to describe what the program does. We can think of the system as being wider than that including other devices and physical objects like credit cards or keys. We can even model the behaviour of people. At first that sounds silly. People don't just follow rules do they? Surely they behave in all sorts of different ways, so how can we model them and why would we want to?

Well, they do behave in different ways, but as we have seen there are some kinds of behaviour that are systematic. Even if you can't say what any one person will do on any specific occasion, you can make predictions about general behaviour. You can say that some kinds of errors will be made frequently, for example. If we model the systematic behaviour then we can reason about the consequences of such highly plausible behaviour. If people will often walk away when they have achieved their goal, what is the consequence for a cashpoint design, for example? Are there any situations when that opens a security vulnerability? Would a change of design allow such likely behaviour but without any bad consequences? We can answer these questions with our models.

It turns out that we can model this kind of systematic behaviour and it can be used to make predictions about the consequences of plausible behaviour. It gives us a way to verify that there are no design flaws that lead to the kinds of systematic human error that are embodied in the model.

We don't have to do the reasoning by hand. Computer programs called model checkers can exhaustively explore all possible behaviours of the model for us. They mathematically check all possible consequences of the model when interacting with our design. A model checker can even tell us the series of steps that would lead to the problem.

Model-checked psychology

Essentially what we are doing with our model of behaviour is modelling the results of cognitive psychology experiments. We can use the models created to explore our understanding of those experiments. To add the result of a new experiment to a model we first work out a rule that encapsulates the result. We then write it in a way so it can be added to the model. We can then do simulations with it - essentially running experiments on the model instead of on people (much quicker and safer!)

We can do better than that though. We can use a model checker to check all the consequences of our rule and how it interacts with all the other rules in the model. That may show that the rule gives unexpected behaviours we did not see in reality. We can then refine the rule to be more accurate if we know those behaviours aren't possible. Alternatively, we can plan new experiments to explore whether the behaviour ever could happen.

Messy reality

In psychology experiments it is important to control everything so that there is only one issue being explored at a time. The aim is to find out what the effect of changing that one thing is. In human-computer interaction studies we need to explore what happens when messy reality sticks its nose in, and that is more complicated. We need to understand what happens when lots of things are changing and what the consequences of their interactions are. Model checking can help do that. Mathematical modelling gives a new way of studying complex cognitive psychology. Mathematical reasoning and empirical experiments work together to give greater understanding of more complex situations.