Parameter synthesis for Markov models: faster than ever
From MaRDI portal
Publication:1990499
DOI10.1007/978-3-319-46520-3_4zbMATH Open1398.68346arXiv1602.05113OpenAlexW2284340808MaRDI QIDQ1990499FDOQ1990499
Authors: Tim Quatmann, Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen 
Publication date: 25 October 2018
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.
Full work available at URL: https://arxiv.org/abs/1602.05113
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
Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited In (34)
- Counterexample-guided inductive synthesis for probabilistic systems
- Tweaking the odds in probabilistic timed automata
- 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
- The complexity of reachability in parametric Markov decision processes
- 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
- Are parametric Markov chains monotonic?
- Sequential convex programming for the efficient verification of parametric MDPs
- Gradient-descent for randomized controllers under partial observability
- Out of control: reducing probabilistic models by control-state elimination
- Deniable Functional Encryption
- Synthesizing optimal bias in randomized self-stabilization
- Inductive synthesis for probabilistic programs reaches new horizons
- An efficient synthesis algorithm for parametric Markov chains against linear time properties
- Automatically finding the right probabilities in Bayesian networks
- Abstraction-Refinement for Hierarchical Probabilistic Models
- Incremental Verification of Parametric and Reconfigurable Markov Chains
- Data-efficient Bayesian verification of parametric 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
- Bridging Boolean and quantitative synthesis using smoothed proof search
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)
