Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
Computer Performance Engineering [[electronic resource] ] : 13th European Workshop, EPEW 2016, Chios, Greece, October 5-7, 2016, Proceedings / / edited by Dieter Fiems, Marco Paolieri, Agapios N. Platis
| Computer Performance Engineering [[electronic resource] ] : 13th European Workshop, EPEW 2016, Chios, Greece, October 5-7, 2016, Proceedings / / edited by Dieter Fiems, Marco Paolieri, Agapios N. Platis |
| Edizione | [1st ed. 2016.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 |
| Descrizione fisica | 1 online resource (XVIII, 221 p. 90 illus.) |
| Disciplina | 004.24 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Computer system failures
Mathematical statistics Computer logic Software engineering Computer simulation System Performance and Evaluation Probability and Statistics in Computer Science Logics and Meanings of Programs Software Engineering Simulation and Modeling |
| ISBN | 3-319-46433-7 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Analysis and Fitting Methods -- Computer Systems and Networking -- Modeling and Analysis of Human Behavior -- Modeling and Simulation Tools. |
| Record Nr. | UNINA-9910484679503321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Computer Performance Engineering [[electronic resource] ] : 13th European Workshop, EPEW 2016, Chios, Greece, October 5-7, 2016, Proceedings / / edited by Dieter Fiems, Marco Paolieri, Agapios N. Platis
| Computer Performance Engineering [[electronic resource] ] : 13th European Workshop, EPEW 2016, Chios, Greece, October 5-7, 2016, Proceedings / / edited by Dieter Fiems, Marco Paolieri, Agapios N. Platis |
| Edizione | [1st ed. 2016.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 |
| Descrizione fisica | 1 online resource (XVIII, 221 p. 90 illus.) |
| Disciplina | 004.24 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Computer system failures
Mathematical statistics Computer logic Software engineering Computer simulation System Performance and Evaluation Probability and Statistics in Computer Science Logics and Meanings of Programs Software Engineering Simulation and Modeling |
| ISBN | 3-319-46433-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Analysis and Fitting Methods -- Computer Systems and Networking -- Modeling and Analysis of Human Behavior -- Modeling and Simulation Tools. |
| Record Nr. | UNISA-996466250103316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Performance Evaluation Methodologies and Tools [[electronic resource] ] : 16th EAI International Conference, VALUETOOLS 2023, Crete, Greece, September 6–7, 2023, Proceedings / / edited by Evangelia Kalyvianaki, Marco Paolieri
| Performance Evaluation Methodologies and Tools [[electronic resource] ] : 16th EAI International Conference, VALUETOOLS 2023, Crete, Greece, September 6–7, 2023, Proceedings / / edited by Evangelia Kalyvianaki, Marco Paolieri |
| Autore | Kalyvianaki Evangelia |
| Edizione | [1st ed. 2024.] |
| Pubbl/distr/stampa | Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2024 |
| Descrizione fisica | 1 online resource (189 pages) |
| Disciplina | 004.2 |
| Altri autori (Persone) | PaolieriMarco |
| Collana | Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering |
| Soggetto topico |
Computer systems
Computers Computer input-output equipment Computer networks Computers, Special purpose Computer System Implementation Computer Hardware Input/Output and Data Communications Computer Communication Networks Special Purpose and Application-Based Systems |
| ISBN | 3-031-48885-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | An Anti-Jamming Game When None Player Knows Rival's Channel Gain -- Selfish Mining in Public Blockchains: A Quantitative Analysis -- Improving Sample Efficiency in Evolutionary RL Using Off-Policy Ranking -- Efficiency of Symmetric Nash Equilibria in Epidemic Models with Confinements -- The best of both worlds: Analytically-guided simulation of HPnGs for optimal reachability -- Kubernetes-in-the-Loop: Enriching Microservice Simulation Through Authentic Container Orchestration -- Quantum-enhanced control of a tandem queue system -- Combining Static and Dynamic Traffic with Delay Guarantees in Time-Sensitive Networking -- Caching Contents with Varying Popularity using Restless Bandits -- dSalmon: High-Speed Anomaly Detection for Evolving Multivariate Data Streams -- RealySt: A C++ Tool for Optimizing Reachability Probabilities in Stochastic Hybrid Systems. |
| Record Nr. | UNINA-9910799218903321 |
Kalyvianaki Evangelia
|
||
| Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2024 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Quantitative evaluation of systems : 19th International Conference, QEST 2022, Warsaw, Poland, September 12-16, 2022, proceedings / / Erika Ábrahám, Marco Paolieri, editors
| Quantitative evaluation of systems : 19th International Conference, QEST 2022, Warsaw, Poland, September 12-16, 2022, proceedings / / Erika Ábrahám, Marco Paolieri, editors |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
| Descrizione fisica | 1 online resource (406 pages) |
| Disciplina | 004.24 |
| Collana | Lecture notes in computer science |
| Soggetto topico | Computer systems - Evaluation |
| ISBN | 3-031-16336-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| 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. |
| Record Nr. | UNINA-9910592994703321 |
| Cham, Switzerland : , : Springer, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Quantitative evaluation of systems : 19th International Conference, QEST 2022, Warsaw, Poland, September 12-16, 2022, proceedings / / Erika Ábrahám, Marco Paolieri, editors
| Quantitative evaluation of systems : 19th International Conference, QEST 2022, Warsaw, Poland, September 12-16, 2022, proceedings / / Erika Ábrahám, Marco Paolieri, editors |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
| Descrizione fisica | 1 online resource (406 pages) |
| Disciplina | 004.24 |
| Collana | Lecture notes in computer science |
| Soggetto topico | Computer systems - Evaluation |
| ISBN | 3-031-16336-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| 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. |
| Record Nr. | UNISA-996490364503316 |
| Cham, Switzerland : , : Springer, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||