Parameter synthesis for Markov models: faster than ever
From MaRDI portal
Publication:1990499
Abstract: We propose a simple technique for verifying probabilistic models whose transition probabilities are parametric. The key is to replace parametric transitions by nondeterministic choices of extremal values. Analysing the resulting parameter-free model using off-the-shelf means yields (refinable) lower and upper bounds on probabilities of regions in the parameter space. The technique outperforms the existing analysis of parametric Markov chains by several orders of magnitude regarding both run-time and scalability. Its beauty is its applicability to various probabilistic models. It in particular provides the first sound and feasible method for performing parameter synthesis of Markov decision processes.
Recommendations
- Synthesis in pMDPs: a tale of 1001 parameters
- An efficient synthesis algorithm for parametric Markov chains against linear time properties
- Parameter Synthesis Algorithms for Parametric Interval Markov Chains
- Parameter synthesis for parametric interval Markov chains
- Finding provably optimal Markov chains
Cited in
(34)- Bridging Boolean and quantitative synthesis using smoothed proof search
- Counterexample-guided inductive synthesis for probabilistic systems
- Tweaking the odds in probabilistic timed automata
- The complexity of reachability in parametric Markov decision processes
- Parameter synthesis for Markov models: covering the parameter space
- Synthesis in pMDPs: a tale of 1001 parameters
- Interval Markov decision processes with multiple objectives: from robust strategies to Pareto curves
- On the Complexity of Reachability in Parametric Markov Decision Processes
- Finding provably optimal Markov chains
- Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination
- Accelerated model checking of parametric Markov chains
- Identity-Based Cryptosystems and Quadratic Residuosity
- Scenario-based verification of uncertain MDPs
- Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination
- Fine-tuning the odds in Bayesian networks
- Parameter Synthesis Algorithms for Parametric Interval Markov Chains
- Sampling-Based Verification of CTMCs with Uncertain Rates
- Gradient-descent for randomized controllers under partial observability
- Out of control: reducing probabilistic models by control-state elimination
- Synthesizing optimal bias in randomized self-stabilization
- Are parametric Markov chains monotonic?
- Sequential convex programming for the efficient verification of parametric MDPs
- Deniable Functional Encryption
- An efficient synthesis algorithm for parametric Markov chains against linear time properties
- Inductive synthesis for probabilistic programs reaches new horizons
- Automatically finding the right probabilities in Bayesian networks
- Abstraction-Refinement for Hierarchical Probabilistic Models
- Data-efficient Bayesian verification of parametric Markov chains
- Incremental Verification of Parametric and Reconfigurable Markov Chains
- Parameter-Independent Strategies for pMDPs via POMDPs
- Parameter synthesis in Markov models: a gentle survey
- Compositional probabilistic model checking with string diagrams of MDPs
- Counterexample-driven synthesis for probabilistic program sketches
- POMDP controllers with optimal budget
This page was built for publication: Parameter synthesis for Markov models: faster than ever
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1990499)
