Mobile Calculi based on Domains

A Modal Logic for Mobile Agents

R. {De Nicola} and M. Loreti


KLAIM is an experimental programming language that supports a programming paradigm where both processes and data can be moved across different computing environments. The language relies on the use of explicit localities. This paper presents a temporal logic for specifying properties of Klaim programs. The logic is inspired by Hennessy-Milner Logic (HML) and the calculus, but has novel features that permit dealing with state properties and impact of actions and movements over the different sites. The logic is equipped with a complete proof system that enables one to prove properties of mobile systems.

  author = \{R. {De Nicola} and M. Loreti},
  title = \{A Modal Logic for Mobile Agents},
  journal = \{ACM Transactions on Computational Logic},
  year = \{To appear}, 
  url = \{}

About this site. Last modified: Sun Sep 24 03:37:46 CEST 2017