共代数中的互模拟证明方法及其应用

本论文主要研究共代数中的互模拟证明方法及其应用两个方面。 代数理论已被证实在计算机科学中具有广泛的应用，其对偶概念——共代数理论是近年来兴起的一个理论，它在描述无穷状态系统方面具有明显的优势。 因此，我们在本文中以共代数作为抽象的研究模型。 因为互模拟判定中的up-to方法能够非常有效地加速判定过程，我们首先将该方法从传统的集合论中 扩展到共代数理论。作为Sangiorgi的可靠函数的扩展，我们引入了一致函数。因此， 为了证明某个二元关系中的进程对都是互模拟等价的，只要证明该关系前进到其在某个一致函数作用下得到的新关系中即可。 另外，我们给出了span-互模拟和ref-互模拟之间的等价转换关系，并且，利用该结果证明了共代数中原有的up-to方法 都能被一致函数所覆盖。 一致函数是为单个函子$F$定义的。但是，当$F$是某种类型的多项式函子时，有可能存在一些 函数，它们与$F$的某些子函子一致却不与整个$F$一致。因此，我们将一致函数进一步扩展，定义 联合一致函数，它是那些只与某些子函子一致的函数在一定条件下的组合。联合一致函数使用起来和一致函数一样，能够用来产生 新的up-to证明方法。另外，我们也相应地给出了传统并发理论中的联合一致函数概念，并且利用它给出了 弱互模拟的up-to方法。 在抽象的共代数模型中给出一般化的up-to方法之后，本文继续研究其在具体的无穷状态系统，即 BPA系统上的应用。Caucal的self-互模拟理论在 BPA系统的互模拟判定算法中起着关键作用，而它恰恰 是运用up-to方法协助互模拟判定的一个典范。 因为一个BPA系统也是一个共代数，我们在共代数理论中利用一致函数证明了该理论。 同时，本文给出了一个tableau算法，用来判定包含normed 与unnormed BPA进程的全BPA系统的互模拟等价问题。该算法非常直接且易于理解。 利用该tableau算法，我们证明了Hans H\"{u}ttel 和 Colin Stirling 为normed BPA进程设计的等式理论对于全BPA系统同样是可靠的与完备的。