Energy-Utility Analysis of Probabilistic Systems with Exogenous Coordination. Baier, C., Chrszon, P., Dubslaff, C., Klein, J., & Klüppelholz, S. In It's All About Coordination, of LNCS, pages 38–56, Cham, 2018. Springer.
abstract   bibtex   
We present an extension of the popular probabilistic model checker \$}{\$\backslashtextsc \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 \$}{\$\backslashtextsc \Reo\\$}{\$for specifying the coordination glue code. The tool provides an automatic compilation feature for translating a \$}{\$\backslashtextsc \Reo\\$}{\$network of channels into \$}{\$\backslashtextsc \Prism\\$}{\$'s guarded command language. Additionally, the tool supports the translation of reward monitoring components that can be attached to the \$}{\$\backslashtextsc \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 \$}{\$\backslashtextsc \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 \$}{\$\backslashtextsc \Reo\\$}{\$.
@inproceedings{Baier2018,
	Abstract = {We present an extension of the popular probabilistic model checker {\$}{\$}{\backslash}textsc {\{}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 {\$}{\$}{\backslash}textsc {\{}Reo{\}}{\$}{\$}for specifying the coordination glue code. The tool provides an automatic compilation feature for translating a {\$}{\$}{\backslash}textsc {\{}Reo{\}}{\$}{\$}network of channels into {\$}{\$}{\backslash}textsc {\{}Prism{\}}{\$}{\$}'s guarded command language. Additionally, the tool supports the translation of reward monitoring components that can be attached to the {\$}{\$}{\backslash}textsc {\{}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 {\$}{\$}{\backslash}textsc {\{}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 {\$}{\$}{\backslash}textsc {\{}Reo{\}}{\$}{\$}.},
	Address = {Cham},
	Author = {Baier, Christel and Chrszon, Philipp and Dubslaff, Clemens and Klein, Joachim and Kl{\"u}ppelholz, Sascha},
	Booktitle = {It's All About Coordination},
	Date-Added = {2019-04-11 13:56:26 +0200},
	Date-Modified = {2019-07-05 16:52:05 +0200},
	Pages = {38--56},
	Publisher = {Springer},
	Series = {LNCS},
	Title = {Energy-Utility Analysis of Probabilistic Systems with Exogenous Coordination},
	Year = {2018}}

Downloads: 0