Quantitative evaluation of systems : 19th International Conference, QEST 2022, Warsaw, Poland, September 12-16, 2022, proceedings / / Erika Ábrahám, Marco Paolieri, editors

• Pubblicazione: Cham, Switzerland : , : Springer, , [2022]; ©2022
• Descrizione fisica: 1 online resource (406 pages)
• Disciplina: 004.24
• Soggetto topico: Computer systems - Evaluation
• Persona (resp. second.): ÁbrahámErika; PaolieriMarco
• Nota di bibliografia: Includes bibliographical references and index.
• Nota di contenuto: Intro -- 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.
• Titolo autorizzato: Quantitative Evaluation of Systems
• ISBN: 3-031-16336-2
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Lingua di pubblicazione: Inglese
• Record Nr.: 9910592994703321
• Lo trovi qui: Univ. Federico II
• Serie: Lecture notes in computer science ; ; 13479.