hide
Free keywords:
-
Abstract:
We define a finite-control fragment of the ambient calculus, a
formalism for 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
$\pi$-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 ambients to deal with
recursively-defined, possibly nonterminating, processes. Moreover, we show
that the problem is PSPACE-complete, like other fragments considered in the
literature. Finite-control versions of other process calculi are obtained via
various 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.
