Quantitative multi-objective verification for probabilistic systems

DOI10.1007/978-3-642-19835-9_11zbMATH Open1315.68177OpenAlexW1584965098MaRDI QIDQ3000641FDOQ3000641

Authors:

Publication date: 19 May 2011

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-19835-9_11

Recommendations

• Compositional probabilistic verification through multi-objective model checking
• Automated verification and strategy synthesis for probabilistic systems
• Quantitative automata model checking of autonomous stochastic hybrid systems
• Automatic verification of competitive stochastic systems
• Multi-objective Model Checking of Markov Decision Processes

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Title not available (Why is that?)
• Model checking of probabilistic and nondeterministic systems
• Markov Decision Processes with Multiple Objectives
• Markov Decision Processes with Multiple Long-Run Average Objectives
• Using probabilistic model checking for dynamic power management
• Quantitative multi-objective verification for probabilistic systems
• Markov decision processes and regular events
• Multi-Objective Model Checking of Markov Decision Processes
• Assume-guarantee verification for probabilistic systems
• Quantitative analysis under fairness constraints
• Title not available (Why is that?)
• Probabilistic contracts: a compositional reasoning methodology for the design of systems with stochastic and/or non-deterministic aspects
• Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives
• Title not available (Why is that?)

Cited In (44)

• Probabilistic model checking for energy-utility analysis
• Lifted model checking for relational MDPs
• Interval Markov decision processes with multiple objectives: from robust strategies to Pareto curves
• Multi-objective parameter synthesis in probabilistic hybrid systems
• Verifying team formation protocols with probabilistic model checking
• Optimal schedulers vs optimal bases: an approach for efficient exact solving of Markov decision processes
• Model checking probabilistic systems
• Combinations of Qualitative Winning for Stochastic Parity Games
• Synthesizing efficient systems in probabilistic environments
• Farkas certificates and minimal witnesses for probabilistic reachability constraints
• Model Checking Exact Cost for Attack Scenarios
• Interval iteration algorithm for MDPs and IMDPs
• Sequential convex programming for the efficient verification of parametric MDPs
• Deniable Functional Encryption
• Simple strategies in multi-objective MDPs
• Quantitative verification and strategy synthesis for stochastic games
• Formal modelling and verification of probabilistic resource bounded agents
• Multi-objective optimization of long-run average and total rewards
• Compositional probabilistic verification through multi-objective model checking
• A multi-objective approach for PH-graphs with applications to stochastic shortest paths
• Multi-cost bounded tradeoff analysis in MDP
• Stochastic games with lexicographic objectives
• Stochastic games with disjunctions of multiple objectives
• Graph Games and Reactive Synthesis
• Multi-objective dynamic programming with limited precision
• Reformulation of the linear program for completely ergodic MDPs with average cost criteria
• Quantitative multi-objective verification for probabilistic systems
• Trading performance for stability in Markov decision processes
• Faster algorithms for quantitative verification in bounded treewidth graphs
• Exact quantitative probabilistic model checking through rational search
• Enhancing probabilistic model checking with ontologies
• Model-Free Reinforcement Learning for Lexicographic Omega-Regular Objectives
• Advances in Quantitative Verification for Ubiquitous Computing
• Error bounds for stochastic shortest path problems
• Automated verification and strategy synthesis for probabilistic systems
• Collaborative models for autonomous systems controller synthesis
• Correct probabilistic model checking with floating-point arithmetic
• Synthesis of covert actuator attackers for free
• Computational Benefits of Intermediate Rewards for Goal-Reaching Policy Learning
• Pareto curves for probabilistic model checking
• Probabilistic timed automata with one clock and initialised clock-dependent probabilities
• Probabilistic timed automata with one clock and initialised clock-dependent probabilities
• Correct Hardware Design and Verification Methods
• Probabilistic black-box reachability checking (extended version)

Uses Software

• PRISM

This page was built for publication: Quantitative multi-objective verification for probabilistic systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3000641)