公理化扁平迭代
摘要：基于原始二进制Kleene星操作P*Q，扁平迭代是一种变体，通过限制第一个参数为原子动作的和来获得。它推广了前缀迭代，其中第一个参数是单个动作。提供了对带有扁平迭代的基本CCS的五种关于双模拟同余的完备有限等式公理化，即强同余，分支同余，eta同余，延迟同余和弱同余。这样的公理化已经知道适用于前缀迭代，并且已知对于一般迭代不存在。与前缀迭代相比，扁平迭代的使用具有两个主要优点：1.当前的公理化适用于完整的CCS，而前缀迭代方法不允许异步并行组合运算符的消除定理。2.扁平迭代的更大表达能力使得完备性证明更加简短。 在前缀迭代设置中，获得eta同余，延迟同余和弱同余的完备性定理最方便的方式是通过将其归约到分支同余的完备性定理。对于弱同余而言，这比找到的唯一直接证明要简单得多。另一方面，在扁平迭代设置中，延迟和弱（但不是eta）同余的完备性定理同样可以通过将其归约到强同余的定理来获得，而不需要将分支同余作为中间步骤。此外，前缀迭代的完备性结果可以从扁平迭代的结果中检索出来，从而在前缀迭代设置中获得用于证明延迟和弱同余的完备性的第二个间接方法。
作者：R. J. van Glabbeek (Stanford)
论文ID：cs/9810008
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23