A predicate spatial logic for mobile processes

被引：0

作者：

Lin, HM ^{[1
]}

机构：

[1] Chinese Acad Sci, Inst Software, Comp Sci Lab, Beijing 100080, Peoples R China

来源：

SCIENCE IN CHINA SERIES F-INFORMATION SCIENCES | 2004年 / 47卷 / 03期

基金：

中国国家自然科学基金;

关键词：

modal logic; predicate mu-calculus; model checking; mobile processes; asynchronous pi-calculus;

D O I：

10.1360/02yf0385

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

A modal logic for describing temporal as well as spatial properties of mobile processes, expressed in the asynchronous pi-calculus, is presented. The logic has recursive constructs built upon predicate-variables. The semantics of the logic is established and shown to be monotonic, thus guarantees the existence of fixpoints. An algorithm is developed to automatically check if a mobile process has properties described as formulas in the logic. The correctness of the algorithm is proved.

引用

页码：394 / 408

页数：15

共 10 条

[1]

[Anonymous], LECT NOTES COMPUTER

[2]

BOUDOL G, 1992, 1702 INRIA

[3]

CAIRES L, 2002, LECT NOTES COMPUTER, V2421, P209

[4]

Cardelli L., 2000, Conference Record of POPL'00: 27th ACM SIGPLAN-SIGACT. Symposium on Principles of Programming Languages. Papers Presented at the Symposium, P365, DOI 10.1145/325694.325742

[5]

Cardelli L, 2001, LECT NOTES COMPUT SC, V2044, P46

[6] Mobile ambients [J].

Cardelli, L ;

Gordon, AD .

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

[7]

CHARATONIK W, 2001, LNCS, V2030, P152

[8]

CHARATONIK W, 2001, LNCS, V2142, P339

[9]

DAM M, 1996, MODEL CHECKING MOBIL, V129, P25

[10]

HONDA K, 1992, LECT NOTES COMPUT SC, V612, P21

← 1 →