有限状态并发程序可以成对表示
摘要：有限状态共享内存并发程序的两两正常形式：所有变量在两个进程之间共享，转换的保卫条件是对这个两两共享状态的条件的合取。这个表示已经被用来高效（多项式时间内）合成和模型检查并发程序的正确性属性。我们的主要结果是，任何有限状态并发程序都可以转换为两两正常形式。具体而言，如果$Q$是一个任意的有限状态共享内存并发程序，则存在一个表达为两两正常形式的有限状态共享内存并发程序$P$，使得$P$与$Q$在强bisimilar关系中。我们的结果是构造性的：我们给出了一个算法，给出了$Q$生成$P$。
作者：Paul C. Attie
论文ID：0801.0677
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2008-01-07