×

zbMATH — the first resource for mathematics

MoMo: A modal logic for reasoning about mobility. (English) Zbl 1143.68364
de Boer, Frank S. (ed.) et al., Formal methods for components and objects. Third international symposium, FMCO 2004, Leiden, The Netherlands, November 2–5, 2004. Revised lectures. Berlin: Springer (ISBN 3-540-29131-8/pbk). Lecture Notes in Computer Science 3657, 95-119 (2005).
Summary: 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 different computing environments. The language relies on the use of explicit localities. The logic is inspired by Hennessy-Milner Logic (HML) and the \(\mu\)-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 sound and complete tableaux-based proof system.
For the entire collection see [Zbl 1084.68008].

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B44 Temporal logic
03B70 Logic in computer science
Software:
MoMo; Freshml; SLMC; KLAIM
PDF BibTeX XML Cite
Full Text: DOI