Qualitative Analysis of VASS-Induced MDPs

TL;DR

This paper investigates the decidability of qualitative objectives in infinite-state Markov decision processes induced by vector addition systems with states, focusing on reachability and Buchi objectives under various control conditions.

Contribution

It identifies decidable subclasses of VASS-induced MDPs for qualitative objectives, where only the controller or only the environment can alter counter values.

Findings

Decidability results for certain subclasses of VASS-MDPs

Undecidability results for general VASS-MDPs

Analysis of reachability and Buchi objectives in infinite-state MDPs

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