Finite-control mobile ambients

Abstract

We define a finite-control fragment of the ambient calculus, a formalismfor describing distributed and mobile computations. A series of examples demonstrates the expressiveness of our fragment. In particular, we encode the choice-free, finite-control, synchronous π-calculus. We present an algorithm for model checking this fragment against the ambient logic (without composition adjunct). This is the first proposal of a model checking algorithm for ambientsto deal with recursively-defined, possibly non terminating, processes. Moreover,we show that the problem is PSPACE-complete, like other fragments consideredin the literature. Finite-control versions of other process calculi are obtained viavarious syntactic restrictions. Instead, we rely on a novel type system that bounds the number of active ambients and outputs in a process; any typable process has only a finite number of derivatives.