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 P expressed in pairwise normal form such that P is strongly bisimilar to P. Our result is constructive: we give an algorithm for producing P, given P.