TA module in PAT is designed to verify systems which can be modeled as
networks of timed automata extended with shared variables, structured data types, user defined functions, and channel synchronization.
The following demonstrates the experimental results on embedded examples
in TA module and UPPAAL as well as the explanations of experiment
results.

We run experiments on four models, namely, Fischer protocol, railway
control systems, FDDI protocol and CSMACD protocol to verify properties
such as deadlock-freeness, liveness, reachability and so on. The
following table summarizes the verification results. Here, ‘Proc’ means
the number of interleaving processesand ‘-‘ means out of memory or more
than 2 hours. We also do the comparison work with UPPAAL, and here ‘UPPAAL-r’ means a recvised version of the original models in UPPAAL to make them consisten with the models in PAT, ‘State-s’ means the bumber of stored states,
‘State-e’ means the number of explored states. The environment of experiments ruuning on UPPALL 4.1.2 is as follows:

1. Use convex-hull approximation
2. Hash table size 16M
3. Automatic extrapolation operator
4. Depth First Search
5. Conservative space consumption
6. Enable sweepline method
7. Enable peephole optimiser
8. Enable symmetry reduction



From the above table, we can see that PAT TA module can verify a rich set of priorities with reasonable time. In addition, some abservations are here:
firstly, we can see that the number of states and
running time increase rapidly with increasing the number of processes,
e.g., 8 processes in Fischer model vs. 9 processes. Secondly, PAT is
efficient and can handle million states in less than one hour. Thirdly,
in some case, PAT is slower than UPPAAL. The main reason of UPPAAL outperforming
PAT is that UPPAAL has benefied from many dedicated optimization techniques such
as extrapolation, while PAT has none yet. The experiment data is available here.