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

详细信息    查看全文

• 作者：Paul C. Attie ^{paul.attie@aub.edu.lb" class="auth_mail" title="E-mail the corresponding author}
• 关键词：Finite-state concurrent programs ; Expressive completeness ; Atomic registers ; State-explosion
• 刊名：Theoretical Computer Science
• 出版年：2016
• 出版时间：14 March 2016
• 年：2016
• 卷：619
• 期：Complete
• 页码：1-31
• 全文大小：1485 K

文摘

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 class="mathmlsrc">class="formulatext stixSupport mathImg" data-mathURL="/science?_ob=MathURL&_method=retrieve&_eid=1-s2.0-S0304397515011184&_mathId=si1.gif&_user=111111111&_pii=S0304397515011184&_rdoc=1&_issn=03043975&md5=4937a53f2f551d0604328f07d9b38292" title="Click to view the MathML source">Pclass="mathContainer hidden">class="mathCode"> expressed in pairwise normal form such that class="mathmlsrc">class="formulatext stixSupport mathImg" data-mathURL="/science?_ob=MathURL&_method=retrieve&_eid=1-s2.0-S0304397515011184&_mathId=si1.gif&_user=111111111&_pii=S0304397515011184&_rdoc=1&_issn=03043975&md5=4937a53f2f551d0604328f07d9b38292" title="Click to view the MathML source">Pclass="mathContainer hidden">class="mathCode"> is strongly bisimilar to P  . Our result is constructive: we give an algorithm for producing class="mathmlsrc">class="formulatext stixSupport mathImg" data-mathURL="/science?_ob=MathURL&_method=retrieve&_eid=1-s2.0-S0304397515011184&_mathId=si1.gif&_user=111111111&_pii=S0304397515011184&_rdoc=1&_issn=03043975&md5=4937a53f2f551d0604328f07d9b38292" title="Click to view the MathML source">Pclass="mathContainer hidden">class="mathCode">, given P.