非状态并发程序可以两两表示
Finite-state concurrent programs can be expressed pairwise
摘要：
我们提出了一个\emph{pairwise normal form}有限状态共享内存并发程序：所有的变量之间的共享正好是两个进程，和警卫的过渡是这个成对共享状态的条件的合取。这种表示已被用来有效地（在多项式时间）综合和模型检查并发程序的正确性。我们的主要结果是任何有限状态并发程序都可以转化为成对范式。具体地，如果$Q$是任意有限状态共享存储器并发程序，则存在以成对范式表示的有限状态共享存储器并发程序$P$，使得$P$与$Q$强双相似。我们的结果是建设性的：我们给出了一个算法产生$P$，给定$Q$。
英文摘要：
We present a \emph{pairwise normal form} for finite-state shared memory concurrent programs: all variables are shared between exactly two processes, and the guards on transitions are conjunctions of conditions over this pairwise shared state. This representation has been used to efficiently (in polynomial time) synthesize and model-check correctness properties of concurrent programs. Our main result is that any finite state concurrent program can be transformed into pairwise normal form. Specifically, if $Q$ is an arbitrary 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 $Q$. Our result is constructive: we give an algorithm for producing $P$, given $Q$.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
