复制受限的环境演算中模态逻辑的内涵性

Intensionality of Modal Logic for Ambient Calculus with Restricted Replication

环境演算(MA)的模态逻辑AL进行了研究.在考虑了复制操作和限制操作的情况下,提出了逻辑等价的协归纳操作描述,并利用协归纳关系与进程结构同余关系进行比较,证明了若对MA加上约束条件得到子集MAsynIF,此时逻辑等价(=L)与结构同余关系是等价的,即AL在MAsynIF中是内涵的.同时发现由于复制操作的存在,AL的内涵性受到了影响,使得AL的区分能力被削弱,但通过对复制公式的构造验证了AL的表达能力.

The Ambient Logic(AL) that has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients(MA) has been researched. In details, in MA with replication operator and restrication operator, we gived the coinductive characterisations of the logic equivalence(=_L), and compared =_L with the structural congruence(≡). As a result, when in , subset of MA, obtained by imposing constraints on MA, AL is intensional because =L is equivalent with ≡. Due to the presence of replication operator, the intensionality of AL has been influenced and its separability has been weaken, but according to the construction of characteristic formulas the expressiveness of AL has been proved.