Quantitative multi-objective verification for probabilistic systems

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

Author name not available (Why is that?)

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 (43)

• Lifted model checking for relational MDPs
• Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints
• Simple Strategies in Multi-Objective MDPs
• Interval Markov decision processes with multiple objectives: from robust strategies to Pareto curves
• Optimal schedulers vs optimal bases: an approach for efficient exact solving of Markov decision processes
• Combinations of Qualitative Winning for Stochastic Parity Games
• Synthesizing efficient systems in probabilistic environments
• Model Checking Exact Cost for Attack Scenarios
• Verifying Team Formation Protocols with Probabilistic Model Checking
• Interval iteration algorithm for MDPs and IMDPs
• Deniable Functional Encryption
• 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
• Probabilistic Timed Automata with One Clock and Initialised Clock-Dependent Probabilities
• Markov automata with multiple objectives
• A multi-objective approach for PH-graphs with applications to stochastic shortest paths
• Multi-cost bounded tradeoff analysis in MDP
• Title not available (Why is that?)
• Stochastic games with lexicographic objectives
• Stochastic games with disjunctions of multiple objectives
• Graph Games and Reactive Synthesis
• Model Checking Probabilistic Systems
• Multi-objective dynamic programming with limited precision
• Reformulation of the linear program for completely ergodic MDPs with average cost criteria
• Trading performance for stability in Markov decision processes
• Faster algorithms for quantitative verification in bounded treewidth graphs
• Probabilistic Model Checking for Energy-Utility Analysis
• Exact quantitative probabilistic model checking through rational search
• Enhancing probabilistic model checking with ontologies
• Model-Free Reinforcement Learning for Lexicographic Omega-Regular Objectives
• Sequential Convex Programming for the Efficient Verification of Parametric MDPs
• Advances in Quantitative Verification for Ubiquitous Computing
• Error bounds for stochastic shortest path problems
• Quantitative Automata under Probabilistic Semantics
• 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
• Quantitative Multi-objective Verification for Probabilistic Systems
• 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)