Process Analysis Toolkit

PAT is a self-contained framework for the support of composing, simulating and reasoning of concurrent, real-time systems and other possible domains.

It comes with user friendly interfaces, featured model editor and animated simulator. Most importantly, PAT implements various model checking techniques catering for different properties such as deadlock-freeness, divergence-freeness, reachability and other.