Abstract.
The calculus of Mobile Ambients has been introduced for expressing mobility
and mobile computation. In this paper we present a probabilistic version of
Mobile Ambients by augmenting the syntax of the original Ambient Calculus
with a (guarded) probabilistic choice operator. To allow for the
representation of both the probabilistic behaviour introduced through the
new probabilistic choice operator and the nondeterminism present in the
original Ambient Calculus we use probabilistic automata as the underpinning
semantic model. We also introduce the Probabilistic Ambient Logic for
specifying properties of Probabilistic Mobile Ambients, which extends the
Ambient Logic, a logic for Mobile Ambients, that contains a novel treatment
of both locations and hidden names. In addition, to show the utility of our
approach we present an example of a virus infecting a network.
|