MoMo: A modal logic for reasoning about mobility. 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.
Keywords for this software
References in zbMATH (referenced in 4 articles , 1 standard article )
Showing results 1 to 4 of 4.
- Banks, C. J.; Stark, I.: A logic of behaviour in context (2014)
- De Nicola, Rocco; Loreti, Michele: Multiple-labelled transition systems for nominal calculi and their logics (2008)
- De Nicola, Rocco; Katoen, Joost-Pieter; Latella, Diego; Loreti, Michele; Massink, Mieke: Model checking mobile stochastic logic (2007)
- De Nicola, Rocco; Loreti, Michele: MoMo: A modal logic for reasoning about mobility (2005)