Mobile Calculi based on Domains


A Modal Logic for Mobile Agents

R. {De Nicola} and M. Loreti

Abstract

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.

@Article\{de-nicola.loreti:modal-logic-mobile-agents,
  author = \{R. {De Nicola} and M. Loreti},
  title = \{A Modal Logic for Mobile Agents},
  journal = \{ACM Transactions on Computational Logic},
  year = \{To appear}, 
  url = \{http://mikado.di.fc.ul.pt/repository/de-nicola.loreti_modal-logic-mobile-agents.pdf}
}


About this site. Last modified: Sat Apr 20 12:48:33 CEST 2024