Finite-state concurrent programs can be expressed in pairwise normal form

We show that any finite-state shared-memory concurrent program can be transformed into pairwise normal form: all variables are shared between exactly two processes, and the guards on transitions are conjunctions of conditions over this pairwise shared state. Specifically, if P   is a finite-state shared-memory concurrent program, then there exists a finite-state shared-memory concurrent program PP expressed in pairwise normal form such that PP is strongly bisimilar to P  . Our result is constructive: we give an algorithm for producing PP, given P.