Finite-state concurrent programs can be expressed succinctly in triple normal form

Research output: Contribution to journalArticle


I show that any finite-state shared-memory concurrent program P can be transformed into triple normal form: all variables are shared between exactly three processes, and the guards on actions are conjunctions of conditions over this triple-shared state. My result is constructive, since the transformation that I present is syntactic, and is easily implemented. If (1) action guards are in disjunctive normal form, or are short, i.e., of size logarithmic in the size of P, and (2) the number of shared variables is logarithmic in the size of P, then the triple normal form program has size polynomial in the size of P, and the transformation is computable in polynomial time.

Original languageEnglish (US)
Pages (from-to)8-13
Number of pages6
JournalInformation Processing Letters
StatePublished - Jul 1 2017
Externally publishedYes



  • Concurrency
  • Expressive completeness
  • Finite-state concurrent programs

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Signal Processing
  • Information Systems
  • Computer Science Applications

Cite this