|Table of Contents|

Spatial Logic With Behavioral Observations for Ambient Calculus(PDF)

南京师范大学学报（工程技术版）[ISSN:1006-6977/CN:61-1281/TN]

Issue:
2011年04期
Page:
70-76
Research Field:
Publishing date:

Info

Title:
Spatial Logic With Behavioral Observations for Ambient Calculus
Author(s):
Chen Jiang; Lin Rongde
Computer Network and Information Center,Huaqiao University,Quanzhou 362021,China
Keywords:
ambient calculus; ambient based logic; spatial and behavioral observations; model checking
PACS:
TP301
DOI:
-
Abstract:
A decidable ambient based spatial logic，named Applied Ambient Logic is proposed，which consists of spatial modal connectives and behavioral modal connectives． In traditional ambient logic，the composition adjunct is very expressive， which makes it possible to observe behavioral properties of processes． However，it is proved that model-checking of logics with composition adjunct is not decidable． In Applied Ambient Logic，both spatial modal connectives and behavioral modal connectives are added which can specify spatial and behavioral properties of processes directly，and fixpoint modals are also added for properties of recursive processes． A concept of property sets is adopted to describe the features of denotational semantics for logic formulas，and soundness between property-set and denotational semantics is proved． Finally，examples of Applied-Ambient Logic formulas are given which are applied to describe spatial-temporal behavioral properties of a resource transformation system model．

References:

［1］Cardelli L，Gordon A D． Anytime，anywhere: Modal logics for mobile ambients［C］/ / POLP 2000． Virginia Gold: ACM Press， 2000: 365-377．
［2］Cardelli L，Gordon A D． Mobile ambients［J］． Foundations of Software Science and Computation Structures( LNCS) ，1998， 1378: 140-155．
［3］Hirschkoff D，Lozes ，Sangiorgi D． On the expressiveness of the ambient logic［J］． Logical Methods in Computer Science， 2006，2 ( 2) : 1-35．
［4］Sangiorgi D． Extensionality and intensionality of the ambient logics［J］． ACM SIGPLAN Notices，2001， 36( 3) : 4-13．
［5］Charatonik W． The complexity of model checking mobile ambients［C］/ / Proceedings of the 4th International Conference on Foundations of Software Science and Computation Structures ( FoSSaCS 2001) ，LNCS 2030． Berlin: Springer-Verlag，2001: 152-167．
［6］Charatonik W，Talbot J M． The decidability of model checking mobile ambients［C］/ / Proceedings of the 15th Annual Conference of the European Association for Computer Science Logic． Berlin: Springer，2001: 339-354．
［7］颜锋，陈韬略，韩婷婷，等． 空间逻辑的一个定义框架及其可判定性［J］． 计算机科学，2006， 33( 6) : 7-10． Yan Feng，Chen Taolue，Han Tingting，et al． A definition framework of spatial logic and decedability［J］． Computer Science， 2006， 33( 6) : 7-10． ( in Chinese)
［8］Fu Y． Fair ambients［J］． Acta Informatica，2007，43( 8) : 535-594．
［9］Charatonik W，Gordon A D，Talbot J M． Finite-control mobile ambients［C］/ / 11th European Symposium on Programming ( ESOP 2002) ，LNCS2305． Berlin: Springer，2002: 295-313．
［10］林荣德． 移动界程演算及模型检测应用的关键问题研究［D］． 广州: 华南理工大学计算机科学与工程学院，2010． Lin Rongde． Research on key issues of mobile ambients and model checking applications［D］． Guangzhou: College of Computer Science and Engineering，South China University of Technology，2010． ( in Chinese)
［11］Caires L． Behavioral and spatial observations in a logic for the π-calculus［J］． Foundations of Software Science and Computation Structures( LNCS) ，2004，2987: 72-89．
［12］Lin H． A predicate spatial logic for mobile processes［J］． Science in China Serise F: Information Sciences，2004，47( 3) : 394-408．
［13］Lin H． A predicate mu-calculus for mobile ambients［J］． Journal of Computer Science and Technology，2005，20( 2) : 95- 104．

Memo

Memo:
-
Last Update: 2013-03-21