The tests were performed on a Mac Pro quad-core 2.66 Ghz, with 16 GB of memory. By default, the timings use seconds except when a 'm' appear for minutes.
Spin was used for reference of non timed automata and Uppaal was used for timed automata.
The numbers for interleaving (only one transition for each step) and multisteps columns are in the order :
the time for the SAT solver to find a solution, the number of clauses in the formula and the number of (multi) steps of the solution, e.g. 2.4/164K/10 indicates a solving time of 2.4s for a formula with approximatively 164.000 clauses and 10 multisteps.
The symbol '-' is used when no solution has been found within 20 minutes, 'Err' when an error has occurred.

Several knights are placed on a chessboard and search a sequence of moves respecting chess rules such that in the end no two knights menace each other. This examples use a high level of parallelism because each square on the board is a process that tests if a knight is present or not. Then it tries to move it on a free square. A process is used to test the if the board is in a safe position. The classical problem of the dining philosophers: it is summarized as five philosophers (or more) sitting at a table doing one of two things: eating or thinking. While eating, they are not thinking, and while thinking, they are not eating. The five philosophers sit at a circular table with a large bowl of spaghetti in the center. A fork is placed in between each pair of adjacent philosophers, and as such, each philosopher has one fork to his left and one fork to his right. As spaghetti is difficult to serve and eat with a single fork, it is assumed that a philosopher must eat with two forks. Each philosopher can only use the forks on his immediate left and immediate right. The philosophers never speak to each other, which creates a dangerous possibility of deadlock when every philosopher holds a left fork and waits perpetually for a right fork (or vice versa). Source : Wikipedia Several NOT gates are connected one to the other. Each gate has a random delay to propagate its input signal to its output. Initially each value is equal to zero. We want to know if the circuit can stabilize, i.e. if there exists a time t where input values and output values are coherent (and thus will no longer change). Of course, the circuit can stabilize only if there is an even number of gates. It turns out that the desired state is reachable with one (synchronous) multi step. We consider the following simplistic broadcast protocol: nodes arranged in a (non complete) binary tree can only send a signal to their children after receiving a signal from their parents. When a leaf receives a signal, it sends back an acknowledgement. When an interior node receives acknowledgements from its two children, it sends one to its own parent, and so on. To resume, a signal starts from the root, is asynchronously propagated to the leaves and back to the root. A random delay for each transmission between a parent and its children is added. The model checker is asked to find a completed broadcast within a tight interval of time.