Predicate mu-Calculus for Mobile Ambients

Ambient logics have been proposed to describe properties for mobile agents which may evolve over time as well as space. This paper takes a predicate-based approach to extending an ambient logic with recursion, yielding a predicate mu-calculus in which fixpoint formulas are formed using predicate variables. An algorithm is developed for model checking finite-control mobile ambients against formulas of the logic, providing the first decidability result for model checking a spatial logic with recursion.