Klaim is an experimental programming language that sup-ports 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.

A Modal Logic for KLAIM / R. De Nicola; M. Loreti. - STAMPA. - (2000), pp. 339-354. [10.1007/3-540-45499-3_25]

A Modal Logic for KLAIM

DE NICOLA, ROCCO;LORETI, MICHELE
2000

Abstract

Klaim is an experimental programming language that sup-ports 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.
2000
9783540675303
Algebraic Methodology and Software Technology. 8th International Conference, AMAST 2000, Proceedings. Lecture Notes in Computer Science 1816
339
354
R. De Nicola; M. Loreti
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificatore per citare o creare un link a questa risorsa: https://hdl.handle.net/2158/2694
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? 3
social impact