MoMo: A Modal Logic for Reasoning About Mobility

Abstract. A temporal logic is proposed as a tool for specifying properties of Klaim programs. Klaim is an experimental programming language that supports a programming paradigm where both processes and data can be moved across dierent computing environments. The language relies on the use of explicit localities. 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 dierent sites. The logic is equipped with a sound and complete tableaux based proof system.

• Type: Conference
• Year: 2004
• Where: FMCO
• Authors: Rocco De Nicola, Michele Loreti
• Keywords: Dierent Computing Environments, FMCO 2004, Logic, Temporal Logic