February 20, 2024

Planning vs Model Checking

Comparing two software technologies you've probably never heard of

New blogpost! Planner programming blows my mind, Patreon here. Next essay out should be the graph project.

The post is about Picat and more specifically, planner programming. Planning very roughly is:

1. You provide a start state, a set of goals, and a set of state transitions (actions),
2. The planner uses the actions to generate a state space,
3. The planner reports a sequence of actions that reaches a goal, if any.

A lot of formal methods stuff like TLA+ is verified with model checking, which very roughly is:

1. You provide initial states, a set of properties, and a set of state transitions
2. The model checker uses the transitions to generate a state space,
3. The checker reports a sequence of actions that violate a property, if any.

These look extremely similar, and in fact they are mathematically the same thing. Any model checker can find a plan that reaches goal P by writing !P as a property to check. Then the "violation" returns a trace that ends with P. That's how you can use TLA+ to solve the diehard puzzle.

Similarly, any planner can be turned into a model checker that by making the goal !P, and then failure to reach that goal means P is a valid property. And in fact that's how the Z3 theorem prover proves properties: to determine if P is true, you check that !P has no satisfying solutions.¹ I believe Alloy does the same thing, running as both a "model finder" and a "model checker".

Planning and model checking are "isomorphic" to each other, a tool for one is identically a tool for the other. Any differences between the two are in the engineering of planners vs model checkers. But these differences are quite significant, because the approaches come from completely different fields. Planning comes from robotics and AI, and (to my understanding) is predominantly used in video games. Model checking comes from formal methods. These fields are making the same class of tools but for very different reasons, and this leads to a lot of practical differences in what these tools do.

Planning

(I have limited experience with planning and am basing most of this off this page, PDDL, and some github research.)

Planning is mostly done for finding a plan to be immediately executed by a robot or game AI. There's three complications to planning problems not seen in model checking:

1. It's not enough to find any plan, you want to find the cheapest plan. So planners can assign a "cost" to each action and then find plans with minimum costs. Most model checkers, if they do minimization, only minimize the number of steps in a trace.
2. The planning may need to be run for many different agents in realtime. There's more emphasis on being able to tune the planner's performance: swap in a different search strategy, fine tune cost heuristics, etc.
3. Planning can be "dynamic", in that world-state can change while an agent is undergoing a plan, in which case it needs to make a new plan. I don't know how this is generally handled.

Model checking

Model checking is mostly done for finding a bug in software to be fixed. If a model check finds a bug, someone has to read the error trace and then try to make changes to the software to fix it. So you see more emphasis on making legible traces, such as by generating visualizations.

There's a lot of different kinds of bugs in a system, so model checkers offer a lot of flexibility in expressing properties. Most of the planners I found look for end states;² these correspond to "invariants" in a model checker, properties that hold true at all states. By contrast, most model checkers also accept a wide range of temporal operators, giving properties over sequences of states. Examples are:

• The counter can only increase, never decrease.
• The boot sequence cannot start until the switch is flipped, and once it starts, it must complete within five seconds.
• The database is eventually consistent.
• Every thread always gets a chance to make progress on its task.

Many model checkers also have interactive or simulation modes, to help programmers better understand the systems without them having to check for specific properties.

Two thoughts on this

Commands vs Queries

Best explained here. Model checking is primarily query-centric (you use it to gather information about the system), planning is primarily command-centric (you use it to set off a bunch of state changes).³ This influences how the tools are engineered: simulation makes sense for gathering information but not effecting change; effecting change means running lots of plans at once, etc.

Engineering matters

Two things can have the same underlying theory but be engineered so differently that one is a poor substitute for the other. Not just in features but performance characteristics, debuggability, etc. Neither is making the wrong choice, both are just adapted to a context. This is a cause of software mimicry.

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.