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

Research output: Contribution to journalArticle

4 Scopus citations

Abstract

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
Volume619
DOIs
StatePublished - Mar 14 2016
Externally publishedYes

Keywords

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint 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