弱共变-逆变模拟的公理刻画

摘要

进程代数是并发理论研究的主流方向,是分析和描述并发与分布式系统的重要工具之一.模拟是进程代数中刻画精化关系的核心概念.共变-逆变模拟派生于通常的模拟关系,它区分动作的类型,直观上,表达了状态的行为数目越多但并不一定越好的事实.然而,该模拟关系忽略了可观测动作与内动作的区别.因此,给出一种弱共变-逆变模拟关系及其相应的公理刻画,并且建立了该公理系统的可靠性与基完备性,进而证明了该公理系统亦是旷完备的.