Quantitative evaluation of systems : 19th international conference, QEST 2022, Warsaw, Poland, September 12-16, 2022 : proceedings

This book constitutes the proceedings of the 19th International Conference on Quantitative Evaluation Systems, QEST 2022, held in Warsaw, Poland, in September 2022. The 19 full papers presented together with 1 keynote paper were carefully reviewed and selected from 44 submissions. The papers are organized in the following topics: program analysis; parameter synthesis; markovian agents and population models; dynamical systems; tools; applications and automata theory; and applications. Preface Organization Robustness Guarantees for Bayesian Neural Networks (Invited Extended Abstract of a Keynote Speaker) Contents Program Analysis Moment-Based Invariants for Probabilistic Loops with Non-polynomial Assignments 1 Introduction 2 Preliminaries 2.1 Prob-Solvable Loops 2.2 Polynomial Chaos Expansion 3 Polynomial Chaos Expansion Algorithm 3.1 Random Function Representation 3.2 PCE Algorithm 4 Prob-Solvable Loops for General Non-polynomial Functions 4.1 Iteration-Stable Distributions of Random Arguments 4.2 Iteration Non-stable Distribution of Random Arguments 5 Evaluation 6 Conclusion References Distribution Estimation for Probabilistic Loops 1 Introduction 2 Preliminaries 2.1 PPs and Moments of Random Variables 2.2 From Moments to Distributions 3 Effective Estimation of Distributions for Probabilistic Loops 3.1 Distribution Estimation 3.2 Assessing Accuracy of Estimated Distributions 4 Experimental Evaluation 5 Conclusion References An Automated Quantitative Information Flow Analysis for Concurrent Programs 1 Introduction 1.1 Paper Outline 2 Background 2.1 Basics 2.2 Information Theory 2.3 Markovian Models 2.4 Probabilistic Schedulers 3 The Proposed Approach 3.1 The Program and Threat Models 3.2 The Attacker's View of the Program: Back-Bisimulation Quotient 3.3 Measuring the Leakage Using Back-Bisimulation Quotient 3.4 Computing Back-Bisimulation Quotient 4 Conclusions and Future Work A Case Study B Related Work References Parameter Synthesis Rate Lifting for Stochastic Process Algebra – Exploiting Structural Properties – 1 Introduction 2 Structural Properties of SPA 2.1 Moving Set and Participating Set 2.2 Involved Set 3 ``Parallel'' Transitions and Relevant Selfloop Combinations 3.1 Multi-transition System 3.2 Calculating Relevant Selfloop Combinations 4 Lifting Algorithm 4.1 Spurious Transitions 4.2 Detailed Description of the Algorithm 5 Experimental Result: Cyclic Server Polling System 6 Correctness and Existence Considerations 7 Conclusion References End-to-End Statistical Model Checking for Parametric ODE Models 1 Introduction 2 Background and Notations 2.1 ODE Preliminaries 2.2 Bounded Linear Time Logic 2.3 Reward Function 3 Global Statistical Guarantees 3.1 Approximation Method for the Numerical Integration of the ODE 3.2 Monte-Carlo Method 3.3 Model Checking Extension Through Reward Functions 4 Case Studies 4.1 Case Study 1: A Study on Aurelia Aurita Population Growth ch5melica14 4.2 Case Study 2: A Prey-Predator Model for Lynx and Hares ch5restrepo10 5 Conclusion A Proof of Lemma 1 B Proof of Theorem 2 References POMDP Controllers with Optimal Budget 1 Introduction 2 Preliminaries 2.1 Rewards for pMCs 2.2 Problem Statement 2.3 Parameter Lifting 3 Monotonicity 3.1 Defining Monotonicity 3.2 Reward Order 3.3 Constructing Reward Orders 3.4 Reachability Probabilities 4 Divide and Conquer 5 Experimental Validation 6 Related Work 7 Conclusion and Future Work A Algorithm B Results C Proofs C.1 Proof Sketch of Theorem 1 C.2 Proof of Lemma 7 References Markovian Agents and Population Models A Logical Framework for Reasoning About Local and Global Properties of Collective Systems 1 Introduction 2 Modelling Global and Local Behaviours 2.1 Multi-agent Discrete Time Markov Chain 3 Global and Local Temporal Logic 3.1 Syntax 3.2 Semantic 4 Model Checking GLoTL 4.1 Operational Semantics of GLoTL Formulas 4.2 Exact Model Checking Algorithm 4.3 Statistical Model Checking of GLoTL 5 Concluding Remarks References Jump Longer to Jump Less: Improving Dynamic Boundary Projection with h-Scaling 1 Introduction 2 Background 3 h-Scaling 3.1 Static Scaling 3.2 Scaled Dynamic Boundary Projection 4 Limit Behaviour 5 Multi-scale Approximation 6 Examples 6.1 Egalitarian Processor Sharing 6.2 Malware Propagation 7 Conclusion and Related Works A Appendix A.1 Derivation of Scaled DBP A.2 Equations for Example 3 A.3 Proof of Theorem 4 A.4 Additional Data on Malware Propagation Model References Dynamical Systems An Algorithm for the Formal Reduction of Differential Equations as Over-Approximations 1 Introduction 2 Background 3 Computing Differential Hulls 4 Case Studies 4.1 SIR Model 4.2 Polymerization 4.3 Protein Interaction Network 4.4 Electrical Network 4.5 Conversion of Light Alkanes over H-ZSM-5 5 Conclusion A Appendix A.1 Proofs A.2 Experiments References Stability Analysis of Planar Probabilistic Piecewise Constant Derivative Systems 1 Introduction 2 Related Work 3 Case Study: Planar Robot with a Faulty Actuator 4 Preliminaries 4.1 Discrete-Time Markov Chain 4.2 Weighted Discrete-Time Markov Chain 4.3 Convergence of Weighted Discrete-Time Markov Chain 4.4 Probabilistic Bisimulation 4.5 Polyhedral Sets 5 Analyzing Convergence of Weighted Discrete-Time Markov Chains 5.1 Analyzing Absolute Convergence of Weighted DTMC 5.2 Analyzing Almost Sure Convergence of Weighted DTMC 5.3 Computability 6 Probabilistic Piecewise Constant Derivative Systems 6.1 Formal Definition of PPCD 6.2 Stability of Planar PPCD 7 Conclusion A Appendix A.1 Proof of Proposition 1 A.2 Algorithms from Sect. 5.3 A.3 Proof of Lemma 2 A.4 Proof of Lemma 4 References Tools LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement Learning 1 Introduction 1.1 Related Work 1.2 Contributions 2 Logically-Constrained Reinforcement Learning (LCRL) 2.1 Installation 2.2 Input Interface 2.3 Output Interface 3 Experimental Evaluation 4 Conclusions and Extensions References LN: A Meta-solver for Layered Queueing Network Analysis 1 Introduction 2 LQN Formalism 3 LQN Decomposition and Iterative Solution 3.1 Layering Strategy 3.2 Homogeneous Layers 3.3 Performance Metrics 3.4 Advanced LN Features 4 Novel Algorithms 4.1 Solving Homogeneous Layers with the CoMoM Algorithm 4.2 Solving Homogeneous Layers with Gaussian Quadratures 4.3 Computing Marginal Probabilities in Homogeneous Layers 4.4 Multi-server Nodes, Load-Dependence and Multi-class FCFS 5 Case Studies 5.1 Meta-solver Capabilities 5.2 Multi-formalism Capabilities 6 Conclusion A Proof of Theorem 1 B Gaussian Quadratures C Proof of Theorem 2 D Proof of Theorem 3 E Software Architecture Design References Eulero: A Tool for Quantitative Modeling and Evaluation of Complex Workflows 1 Introduction 2 The Eulero Library 3 Workflow Modeling 3.1 Structure Tree and STPN Blocks 3.2 Complexity Measures 3.3 Package Description 4 Workflow Evaluation 4.1 Analysis Heuristics 4.2 Package Description 5 Workflow Generation 5.1 Random Generation 5.2 Package Description 6 Conclusions References Applications Preference-Aware Computation Offloading for IoT in Multi-access Edge Computing Using Probabilistic Model Checking 1 Introduction 2 A Motivating Example 3 Problem Formulation 4 Formal Model of Computation Offloading 4.1 LTS Model of the Offloading Policy 4.2 LTS Model of the IoT Device 4.3 DTMC Model of Task Execution Latencies 4.4 Turn-Based Stochastic Multi-player Game Model Composition 4.5 Reward Formulation and IoT User Preferences 4.6 Offloading Strategy Objectives 5 Results and Discussion 6 Related Work 7 Conclusion and Future Work A Battery Model B Experimental Setup B.1 Simulation Setup References Analysis of an Electric Vehicle Charging System Along a Highway 1 Introduction 2 State of the Art 3 The Infrastructure and the EV 4 Fluid Stochastic Petri Net: The Scenario 4.1 The Battery Level 4.2 Stopping Decision Policies 4.3 Computing Decision Policy Probability 5 Solution Equation 6 Numerical Results 7 Conclusions References Verifier's Dilemma in Ethereum Blockchain: A Quantitative Analysis 1 Introduction 2 Related Work 3 Background 3.1 Verifier's Dilemma 3.2 PEPA 4 Analysis of the Verifier's Dilemma 4.1 Model Description 4.2 Model Assessment 5 Analysis of the Invalid Block Injection Policy 5.1 Model Description 5.2 Model Assessment 6 Optimal Invalid Block Injection Rate 7 Conclusion A Tables of Notations B Steady State Probabilities for BM C Steady-State Probabilities for IBIM References Comparing Statistical and Analytical Routing Approaches for Delay-Tolerant Networks 1 Introduction 2 Background 3 Routing in Uncertain DTNs 3.1 RUCoP 3.2 LSS 4 Evaluation 4.1 Benchmark Set 4.2 Analysis 5 Conclusions References Automata Theory and Applications Mirrors and Memory in Quantum Automata 1 Introduction 2 Preliminaries 2.1 Strings and Languages 2.2 Quantum Computing 3 Measure-Once Quantum Finite Automata 4 Heisenberg Quantum Finite Automata 5 Heisenberg Inspired Automata: (Un)bounded Memory 5.1 Bounded Memory 5.2 Unbounded Memory 6 Conclusions References Monte Carlo Tree Search for Priced Timed Automata 1 Introduction 2 Priced Timed Automata 3 Monte Carlo Tree Search 4 General PTA Challenges 5 Policies 6 Enhancements 7 Experiments 8 Conclusion References Author Index