TY - JOUR

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

AU - Attie, Paul C.

N1 - Publisher Copyright:
© 2015 Elsevier B.V.
Copyright:
Copyright 2016 Elsevier B.V., All rights reserved.

PY - 2016/3/14

Y1 - 2016/3/14

N2 - 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.

AB - 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.

KW - Atomic registers

KW - Expressive completeness

KW - Finite-state concurrent programs

KW - State-explosion

UR - http://www.scopus.com/inward/record.url?scp=84957936177&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84957936177&partnerID=8YFLogxK

U2 - 10.1016/j.tcs.2015.11.032

DO - 10.1016/j.tcs.2015.11.032

M3 - Article

AN - SCOPUS:84957936177

VL - 619

SP - 1

EP - 31

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

ER -