{"text_format":"2","workbook":"xls","n_sheets":1,"sheets":["report2"],"not_rendered":{"charts":0,"images":0,"macros":0,"external_links":1,"defined_names":1,"comments":0,"pivot_tables":0},"unopened":[],"bounds":{"document_bytes":16777216,"sheet_cells":100000,"run_cost":"one","rows_first":2000,"rows_last":500,"rows_between":2000,"halvings":0,"cell_chars":16384,"cell_head_chars":4096},"cells_cut":0,"cells_raw":0,"read":"whole","date_system":"1900","formulas":"cached_only"}

{"sheet":"report2","index":0,"n_rows":22,"n_cols":5,"rows_kept":22,"cut":false,"hidden":false,"merged":[[0,2,0,3],[0,4,0,5],[1,2,1,3],[1,4,1,5],[2,2,2,3],[4,2,4,3],[5,2,5,3],[6,2,6,3],[7,2,7,3],[8,2,8,3],[9,2,9,3],[10,2,10,3],[13,2,13,3]],"flags":["formulas_cached_only"]}
[null,"1.","Record Nr.",null,"UNISA996490364503316"]
[null,null,"Titolo",null,"Quantitative evaluation of systems : 19th International Conference, QEST 2022, Warsaw, Poland, September 12-16, 2022, proceedings / / Erika Ábrahám, Marco Paolieri, editors"]
[null,null,"Pubbl/distr/stampa",null,"Cham, Switzerland : , : Springer, , [2022]"]
[{"$nulls":4},"©2022"]
[null,null,"ISBN",null,"3-031-16336-2"]
[null,null,"Descrizione fisica",null,"1 online resource (406 pages)"]
[null,null,"Collana",null,"Lecture notes in computer science ; ; 13479"]
[null,null,"Disciplina",null,"004.24"]
[null,null,"Soggetti",null,"Computer systems - Evaluation"]
[null,null,"Lingua di pubblicazione",null,"Inglese"]
[null,null,"Formato",null,"Materiale a stampa"]
[null,null,null,"Livello bibliografico","Monografia"]
[null,null,null,"Nota di bibliografia","Includes bibliographical references and index."]
[null,null,"Nota di contenuto",null,"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 "]
[{"$nulls":4},"Stochastic Process Algebra - Exploiting Structural Properties - -- 1 Introduction -- 2 Structural Properties of SPA -- 2.1 Moving Set and Participating Set -- 2.2 Involved Set."]
[{"$nulls":4},"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."]
[{"$nulls":4},"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 "]
[{"$nulls":4},"-- 6.1 Formal Definition of PPCD -- 6.2 Stability of Planar PPCD -- 7 Conclusion -- A  Appendix."]
[{"$nulls":4},"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."]
[{"$nulls":4},"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-"]
[{"$nulls":4},"Once Quantum Finite Automata."]
[{"$nulls":4},"4 Heisenberg Quantum Finite Automata."]