A Modal Logic for Klaim

  • Rocco De Nicola
  • Michele Loreti
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1816)


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, and on allocation environments that associate logical localities to physical sites. 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 to describe the effect of actions over the different sites. The logic is equipped with a consistent and complete proof system that enables one to prove properties of mobile systems.


Mobile Code Languages Temporal Logics of Programs Coordination Models 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Nicholas Carriero and David Gelernter. Linda in Context. Communications of the ACM, 32(10):444–458, October 1989. Technical Correspondence.CrossRefGoogle Scholar
  2. 2.
    Rance Cleaveland. Tableau-based model checking in the propositional μ-calculus. Acta Informatica, 27(8):725–747, September 1990.zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    D. Gelernter. Generative communication in linda. ACM Transactions on Programming Languages and Systems, 7(1):80–112, 1985.zbMATHCrossRefGoogle Scholar
  4. 4.
    D. Gelernter. Multiple tuple spaces in linda. In J. Hartmanis G. Goos, editor, Proceedings, PARLE’ 89, volume 365 of LNCS, pages 20–27, 1989.Google Scholar
  5. 5.
    Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137–161, January 1985.zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989. SU Fisher Research 511/24.Google Scholar
  7. 7.
    Rocco De Nicola, Gian Luigi Ferrari, and Rosario Pugliese. KLAIM: A kernel language for agents interaction and mobility. IEEE Transactions on Software Engineering, 24(5):315–330, May 1998. Special issue: Mobility and Network Aware Computing.CrossRefGoogle Scholar
  8. 8.
    Rocco De Nicola and Michele Loreti. A logic for klaim (full paper). Avaiable at

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Rocco De Nicola
    • 1
  • Michele Loreti
    • 1
  1. 1.Dipartimento di Sistemi e InformaticaUniversità di FirenzeFirenze

Personalised recommendations