Energy-Utility Analysis of Probabilistic Systems with Exogenous Coordination

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in Buch/Sammelband/GutachtenBeigetragen

Abstract

We present an extension of the popular probabilistic model checker PRISM with multi-actions that enables the modeling of complex coordination between stochastic components in an exogenous manner. This is supported by tooling that allows the use of the exogenous coordination language REO for specifying the coordination glue code. The tool provides an automatic compilation feature for translating a REO network of channels into PRISM’s guarded command language. Additionally, the tool supports the translation of reward monitoring components that can be attached to the REO network to assign rewards or cost to activity within the coordination network. The semantics of the translated model is then based on weighted Markov decision processes that yield the basis, e.g., for a quantitative analysis using PRISM. Feasibility of the approach is shown by a quantitative analysis of an energy-aware network system example modeled with a role-based modeling approach in REO.

Details

OriginalspracheEnglisch
TitelIt's All About Coordination
Redakteure/-innenFrank de Boer, Marcello Bonsangue, Jan Rutten
Herausgeber (Verlag)Springer, Berlin [u. a.]
Seiten38–56
ISBN (Print)978-3-319-90088-9
PublikationsstatusVeröffentlicht - 2018
Peer-Review-StatusNein

Publikationsreihe

ReiheLecture Notes in Computer Science, Volume 10865
ISSN0302-9743

Externe IDs

ORCID /0000-0002-5321-9343/work/142236677
Scopus 85047819619
ORCID /0000-0003-1724-2586/work/165453582

Schlagworte

Schlagwörter

  • Energy-Utility Analysis of Probabilistic Systems with Exogenous Coordination

Bibliotheksschlagworte