Mobile Calculi based on Domains

Open Nets Contexts and Their Properties

R. {De Nicola} and M. Loreti


KLAIM (A Kernel Language for Agents an Mobility) is a simple formalism that can be used to model and program mobile systems; it allows programmers to concentrate on the distributed structure of programs while ignoring their precise physical allocations. For establishing properties of KLAIM Nets, a logic based on HML was defined. This logic permits specifying properties related to resource allocation, security and behaviours. A weakness of the approach is that, in order to use KLAIM and its associated logic to establish nets properties one needs to have a full implementation of the system under consideration. This is a very strong assumption when dealing with wide area networks, because very often, only a fragment of the system is known and a limited knowledge of the overall context is available. In the paper, after recalling KLAIM and its logic, we shall present a framework for specifying contexts for KLAIM. Then, by relying on a notion of agreement, we shall set up a framework ensuring that, whenever an abstract specification is partially implemented as a concrete net (guaranteeing agreement with specifications) all formulae satisfied by the more abstract description are satisfied also by the refined one.

  author = \{R. {De Nicola} and M. Loreti},
  title = \{Open Nets Contexts and Their Properties},
  year = \{2004}, 
  note = \{submitted}, 
  url = \{}

About this site. Last modified: Tue Jul 17 07:51:03 CEST 2018