Quantitative Evaluation of Systems: 14th International Conference, QEST 2017, Berlin, Germany, September 5-7, 2017, Proceedings (Lecture Notes in Computer Science Book 10503)

This book constitutes the proceedings of the 14th International Conference on Quantitative Evaluation Systems, QEST 2017, held in Berlin, Germany, in September 2017.The 20 full papers and 4 tool papers presented were carefully reviewed and selected From 58 submissions. The papers are organized in topical sections entitled: probabilistic modeling; smart energy systems over the cloud; Petri nets and performance modeling; parametric verification; machine learning and formal methods; tools. . Front Matter ....Pages I-XIII Front Matter ....Pages 1-1 Extending Parikh’s Theorem to Weighted and Probabilistic Context-Free Grammars (Vijay Bhattiprolu, Spencer Gordon, Mahesh Viswanathan)....Pages 3-19 Exploiting Non-deterministic Analysis in the Integration of Transient Solution Techniques for Markov Regenerative Processes (Marco Biagi, Laura Carnevali, Marco Paolieri, Tommaso Papini, Enrico Vicario)....Pages 20-35 alphaFactory: A Tool for Generating the Alpha Factors of General Distributions (Elvio Gilberto Amparore, Susanna Donatelli)....Pages 36-51 Front Matter ....Pages 53-53 Quantitative Model Checking for a Smart Grid Pricing (YoungMin Kwon, Eunhee Kim, Seonghwan Jeong, Arthur H. Lee)....Pages 55-71 Aggregated Markov Models of a Heterogeneous Population of Photovoltaic Panels (Andrea Peruffo, Emeline Guiu, Patrick Panciatici, Alessandro Abate)....Pages 72-87 Battery Aging, Battery Charging and the Kinetic Battery Model: A First Exploration (Marijn R. Jongerden, Boudewijn R. Haverkort)....Pages 88-103 Front Matter ....Pages 105-105 A Hybrid Multi-trajectory Simulation Algorithm for the Performance Evaluation of Stochastic Petri Nets (Armin Zimmermann, Thomas Hotz, Andrés Canabal Lavista)....Pages 107-122 A Probabilistic Small Model Theorem to Assess Confidentiality of Dispersed Cloud Storage (Marco Baldi, Ezio Bartocci, Franco Chiaraluce, Alessandro Cucchiarelli, Linda Senigagliesi, Luca Spalazzi et al.)....Pages 123-139 On the Cost of Diagnosis with Disambiguation (Loïc Hélouët, Hervé Marchand)....Pages 140-156 Multi-class Resource Sharing with Batch Arrivals and Complete Blocking (Paul Ezhilchelvan, Isi Mitrani)....Pages 157-169 Front Matter ....Pages 171-171 Reachability in Parametric Interval Markov Chains Using Constraints (Anicet Bart, Benoît Delahaye, Didier Lime, Éric Monfroy, Charlotte Truchet)....Pages 173-189 Mean-Payoff Optimization in Continuous-Time Markov Chains with Parametric Alarms (Christel Baier, Clemens Dubslaff, Ľuboš Korenčiak, Antonín Kučera, Vojtěch Řehák)....Pages 190-206 Multi-objective Robust Strategy Synthesis for Interval Markov Decision Processes (Ernst Moritz Hahn, Vahid Hashemi, Holger Hermanns, Morteza Lahijanian, Andrea Turrini)....Pages 207-223 Investigating Parametric Influence on Discrete Synchronisation Protocols Using Quantitative Model Checking (Paul Gainer, Sven Linker, Clare Dixon, Ullrich Hustadt, Michael Fisher)....Pages 224-239 Front Matter ....Pages 241-241 Statistical Abstraction for Multi-scale Spatio-Temporal Systems (Michalis Michaelides, Jane Hillston, Guido Sanguinetti)....Pages 243-258 Automated Experiment Design for Data-Efficient Verification of Parametric Markov Decision Processes (Elizabeth Polgreen, Viraj B. Wijesuriya, Sofie Haesaert, Alessandro Abate)....Pages 259-274 Data-Driven Model-Based Detection of Malicious Insiders via Physical Access Logs (Carmen Cheh, Binbin Chen, William G. Temple, William H. Sanders)....Pages 275-291 Front Matter ....Pages 293-293 Tulsa: A Tool for Transforming UML to Layered Queueing Networks for Performance Analysis of Data Intensive Applications (Chen Li, Taghreed Altamimi, Mana Hassanzadeh Zargari, Giuliano Casale, Dorina Petriu)....Pages 295-299 Modelling and Performance Evaluation with TimeNET 4.4 (Armin Zimmermann)....Pages 300-303 RODES: A Robust-Design Synthesis Tool for Probabilistic Systems (Radu Calinescu, Milan Češka, Simos Gerasimou, Marta Kwiatkowska, Nicola Paoletti)....Pages 304-308 QUEST: A Tool for State-Space Quantization-Free Synthesis of Symbolic Controllers (Pushpak Jagtap, Majid Zamani)....Pages 309-313 Front Matter ....Pages 315-315 Three-Valued Spatio-Temporal Logic: A Further Analysis on Spatio-Temporal Properties of Stochastic Systems (Ludovica Luisa Vissat, Michele Loreti, Laura Nenzi, Jane Hillston, Glenn Marion)....Pages 317-332 Sequential Schemes for Frequentist Estimation of Properties in Statistical Model Checking (Cyrille Jegourel, Jun Sun, Jin Song Dong)....Pages 333-350 Multilevel Monte Carlo Method for Statistical Model Checking of Hybrid Systems (Sadegh Esmaeil Zadeh Soudjani, Rupak Majumdar, Tigran Nagapetyan)....Pages 351-367 Back Matter ....Pages 369-370 This book constitutes the proceedings of the 14th International Conference on Quantitative Evaluation Systems, QEST 2017, held in Berlin, Germany, in September 2017. The 20 full papers and 4 tool papers presented were carefully reviewed and selected From 58 submissions. The papers are organized in topical sections entitled: probabilistic modeling; smart energy systems over the cloud; Petri nets and performance modeling; parametric verification; machine learning and formal methods; tools