Titlebook: Quantitative Evaluation of Systems; 15th International C Annabelle McIver,Andras Horvath Conference proceedings 2018 Springer Nature Switze

道学气

WITH

How Fast Is MQTT?,tions in various settings. We present a model-based performance testing approach that allows a fast simulation of specific usage scenarios in order to perform a quantitative analysis of the latency. Out of automatically generated log-data, we learn the distributions of latencies and apply statistica

IVORY

热心

On the Verification of Weighted Kripke Structures Under Uncertainty,n of weighted Kripke structures, namely (i) ., having transitions weights modelled as affine maps over a set of parameters and, (ii) ., having transition labelled by real-valued random variables as opposed to precise real valued weights..We address this problem by using ., a symbolic extension of de

EWE

Hospital Inventory Management Through Markov Decision Processes @runtime,ient care as well as on purchasing and logistics costs. We address daily drug ordering in a ward of an Italian public hospital, where patient admission/discharge and drug consumption during the sojourn are subject to uncertainty. To derive optimal control policies minimizing the overall purchasing a

无法破译

Guaranteed Error Bounds on Approximate Model Abstractions Through Reachability Analysis,hly sensitive to the specific choice of parameters. In this paper we consider this problem for nonlinear ordinary differential equations (ODEs) with polynomial derivatives. We introduce approximate differential equivalence as a more permissive variant of a recently developed exact counterpart, allow

CRATE

Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties,a wide range of applications that involve both stochastic and timed behaviours. In this work, we consider the problem of model-checking linear . properties over PTAs. In particular, we study linear dense-time properties that can be encoded by TAs with infinite acceptance criterion. First, we show th

饥荒

Incremental Verification of Parametric and Reconfigurable Markov Chains,y. This is partly because it is much harder: while there are beautiful cut-off results for non-stochastic systems that allow to focus only on small instances, there is little hope that such approaches extend to the quantitative analysis of probabilistic systems, as the probabilities depend on the si

集合

Lumping the Approximate Master Equation for Multistate Processes on Complex Networks,y of emerging phenomena such as the dynamics of an epidemic or the spreading of information on complex networks. In recent years, mean-field type approximations gained widespread attention as a tool to analyze and understand complex network dynamics. They reduce the model’s complexity by assuming th

brother