Open nets, contexts and their properties

Rocco De Nicola and Michele Loreti 
Dipartimento di Sistemi e Informatica, Universita' di Firenze 


KLAIM (A Kernel Language for Agents Interaction 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 dened. This logic permits specifying properties related to resource allocation, security and behaviours. However, 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 specication is partially instantiated (implemented) as a concrete net while guaranteeing agreement between specication and implementation, all formulae satised by the more abstract description are satised also by the rened one.