并发计算的元模型 Ⅳ.公理化

Meta Model of Concurrent Computation Ⅳ. Axiomatization

在 chi进程间互模拟格的基础上 ,利用 L-互模拟的开刻划 ,给出所有 4个 L-互模拟等价诱导的同余关系的完全公理化系统 .4个 L-互模拟等价中最小的同余关系的公理系统 ,由强互模拟等价的公理系统与 3条 tau规则构成 .在此基础上 ,分别加入一条输出规则和 /或其对偶形式 ,即得其他

This is the fourth of a series of papers on concurrent computation models. Based on the bisimulation lattice discussed in the previous paper, it gave complete equational axiomatization of the largest congruence contained in each of the four L bisimilarities. This is done by exploiting the coincidence of L bisimilarities and their open characterization. The complete system of the bottom congruence relation consists of the laws for strong bisimilarity and the three well known tau laws. Complete systems for the other three congruence relations are obtained by extending this system with a prefix law.