Adversarial Nondeterminism

Damn, has it been two weeks since the last "real" newsletter? I feel like my brain is out shape. Anyway, I thought of a fun metaphor to explain model checking nondeterministic specifications. No deep lessons here, just explaining a cool concept.

Model Checking

So first off, I should define model checking. Most of you probably know this but a good 10% of you joined after the Crossover Project and haven't seen my day-to-day work.

TLA+ is a formal specification language, a notation for describing systems and their properties. Once you have written your TLA+ specification, you can use a model checker to see if any of your properties can be broken. There are many different ways to design model checkers, but the main one for TLA+, called TLC, is a brute force checker. It tests every possible system behavior. It starts from an initial state, looks for all the next states, and branches testing for each one of them.¹

When modeling, we often introduce nondeterminism to represent one of a set of things happening, but we don't know which. For example:

with msg \in {1, 2, 3} do
  queue := Append(queue, msg)
end with;

So we can append 1, or 2, or 3. Nondeterminism has many uses in modeling, like representing randomness. One of the most important is abstraction. We can use nondeterminism to handwave away implementation details we don't care about. Then we can specify things at a much higher level than the code level, making specifications both easier to write and to model check.

But what does it mean to "abstract out" details with nondeterminism? Analogy time!

The Actual Analogy

You're writing a tic-tac-toe AI. Tic-tac-toe is a solved game: there exists a simple algorithm that, when followed, guarantees you either win or tie the game. You've implemented some algorithm, which may or may not be correct, and have it run against me. If I can't beat the AI, then you've implemented the algorithm correctly, otherwise it's back to coding.

You start. Here's your move:

X--
---
---

I have eight possible choices. Some of them are good, some are bad. I could use my own skill in playing to make a decision, or follow a different algorithm, but that would defeat the point. We want to know "is the AI beatable", not "is the AI beatable by Hillel".

So instead I do this:

    XO- X-O
    --- ---
    --- ---

X-- X-- X--
O-- -O- --O
--- --- ---

X-- X-- X--
--- --- ---
O-- -O- --O

Then I ask you to make a move on all eight boards. Once you do that, each board has six spaces left. For each of those boards, I draw six new boards then pass all 48 boards back to you. Let's imagine that for the board where I go bottom-left, you go bottom-right. Here are the six boards I draw for that branch:

    XO- X-O
    --- ---
    O-X O-X

X-- X-- X--
O-- -O- --O
O-X O-X O-X

    X-- 
    --- 
    OOX 

If your algorithm includes "always get 3 in a row if possible", then you'd win five of those boards. But your algorithm will have to do something else on the middle board. Imagine for this one particular board it plays suboptimally and places center-right instead of top-right. I make all of my moves:

    XO- X-O
    -OX -OX
    O-X O-X

X--        
OOX        
O-X        

    X-- 
    -OX 
    OOX 

It doesn't matter that you'll win three of those boards, or that you'll win or tie on every other board. Because there is at least one board where your AI loses, your specification has bug.

Tying it back to formal specification: me forcing you to play against every possible move is equivalent to me making a nondeterministic choice. Notice that this all works out because we only care about worst case scenarios. We want to know if it's possible for the system to break the property, not whether it's likely. This means there's no penalty for me "guessing wrong".

I'm not the first person to use adversarial games as a metaphor here. In fact, some people use them as a mathematical foundation! You see it a lot in verifying bisimulation of labelled transition systems, which is a different branch of formal specifications I haven't really touched. As I understand it, if you want to prove that two state machines are equivalent, you can represent it as an adversarial game where the attacker tries to make them diverge and the defender tries to keep them in sync. As with the nondeterminism metaphor, the attacker only needs to win once to show there's a problem. The defender has to win every time to show it's correct.

Okay, thinking I remember how this "writing" thing goes. Next week's newsletter should be back to normal.

If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.

My new book, Logic for Programmers, is now in early access! Get it here.