Quantitative Multi-objective Verification for Probabilistic Systems
From MaRDI portal
Publication:3000641
DOI10.1007/978-3-642-19835-9_11zbMath1315.68177OpenAlexW1584965098MaRDI QIDQ3000641
No author found.
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
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)
Related Items (36)
Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints ⋮ Simple Strategies in Multi-Objective MDPs ⋮ Probabilistic Timed Automata with One Clock and Initialised Clock-Dependent Probabilities ⋮ Synthesizing efficient systems in probabilistic environments ⋮ Graph Games and Reactive Synthesis ⋮ Model Checking Probabilistic Systems ⋮ Interval iteration algorithm for MDPs and IMDPs ⋮ Quantitative verification and strategy synthesis for stochastic games ⋮ Markov automata with multiple objectives ⋮ Trading performance for stability in Markov decision processes ⋮ Computational Benefits of Intermediate Rewards for Goal-Reaching Policy Learning ⋮ A multi-objective approach for PH-graphs with applications to stochastic shortest paths ⋮ Error bounds for stochastic shortest path problems ⋮ Reformulation of the linear program for completely ergodic MDPs with average cost criteria ⋮ Compositional probabilistic verification through multi-objective model checking ⋮ Collaborative models for autonomous systems controller synthesis ⋮ Formal modelling and verification of probabilistic resource bounded agents ⋮ Multi-cost bounded tradeoff analysis in MDP ⋮ Synthesis of covert actuator attackers for free ⋮ Unnamed Item ⋮ Optimal schedulers vs optimal bases: an approach for efficient exact solving of Markov decision processes ⋮ Exact quantitative probabilistic model checking through rational search ⋮ Quantitative Multi-objective Verification for Probabilistic Systems ⋮ Quantitative Automata under Probabilistic Semantics ⋮ Combinations of Qualitative Winning for Stochastic Parity Games ⋮ Sequential Convex Programming for the Efficient Verification of Parametric MDPs ⋮ Model Checking Exact Cost for Attack Scenarios ⋮ Probabilistic Model Checking for Energy-Utility Analysis ⋮ Probabilistic black-box reachability checking (extended version) ⋮ Deniable Functional Encryption ⋮ Multi-objective optimization of long-run average and total rewards ⋮ Faster algorithms for quantitative verification in bounded treewidth graphs ⋮ Verifying Team Formation Protocols with Probabilistic Model Checking ⋮ Enhancing probabilistic model checking with ontologies ⋮ Lifted model checking for relational MDPs ⋮ Multi-objective dynamic programming with limited precision
Uses Software
Cites Work
- Probabilistic contracts: a compositional reasoning methodology for the design of systems with stochastic and/or non-deterministic aspects
- Using probabilistic model checking for dynamic power management
- Model checking of probabilistic and nondeterministic systems
- Quantitative Multi-objective Verification for Probabilistic Systems
- Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives
- Assume-Guarantee Verification for Probabilistic Systems
- Multi-Objective Model Checking of Markov Decision Processes
- Quantitative Analysis under Fairness Constraints
- Markov decision processes and regular events
- Markov Decision Processes with Multiple Objectives
- Markov Decision Processes with Multiple Long-Run Average Objectives
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Quantitative Multi-objective Verification for Probabilistic Systems