Quantitative Evaluation of Systems

Name: Quantitative Evaluation of Systems | 15th International Conference, QEST 2018, Beijing, China, September 4-7, 2018, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

15th International Conference, QEST 2018, Beijing, China, September 4-7, 2018, Proceedings

Annabelle McIver Andras Horvath(Herausgeber*in)

Springer (Verlag)

Erschienen am 27. August 2018

XI, 423 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-319-99154-2 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

Intro
Preface
Organization
Contents
On the Additive Capacity Problem for Quantitative Information Flow
1 Introduction
2 Preliminaries
3 Computing Additive Capacities
3.1 The Kantorovich and Wasserstein Distances
3.2 Computing Additive (G,)-capacity
3.3 Additive Capacity for 1-spanning Gain Functions
3.4 Additive Capacity for 1-spanning Vulnerability Functions
3.5 Maximize over both g and
4 The Additive Miracle Theorem
5 Conclusion and Future Work
References
HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties
1 Introduction
2 HyperPCTL
2.1 HyperPCTL Syntax
2.2 HyperPCTL Semantics
3 HyperPCTL in Action
3.1 Probabilistic Bisimulation
3.2 Probabilistic Noninterfence
3.3 Differential Privacy
3.4 Probabilistic Causation
4 HyperPCTL Model Checking
5 Related Work
6 Conclusion and Future Work
References
How Fast Is MQTT?
1 Introduction
2 Background
2.1 Statistical Model Checking (SMC)
2.2 Property-Based Testing (PBT)
2.3 Stochastic Timed Automata
2.4 Integration of SMC into PBT
3 Method
4 Evaluation
5 Conclusion
References
Parameter-Independent Strategies for pMDPs via POMDPs
1 Introduction
2 Related Work
3 The Models
3.1 Markov Decision Processes - MDPs
3.2 Parametric MDPs - pMDPs
3.3 Partially Observable MDPs - POMDPs
4 The Encoding
5 Experiments
6 Conclusion
References
On the Verification of Weighted Kripke Structures Under Uncertainty
1 Introduction
2 Weighted Kripke Structures and Weighted CTL
3 Parametric Weighted Kripke Structures
4 Extended Parametric Dependency Graphs
5 Model Checking Parametric WKSS Using EPDGs
6 Weight-Uncertain Kripke Structures
7 Experimental Results
8 Conclusion and Future Work
References
Hospital Inventory Management Through Markov Decision Processes @runtime
1 Introduction
2 Application Context
2.1 Problem Formulation
2.2 Drug Consumption Data
3 Solution Method
3.1 Probabilistic Model Checking of an MDP @runtime
3.2 Estimating Drug Consumption Probabilities Through a DPH
3.3 Estimating Drug Consumption Probabilities Through an HMM
4 Experiments
4.1 Experimental Setup
4.2 Experimental Results
5 Conclusions
References
Guaranteed Error Bounds on Approximate Model Abstractions Through Reachability Analysis
1 Introduction
2 Background
3 Approximate Differential Equivalences
4 Error Bounds
5 Evaluation
6 Conclusion
References
Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties
1 Introduction
2 Preliminaries
2.1 Probabilistic Timed Automata
2.2 Timed Automata
3 Problem Statement
4 The PTA-DTRA Problem
5 The PTA-TRA Problem
6 Conclusion
7 Related Works
References
Incremental Verification of Parametric and Reconfigurable Markov Chains
1 Introduction
2 Related Work
3 Algorithms
3.1 State Elimination
3.2 Reconfiguration
3.3 Correctness
3.4 Extension to Parametric Markov Reward Models
4 Case Studies
4.1 Zeroconf
4.2 Oscillator Synchronisation
5 Conclusion and Future Work
References
Lumping the Approximate Master Equation for Multistate Processes on Complex Networks
1 Introduction
2 The Multistate Approximate Master Equation
2.1 Multistate Markovian Processes
2.2 Multistate AME
3 Lumping
3.1 Lumping the Initial State and the Time Derivative
3.2 Building the Lumped Equations
4 Partitioning of the Neighborhood Set
4.1 Hierarchical Clustering for Degrees
4.2 Proportionality Clustering
4.3 Joint Clusters
4.4 Stopping Heuristic
5 Case Studies
5.1 SIR
5.2 Rumor Spreading
5.3 Competing Pathogens
6 Conclusions and Future Work
References
Analytical Solution for Long Battery Lifetime Prediction in Nonadaptive Systems
1 Introduction
2 Battery Model
2.1 Kinetic Battery Model
2.2 Modeling KiBaM in Uppaal SMC
2.3 Analytical Solution to KiBaM
2.4 Tool Chain for KiBaM Battery Consumption
3 Case Study on Battery Charge in Wireless Networks
3.1 Protocol Descriptions
3.2 Power Modes in Protocols
3.3 Experiments
4 Simulation Traces for Estimating Long Battery Lifetime
4.1 Extension of Simulation Traces
4.2 Experiments with Long Battery Lifetime Prediction
5 Conclusion and Future Work
References
Action and State Based Computation Tree Measurement Language and Algorithms
1 Introduction
2 Foundations
3 Action and State Based Computation Tree Measurement Language
3.1 asCTML Syntax
3.2 Semantics of asCTML
4 asCTML Computation
5 The University Graduation Application
5.1 Specification Examples
5.2 Experimental Results
6 Related Work
7 Conclusions and Future Work
References
Model Checking for Safe Navigation Among Humans
1 Introduction
2 Preliminaries
3 Partially Controlled Multi-agent Setting
4 Case Study
4.1 Operational Model
4.2 Experimental Setup
5 Results
6 Discussion
7 Conclusion
References
Automated Verification of Concurrent Stochastic Games
1 Introduction
2 Preliminaries
3 rPATL for Concurrent Stochastic Games
4 Model Checking CSGs Against rPATL
5 Implementation and Tool Support
6 Case Studies and Experimental Results
7 Conclusion
References
Bounded Verification of Reachability of Probabilistic Hybrid Systems
1 Introduction
2 Preliminaries
3 Markov Decision Processes
3.1 Inductive Definition of Probabilistic Reachability
4 Probabilistic Hybrid Systems
4.1 Syntax
4.2 Semantics
4.3 Subclasses of Probabilistic Hybrid Systems
5 Computing Probability of Reachability
6 Experiments
7 Conclusions
References
Control and Optimization of the SRPT Service Policy by Frequency Scaling
1 Introduction
2 Related Work
3 Description of the Model
4 The Model with K=2 Frequency Levels
4.1 Exact Analysis
4.2 Approximate Solution
5 Numerical and Simulation Results
6 Conclusion
References
Biased Processor Sharing in Fork-Join Queues
1 Introduction
2 Related Work
3 Policies for Biased Processor Sharing in Fork-Join Queues
4 The Model for the DBS
4.1 Stationary Analysis of XK(t) for K=2
4.2 Stationary Analysis of XK(t) for K&2
4.3 Marginal Probabilities and Expected Performance Indices
5 Comparison of the Scheduling Disciplines
6 Conclusion
References
Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference
1 Introduction
2 Related Work
3 Background
3.1 Moment Closure Approximation
3.2 Probabilistic Model Checking
4 Methodology
4.1 Time-Bounded Reachability as Bayesian Inference
4.2 The Time-Bounded Until Operator
4.3 Gaussian Approximation via Assumed Density Filtering
4.4 Algorithm
5 Examples
5.1 An Epidemiology Model
5.2 LacZ - A Model of Prokaryotic Gene Expression
5.3 A Stiff Viral Model
5.4 A Genetic Oscillator
5.5 A Note on the Execution Times
6 Conclusions
References
LIFT: Learning Fault Trees from Observational Data
1 Introduction
2 Related Work
3 Background: Fault Trees
4 Machine Learning Fault Trees
5 Evaluation
5.1 Results
5.2 Complexity
6 Discussion
7 Conclusion
References
A Robust Genetic Algorithm for Learning Temporal Specifications from Data
1 Introduction
2 Signal Temporal Logic
3 Problem Formulation
4 Methodology
4.1 Discrimination Function G()
4.2 GB-UCP: Learning the Parameters of the Formula
4.3 Genetic Algorithm: Learning the Structure of the Formula
5 Case Studies and Experimental Results
5.1 Maritime Surveillance
5.2 Ineffective Inspiratory Effort (IIE)
6 Conclusion
References
A Hemimetric Extension of Simulation for Semi-Markov Decision Processes
1 Introduction
2 Semi-Markov Decision Processes
3 Comparing the Speed of Residence-Time Distributions
4 A Hemimetric for Semi-Markov Decision Processes
5 Computing the Simulation Distance
6 Compositional Properties of the Simulation Distance
7 Logical Properties of the Simulation Distance
7.1 Reachability Properties
8 Conclusions and Open Problems
References
Policy Synthesis for Collective Dynamics
1 Introduction
2 System Specification
2.1 Broadcast Communication
2.2 Language and Configuration
2.3 Syntax
2.4 Semantics
3 Policy Synthesis
3.1 Policy Synthesis via Fluid Approximation
3.2 Approximation for Mode Switching
4 Analysis: Running Example
4.1 Policy Synthesis
5 Conclusion
References
Modeling Humans: A General Agent Model for the Evaluation of Security
1 Introduction
2 Related Work
3 A General Agent Model for Evaluation of Security
3.1 Model Formalism Definition
3.2 Model Execution
3.3 Metrics
3.4 Limitations
4 Example
4.1 Composed Model
4.2 Adversary Submodel
4.3 Defender Submodel
4.4 User Submodel
4.5 Media Submodel
4.6 Reward Model: Defining Metrics
4.7 Model Execution and Results
5 Conclusion
References
Approximate Time Bounded Reachability for CTMCs and CTMDPs: A Lyapunov Approach
1 Introduction
2 Continuous-Time Markov Chains
3 Time-Bounded Reachability on CTMCs
3.1 From Reachability to Linear Dynamical Systems
3.2 Bisimulation and Projections
3.3 Generalised Projections and Reduction
4 Time-Bounded Reachability on CTMDPs
5 Simulation Results
6 Discussions
References
On Saturation Effects in Coupled Speed Scaling
1 Introduction
2 Background and Related Work
3 System Model
3.1 Model Overview and Assumptions
3.2 Markov Chain Model
4 Analytical and Numerical Results
4.1 Mean and Variance of Speed
4.2 Mean and Variance of Occupancy
4.3 System Saturation
4.4 Mean Busy Period
5 Simulation Results
6 Conclusions
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken