移动进程的空间逻辑

被引：4

作者：

林惠民

机构：

[1] 中国科学院软件研究所计算机科学重点实验室北京

来源：

中国科学E辑:技术科学 | 2004年 / 02期

关键词：

模态逻辑; 谓词μ-演算; 模型检测; 移动进程; 异步π-演算;

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

提出了一个用于描述异步π-演算中移动进程的时态和空间性质的模态逻辑.该逻辑具有基于谓词变量的递归构造.建立了这一逻辑的语义理论,并证明了语义的单调性,从而保证了不动点的存在.还设计了一个算法来自动地检测移动进程是否具有用该逻辑公式所描述的性质,并证明了该算法的正确性.

引用

页码：139 / 150

页数：12

共 4 条

[1] Mobile ambients [J].

Cardelli, L ;

Gordon, AD .

THEORETICAL COMPUTER SCIENCE, 2000, 240 (01) :177-213

[2] Model checking mobile processes [J].

Dam, M .

INFORMATION AND COMPUTATION, 1996, 129 (01) :35-51

[3]

Aspatial logic for concurrency(Part I) .2 Caires L,Cardelli L. Proceedings of the4th International Conference on TheoreticalAspects of Computer Science(TACS2001) . 2001

[4]

Logical properties of Name Restriction .2 Cardelli L,Gordon A. Proc of the 5th International Conference on Typed Lambda Calculus and Application . 2001

← 1 →