Sampling-Based Verification of CTMCs with Uncertain Rates
From MaRDI portal
Abstract: We employ uncertain parametric CTMCs with parametric transition rates and a prior on the parameter values. The prior encodes uncertainty about the actual transition rates, while the parameters allow dependencies between transition rates. Sampling the parameter values from the prior distribution then yields a standard CTMC, for which we may compute relevant reachability probabilities. We provide a principled solution, based on a technique called scenario-optimization, to the following problem: From a finite set of parameter samples and a user-specified confidence level, compute prediction regions on the reachability probabilities. The prediction regions should (with high probability) contain the reachability probabilities of a CTMC induced by any additional sample. To boost the scalability of the approach, we employ standard abstraction techniques and adapt our methodology to support approximate reachability probabilities. Experiments with various well-known benchmarks show the applicability of the approach.
Recommendations
- Scenario-based verification of uncertain MDPs
- Smoothed model checking for uncertain continuous-time Markov chains
- Lumpability for uncertain continuous-time Markov chains
- Parameter synthesis for Markov models: faster than ever
- Nested Reachability Approximation for Discrete-Time Markov Chains with Univariate Parameters
Cites work
- scientific article; zbMATH DE number 1670788 (Why is no real title available?)
- scientific article; zbMATH DE number 50712 (Why is no real title available?)
- scientific article; zbMATH DE number 2107836 (Why is no real title available?)
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- A sampling-and-discarding approach to chance-constrained optimization: feasibility and Optimality
- Bayesian statistical parameter synthesis for linear temporal properties of stochastic models
- Bounded-parameter Markov decision processes
- Computer Aided Verification
- Discrete time Markov chains with interval probabilities
- Fault tree analysis: a survey of the state-of-the-art in modeling, analysis and tools
- Introduction to the Scenario Approach
- Lumpability for uncertain continuous-time Markov chains
- Model-checking continuous-time Markov chains
- Polynomial-time verification of PCTL properties of MDPs with convex uncertainties
- Precise parameter synthesis for stochastic biochemical systems
- Risk and complexity in scenario optimization
- Sampling-Based Verification of CTMCs with Uncertain Rates
- Scenario-based verification of uncertain MDPs
- Smoothed model checking for uncertain continuous-time Markov chains
- Statistical model checking
- Statistical probabilistic model checking with a focus on time-bounded properties
- Stochastic epidemic models and their statistical analysis
- The Exact Feasibility of Randomized Solutions of Uncertain Convex Programs
- The Scenario Approach to Robust Control Design
- The probabilistic model checking landscape
- Theoretical Aspects of Computing - ICTAC 2004
- Tools and Algorithms for the Construction and Analysis of Systems
- Wait-and-judge scenario optimization
Cited in
(5)- Parameter synthesis for Markov models: covering the parameter space
- Robust Control for Dynamical Systems with Non-Gaussian Noise via Formal Abstractions
- Sampling-Based Verification of CTMCs with Uncertain Rates
- Parameter synthesis in Markov models: a gentle survey
- An MM algorithm to estimate parameters in continuous-time Markov chains
This page was built for publication: Sampling-Based Verification of CTMCs with Uncertain Rates
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6399373)
