摘要
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.
基金
国家自然科学基金，中国科学院资助项目
