Predicate μ-Calculus for Mobile Ambients  

作　　者：Hui-MinLin 

机构地区：[1]LaboratoryforComputerScience,InstituteofSoftware,ChineseAcademyofSciences,Beijing100080,P.R.China

出　　处：《Journal of Computer Science & Technology》2005年第1期95-104,共10页计算机科学技术学报（英文版）

基　　金：国家自然科学基金，中国科学院资助项目

摘　　要：Ambient logics have been proposed to describe properties for mobile agentswhich may evolve over time as well as space. This paper takes a predicate-based approach toextending an ambient logic with recursion, yielding a predicate μ-calculus in which fixpointformulas are formed using predicate variables. An algorithm is developed for model checkingfinite-control mobile ambients against formulas of the logic, providing the first decidabilityresult for model checking a spatial logic with recursion.Ambient logics have been proposed to describe properties for mobile agentswhich may evolve over time as well as space. This paper takes a predicate-based approach toextending an ambient logic with recursion, yielding a predicate μ-calculus in which fixpointformulas are formed using predicate variables. An algorithm is developed for model checkingfinite-control mobile ambients against formulas of the logic, providing the first decidabilityresult for model checking a spatial logic with recursion.

关 键 词：model checking mobile ambients spatial logic MU-CALCULUS fixpoints 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]