PAT (model checker)

{{Infobox software

| name = PAT

| logo =

| screenshot =

| caption =

| developer = National University of Singapore

| released = {{Start date|2008}}

| latest release version = 3.5.1

| latest release date = {{release date and age|2013|08|13}}

| latest preview version =

| latest preview date =

| programming_language = C#

| operating system = Microsoft Windows; Linux, Unix, Mac OS X with Mono

| platform = .Net 3.0

| genre = Model checking

| language = English
Chinese(Simplified)
Chinese(Traditional)
Japanese
German
Vietnamese

| license =

| website = http://pat.comp.nus.edu.sg/

}}

PAT (Process Analysis Toolkit) is a self-contained framework for composing, simulating and reasoning of concurrent, real-time systems and other possible domains. It includes user interfaces, model editor and animated simulator. PAT implements various model checking techniques catering for different properties such as freedom from deadlock and divergence, reachability, LTL properties with fairness assumptions, refinement checking and probabilistic model checking. To achieve good performance, advanced optimization techniques are implemented in PAT, e.g. partial order reduction, [https://web.archive.org/web/20110217191210/http://library.thinkquest.org/27930/symmetry.htm symmetry reduction], process counter abstraction.