Qualitative analysis of VASS-induced MDPs

DOI10.1007/978-3-662-49630-5_19MaRDI QIDQ2811349zbMATH OpenOpenAlexFDO

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)

Full work available at URL https://arxiv.org/abs/1512.08824, http://link.springer.com/chapter/10.1007/978-3-662-49630-5_19

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)

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).

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

Cites work

• scientific article; zbMATH DE number 559221 (Why is no real title available?)
• scientific article; zbMATH DE number 1134975 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• scientific article; zbMATH DE number 3310089 (Why is no real title available?)
• Automata, Languages and Programming
• Computer Science Logic
• Games for counting abstractions
• Long-run average behaviour of probabilistic vector addition systems
• Monotonic and Downward Closed Games
• One-counter Markov decision processes
• One-counter stochastic games
• Parallel program schemata
• Qualitative Logics and Equivalences for Probabilistic Systems
• Qualitative analysis of VASS-induced MDPs
• Solving parity games on integer vectors
• Stochastic Games
• The complexity of stochastic games

Cited in

(5)

• 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
• On the existence and computability of long-run average properties in probabilistic VASS
• Qualitative analysis of VASS-induced MDPs

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)