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

Research output: Contribution to journalArticlepeer-review

4 Scopus citations


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.

Original languageEnglish (US)
Pages (from-to)1-31
Number of pages31
JournalTheoretical Computer Science
StatePublished - Mar 14 2016
Externally publishedYes


  • Atomic registers
  • Expressive completeness
  • Finite-state concurrent programs
  • State-explosion

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Finite-state concurrent programs can be expressed in pairwise normal form'. Together they form a unique fingerprint.

Cite this