Qualitative analysis of VASS-induced MDPs

DOI10.1007/978-3-662-49630-5_19zbMATH Open1475.68199arXiv1512.08824OpenAlexW2216663278MaRDI QIDQ2811349FDOQ2811349

Authors: Arnaud Sangnier, Jeremy Sproston, Parosh A. Abdulla, Richard M. Mayr 

Publication date: 10 June 2016

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Abstract: We consider infinite-state Markov decision processes (MDPs) that are induced by extensions of vector addition systems with states (VASS). Verification conditions for these MDPs are described by reachability and Buchi objectives w.r.t. given sets of control-states. We study the decidability of some qualitative versions of these objectives, i.e., the decidability of whether such objectives can be achieved surely, almost-surely, or limit-surely. While most such problems are undecidable in general, some are decidable for large subclasses in which either only the controller or only the random environment can change the counter values (while the other side can only change control-states).

Full work available at URL: https://arxiv.org/abs/1512.08824

Recommendations

• Reachability in recursive Markov decision processes
• Probabilistic Systems with LimSup and LimInf Objectives
• Reachability in Recursive Markov Decision Processes
• Decisive Markov Chains
• Qualitative Logics and Equivalences for Probabilistic Systems

Mathematics Subject Classification ID

Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• The complexity of stochastic games
• Stochastic Games
• Title not available (Why is that?)
• Title not available (Why is that?)
• Parallel program schemata
• Title not available (Why is that?)
• Title not available (Why is that?)
• One-counter Markov decision processes
• Automata, Languages and Programming
• Solving parity games on integer vectors
• Computer Science Logic
• One-counter stochastic games
• Qualitative Logics and Equivalences for Probabilistic Systems
• Monotonic and Downward Closed Games
• Qualitative analysis of VASS-induced MDPs
• Games for counting abstractions
• Long-run average behaviour of probabilistic vector addition systems

Cited In (5)

• Qualitative analysis of VASS-induced MDPs
• On the existence and computability of long-run average properties in probabilistic VASS
• Simple stochastic games with almost-sure energy-parity objectives are in NP and conp
• Strategy Complexity of Point Payoff, Mean Payoff and Total Payoff Objectives in Countable MDPs
• Deciding fast termination for probabilistic VASS with nondeterminism

This page was built for publication: Qualitative analysis of VASS-induced MDPs

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