State explosion: Peterson's mutual exclusion algorithm

The following state spaces have been generated for Peterson's mutual exclusion algorihtm with a different number of processes as an example for the state space explosion when model checking parameterized systems with finite state methods. The camera viewpoint and parameters are kept the same for all three images. Note that these state spaces have been processed with path reduction, and would me much larger without.

2 processes, 30 states:

3 processes, 853 states:

4 processes, 55043 states:

Back to the gallery