Model checking is a way to see if a design meets requirements. It starts with a model that abstracts how events affect a system. Then, the designers formulate a required behavior, for example, that something will never happen. The checker then searches for sequences of events that do not meet the requirement. There are half-a-dozen alternate ways of doing this, and each has its own set of tools. All are based on formal logic and mathematics. One problem is that the number of sequences grows very quickly, so each toolset has ways of reducing it.

This paper gives a detailed description of how a known state-space reduction technique has been applied in the ProB toolset [1] for checking Event-B models. Event-B uses the notations from the B method to describe events. Each has an enabling condition and an action. The paper shows how to compute if two events are dependent or independent. Then, it shows how to calculate what are called “ample” sets of enabled events that can happen first without loss of generality. The paper gives an explanation that is sufficient for people who are familiar with ample sets. The original publication [2] provides a detailed exposition.

This paper’s main contribution is to use the toolset’s existing constraint solver to discover dependencies. The paper presents algorithms and results of timing tests. I found these disappointing because most of the test cases don’t have many independent events.