Benchmarks of Timed Automata

This page is dedicated to contain our benchmarks of timed automata. There are 5 benchmarks selected to compare the verification time (in second) of our tool with the one of Rabbit and Uppaal: Fischer mutual exclusion protocol, Lynch-Shavit protocol, CSMACD protocol, Critical Region, and Token Ring FDDI Protocol. (Download all of the models here). All of the experiments are performed on a PC with Intel Core i7-2600 CPU at 3.4GHz and 2GB RAM with a time limit of 3 CPU hours. Uppaal is run under default option. Since we can allocate Rabbit maximum 800MB memory, both PAT and Rabbit are run with a memory limit of 800MB. An entry "to" in the table means that the time limit is reached, and an entry "oom" means that the program runs out of memory.

In the first experiment, for each benchmark we exponentially increase the upper bound of the timing constraints while keeping the number of processes 4. Because Uppaal does not depend much on the maximal clock constants, it is not used in our first experiment. Table 1 summarizes the experiment results of PAT and Rabbit.

PAT Rabbit
Fischer 64 1.1 1.7
Fischer 128 3 7
Fischer 256 19 53
Fischer 512 134 1290
Fischer 1024 1146 oom
Lynch 16 0.7 6
Lynch 32 3 30
Lynch 64 16 284
Lynch 128 126 to
Lynch 256 1028 oom
CSMACD 202 1 1
CSMACD 404 4 23
CSMACD 808 29 226
CSMACD 1616 206 1631
CSMACD 3232 1780 to
Critical 20 44
Critical 40 1318
Critical 80 46124
Critical 160 2061210
Critical 320 1024to
FDDI 8 0.1 1
FDDI 16 0.6 1
FDDI 32 8 2
FDDI 64 135 16
FDDI 128 4461 279
Table 1: Compare PAT, Rabbit in handling large clock constants

In the second experiment, PAT, Rabbit and Uppaal are compared in 5 benchmarks the same as ones in the first experiment. However in this experiment, we fix the maximal clock constant and increase the number of processes in each model to compare which tool can verify most processes. Specifically we fix the maximal clock constant 64 in Fischer protocol, 16 in Lynch-Shavit protocol, 404 in CSMACD protocol, 50 in Critical and 40 in FDDI protocol. Table 2 summarizes the experiment results of PAT, Rabbit, and Uppaal.

PAT Rabbit Uppaal
Fischer4 2.3 5 0.1
Fischer8 39 8994 0.7
Fischer16 268 oom oom
Fischer32 2744 oom oom
Lynch4 0.8 4 0.1
Lynch8 8 2691 1.1
Lynch16 79 oom oom
Lynch32 2107 oom oom
CSMACD8 15 810 0.3
CSMACD16 58 6674 oom
CSMACD32 398 to oom
CSMACD64 3968 to oom
Critical5 106 221 5
Critical6 391 929 479
Critical7 1231 3588 to
Critical8 4108 to to
FDDI16 7 4 0.1
FDDI24 49 12 0.7
FDDI32 231 3300 3
FDDI40 782 to 9
Table 2: Compare PAT, Rabbit and Uppaal in handle large number of processes