Quantitative Evaluation of Systems: 18th International Conference, QEST 2021, Paris, France, August 23–27, 2021, Proceedings (Lecture Notes in Computer Science)

This book constitutes the proceedings of the 18th International Conference on Quantitative Evaluation Systems, QEST 2021, held in Paris, France, in August 2021. The 21 full papers and 2 short papers presented together with 2 keynote papers were carefully reviewed and selected from 47 submissions. The papers are organized in the following topics: probabilistic model checking; quantitative models and metamodels: analysis and validation; queueing systems; learning and verification; simulation; performance evaluation; abstractions and aggregations; and stochastic models. Preface Organization Stochastic Geometry Based Performance Analysis of Wireless Networks (Abstract of Keynote) Contents Keynote Speaker Performance Evaluation: Model-Driven or Problem-Driven? 1 Introduction 2 On the Insularity of Quantitative Methods 3 Observations and Recommendations 4 Towards Digital Twins 5 Epilogue References Probabilistic Model Checking A Modest Approach to Dynamic Heuristic Search in Probabilistic Model Checking 1 Introduction 2 Theoretical Background 3 Dynamic Heuristic Search 3.1 Reachability Properties 3.2 Expected Reward Properties 3.3 Bounded Properties 4 Empirical Evaluation 5 Related Work 6 Conclusion A Proof for MinProb B Proof for MaxProb References Tweaking the Odds in Probabilistic Timed Automata 1 Introduction 2 Preliminaries 2.1 Timed Automata 2.2 Probabilistic Timed Automata 2.3 Parametric Probabilistic Timed Automata 2.4 Problem Statement 3 PPTA to pMDP Methods 3.1 Digital Clocks 3.2 Backwards Reachability 3.3 Other Methods 4 Implementation 5 Evaluation 6 Conclusion References Quantifying Software Reliability via Model-Counting 1 Introduction 2 Foundations of the Pipeline 3 Pipeline 3.1 Transformation: Make Violation Countable 3.2 Conversion into CNF 3.3 Model Counting in the Pipeline 3.4 Correctness of the Pipeline 4 Evaluation 5 Related Work 6 Conclusion A Model Counting B Correctness of the pipeline References Quantitative Models and Metamodels: Analysis and Validation Compositional Safe Approximationpg of Response Time Distributionpg of Complex Workflows 1 Introduction 2 Modeling Workflows with Structured STPNs 2.1 Stochastic Time Petri Nets (STPNs) 2.2 STPN Blocks 2.3 Structure Tree 3 Compositional Evaluation of Workflows Response Time 3.1 Regenerative Transient Analysis 3.2 Complexity Heuristics 3.3 Analysis Heuristics 3.4 Approximation Safety 4 Experimentation 4.1 Experimentation Models 4.2 Experimentation Results 5 Conclusions 6 Appendix 6.1 Formal Syntax and Semantics of STPNs 6.2 Numerical Analysis of Well-Structured Workflows 6.3 Theorem Proofs 6.4 Analysis Actions References Transient Analysis of Hierarchical Semi-Markov Process Models with Tool Support in Stateflow 1 Introduction 2 Preliminaries 2.1 Semi-Markov Process 2.2 Laplace-Stieltjes Transform 2.3 Expolynomials 3 Transient Analysis of Hierarchical Semi-Markov Processes 3.1 HSMP-models 3.2 Algorithm for Transient Analysis of HSMP-models 3.3 Discussion 4 Transient Analysis of HSMP-models with Unbounded Regeneration 4.1 Evaluation of Numerical Performance 5 Tool Support and Case Study 5.1 Tool Support 5.2 Case Study 5.3 Analysis Results 6 Related Work 7 Conclusions and Future Work A Convolution of Expolynomials B Semi-Markov Kernel of Expolynomials References Evaluating the Effectiveness of Metamodeling in Emulating Quantitative Models 1 Introduction 2 Test Cases 3 Approach 3.1 Stacking Review and Variants 4 Evaluation of Accuracy and Speed 4.1 Accuracy Given Different Committee Compositions and Filters 4.2 Metamodel Accuracy: Naive vs. Best of Many vs. Stacked 4.3 Accuracy Given Different Training Sample Dataset Sizes 4.4 Speed Comparison 5 Discussion and Recommendations 6 Related Work 7 Conclusion A Appendix: Values of Input Variables for Test Case Models References Queueing Systems Network Calculus for Bounding Delays in Feedforward Networks of FIFO Queueing Systems 1 Introduction 2 Network Calculus Basics and Related Work 2.1 Network Calculus Ressource Models 2.2 Network Calculus Analyses and Tool Support 2.3 The LUDB Analysis and the DEBORAH Tool 3 Bringing the LUDB Analysis to Feedforward Networks 3.1 Arrival Bounding Procedure for FIFO 3.2 Parameter and Residual Service Computation of LUDB-FF 3.3 DEBORAH-Integration by TFA's Output from Delay 4 Numerical Evaluation 5 Conclusion A SFA-FIFO References SEH: Size Estimate Hedging for Single-Server Queues 1 Introduction 2 Related Work 3 Size Estimate Hedging: A Simple Dynamic Priority Scheduling Policy 3.1 Model 3.2 Gittins' Index Approach 3.3 Motivation 3.4 The SEH Policy 3.5 Gittins' Index Vs. SEH 4 Evaluation Methodology 4.1 Policies Under Evaluation 4.2 Performance Metrics 4.3 Simulation Parameters 5 Simulation Results 6 Conclusion and Future Work References An Approximate Bribe Queueing Model for Bid Advising in Cloud Spot Markets 1 Introduction 2 Problem Description 3 Modeling and Analysis 3.1 Definitions and Assumptions 3.2 Bribery Queueing Model 3.3 Parameter Estimation 4 Simulations 5 Related Work 6 Conclusion References Learning and Verification DSMC Evaluation Stages: Fostering Robust and Safe Behavior in Deep Reinforcement Learning 1 Introduction 2 Background 2.1 Markov Decision Processes 2.2 Deep Q-learning 2.3 Deep Statistical Model Checking 3 RL with Evaluation Stages 3.1 Initial State Partitioning and Notations 3.2 Evaluation-Based Initial Distribution (EID) 3.3 Evaluation-Based Prioritized Replay (EPR) 3.4 Deep Q-learning with Evaluation Stages 4 Case Studies 4.1 Racetrack 4.2 Experiments Setup 5 Results 5.1 Local Robustness (Deficiency (i)) 5.2 Fostering Goal Probability (Deficiency (ii)) 6 Conclusion and Future Work A Hyperparameters References Active and Sparse Methods in Smoothed Model Checking 1 Introduction 2 Related Work 3 Background 3.1 Continuous Time Markov Chains 3.2 Smoothed Model Checking 3.3 Variational Inference with Inducing Points 3.4 Active Learning 4 Active Model Checking 4.1 Streaming Setting 4.2 Query Strategies 4.3 Implementation 4.4 Results 5 Conclusions References Safe Learning for Near-Optimal Scheduling 1 Introduction 2 Preliminaries 3 Model-Based Learning 4 Monte Carlo Tree Search with Advice 5 Experimental Results A Proof of Theorem 1 B Proof of Lemma 2 C Proof of Theorem 2 References Simulation Symbolic Simulation of Railway Timetables Under Consideration of Stochastic Dependencies 1 Introduction 2 Railway Systems 2.1 Modeling Railway Infrastructure Networks 2.2 Modeling Primary Delays 2.3 Timetable Execution 3 Symbolic Simulation 3.1 Initialization 3.2 Algorithm 4 Experimental Results 5 Conclusion References Simulation of N-Dimensional Second-Order Fluid Models with Different Absorbing, Reflecting and Mixed Barriers 1 Introduction 2 Related Work 3 Simulation of First and Second Order Fluid Models with Reflecting and Absorbing Barriers 3.1 Simulation of First Order Fluid Models 3.2 Simulation of Brownian Motion for Second Order Models 3.3 Considering Boundaries 3.4 Reflecting Barrier in One Dimension 3.5 Absorbing Barrier in One Dimension 4 Extending to More Than One Dimension 4.1 Reflecting Barriers in More Than One Dimension 4.2 Absorbing Barrier in More Than One Dimension 4.3 Extensions 5 Conclusions References Performance Evaluation Queue Response Times with Server Speed Controlled by Measured Utilizations 1 Introduction 2 The Model 3 The Solution 4 An Idealized “Perfect Knowledge” (PK) Analysis 5 Effectiveness of Utilization Control and Power Saving 6 Control of Finite-Population Queues 7 Conclusions References Service Demand Distribution Estimation for Microservices Using Markovian Arrival Processes 1 Introduction 2 Preliminaries 3 Problem Formulation 4 Global Optimization Based Estimation 5 Heuristics-Based Estimation 6 Evaluation 6.1 Experimental Setup 6.2 Data Preprocessing and Clustering 6.3 Numerical Experiment Results 6.4 Analysis of Results on Measured Traces 7 Related Work 8 Conclusion References Performance Analysis of Work Stealing Strategies in Large Scale Multi-threaded Computing 1 Introduction 2 System Description and Strategies 3 Quasi-Birth-Death Markov Chain 4 Response Time Distribution 5 Numerical Experiments 6 Conclusions and Future Work A Model Validation References Abstractions and Aggregations Abstraction-Guided Truncations for Stationary Distributions of Markov Population Models 1 Introduction 2 Related Work 3 Preliminaries 3.1 Markov Population Models 3.2 Stationary Distribution 3.3 Truncation-Based Approximation of 3.4 Lyapunov Bounds 4 Method 4.1 State-Space Aggregation 4.2 Initial Aggregation 4.3 Iterative Refinement Algorithm 5 Results 5.1 Parallel Birth-Death Process 5.2 Exclusive Switch 5.3 P53 Oscillator 6 Conclusion A Detailed Results B Lyapunov Analysis of the p53 Oscillator References Reasoning About Proportional Lumpability 1 Introduction 2 Background 3 Proportional Lumpability 3.1 Alternative Characterizations of Proportional Lumpability 3.2 Comparison with Lumpability of the Embedded Markov Chain 4 Computing Proportional Lumpability 5 Conclusion A Appendix References Lumpability for Uncertain Continuous-Time Markov Chains 1 Introduction 2 Preliminaries 3 Uncertain Continuous-Time Markov Chains 3.1 Model Definition 3.2 Reachable-Set Semantics 3.3 CTMDP Semantics 3.4 Discrete-Time Approximation of the CTMDP Semantics 4 UCTMC Lumpability 4.1 UCTMC Lumpability 4.2 Logical Characterization 4.3 UCTMC Lumping Algorithm 5 Evaluation 6 Conclusion References Stochastic Models Accurate Approximate Diagnosis of (Controllable) Stochastic Systems 1 Introduction 2 Diagnosis of Markov Chains 2.1 Observable Markov Chains 2.2 Faulty Paths and Notions of Disclosure 3 Diagnosis of Controllable Systems 3.1 Controllable Observable Markov Chains 3.2 Solving AA-Diagnosability for CoMCs 4 Conclusion A AA-Disclosure Problem for oMC References Optimizing Reachability Probabilities for a Restricted Class of Stochastic Hybrid Automata via Flowpipe-Construction 1 Introduction 2 Stochastic Hybrid Automata 3 Reachability Analysis 4 Optimal Schedulers 4.1 Optimal Non-prophetic Scheduler 4.2 Optimal Prophetic Scheduler 5 Case Study 6 Conclusion Appendix A Proof of Correctness Appendix B Singular Automaton for Case study Appendix C Validation of Prophetic Probabilities References Attack Trees vs. Fault Trees: Two Sides of the Same Coin from Different Currencies 1 Introduction 2 Similarities Between Fault and Attack Trees 2.1 Syntactic Structure: Static FTs and ATs 2.2 Semantics and Analysis 3 Differences Between Fault and Attack Trees 3.1 Analyses that Differ for Static FTs and ATs 3.2 Extensions of the Formalisms 4 Conclusions and Future Work References Author Index