Ludwig-Maximilians-Universität München, Institut für Informatik,Beyond a global infrastructure for the exchange of primarily static documents, the internet can be used as a platform for (widely) distributed applications. This development is reinforced by the increasing availability of mobile devices that aim to provide complete working environments for use across administrative and spatial boundaries. However, these new applications demand high levels of security, fault-tolerance, and availability of computational and transmission bandwidth. This project aims at contributions to developing formal semantics and logics that are adequate for the description of mobile systems.
Historically, the first formalism for the description of aspects of mobility was Milner's pi calculus that extends the process algebra CCS by primitives for the generation and transmission of names. Mobility of code can, however, not be directly modelled in the pi calculus. The best-known calculus that allows to model this kind of mobility is the Ambient Calculus defined by Cardelli and Gordon, which also serves as the starting point of our research.
In this project we want to concentrate on appropriate semantic models underlying formalisms and techniques for the specification and analysis of mobile systems, extending standard models of transition systems. The spatial distribution will be modelled by endowing states with a tree (or more generally, graph) structure. Coalgebraic description techniques provide an attractive framework for specifying transition systems, they also allow to characterize bisimulation relations in a general, categorial framework as well as to systematically define modal logics that will be expressively complete. This generic approach will be instantiated for the application to mobile systems and will be suitably extended (e.g., by fixed point operators).
Moreover, we will define a logic containing both spatial and temporal modalities suitable to specify mobile systems and prove properties abouth them. The semantics of this logic will be defined in terms of our model of generalized transition systems. We will study meta properties such as axiomatizability, decidability, and expressiveness (of the propositional fragment) to assess the power of the formalism.
Finally we want to study refinement of mobile systems. The refinement notion found in the temporal logic TLA will serve as a first starting point. It will be interesting to consider new issues pertaining to the spatial structure of mobile systems such as the specialization of administrative domains. The developed logic should support conducting refinement proofs.
Project partner: Dr. Bernhard Reus, University of Sussex, Brighton, UK
Contact: Dr. Stephan Merz, Dr. Dirk Pattinson, Júlia Zappe.
Projekte
Lehrstuhl
Institut
Universität