Towards a logic for performance and mobility


De Nicola, Rocco and Katoen, Joost-Pieter and Latella, Diego and Massink, Mieke (2005) Towards a logic for performance and mobility. Electronic Notes in Theoretical Computer Science (ENTCS), 153 (2). pp. 161-175. ISSN 1571-0661

[img] PDF
Restricted to UT campus only
: Request a copy
Abstract:StoKLAIM is an experimental language designed for modeling and programming distributed systems composed of mobile components where distribution awareness and dynamic system architecture configuration are key issues. StoKLAIM is a Markovian extension of the core subset of KLAIM which includes process distribution, process mobility, asynchronous communication, and site creation. In this paper, a temporal logic for StoKLAIM is proposed which addresses and integrates the issues of distribution awareness and mobility and those concerning stochastic behaviour of systems. The satisfiability relation is formally defined over labelled Markov chains. A large fragment of the proposed logic can be translated to action-based CSL for which efficient model-checkers exist. This way, such model-checkers can be used for the verification of StoKLAIM models. An example application is provided in the present paper.
Item Type:Article
Additional information:Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages (QAPL 2005), April 2-3, 2005, Edinburgh, UK
Copyright:© 2006 Elsevier
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:
Official URL:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 229289