Basic Model Checking Problems for Stochastic Games
| Authors | |
|---|---|
| Year of publication | 2009 |
| MU Faculty or unit | |
| Citation | |
| Description | This thesis concerns stochastic turn based games over infinite graphs with linear objectives. Stochastic games are a fundamental model for systems where three modes of behaviour appear: random changes of the state, nondeterministic changes driven by some controller and nondeterministic changes made by en environment. The nondeterminism is modelled by two players. By eliminating one of the players we get a Markov decision process, another fundamental model in probability theory and formal verification. As a game graph generator for the games studied here various subclasses of pushdown automata (PDA) are considered, in particular the class of stateless PDA (BPA), the class of one-counter automata and the whole class of PDA. Pushdown automata correspond to systems with procedures with recursive calls, which use both global and local variables. BPA, where the number of control states is eliminated to 1 model such systems without global variables. One counter automata are finite automata with one unbounded counter, capable of modelling e.g. a queue with processes of a single type which can work in various modes (quasi-birth-death processes, QBD). The central objective studied in this thesis is the reachability objective. Such an objective is specified by a set of target vertices and a probability threshold. In this setting, one of the players tries to maximise the probability of reaching the target of vertices, whereas the other player tries to minimise it. The maximiser wins if he has a strategy to ensure the probability being (strictly or non-strictly) above the threshold, no matter what the other player does. The winning condition for the minimiser is defined dually. We note that from the logical point of view, the winning conditions are not negations of each other. The problems associated with reachability which are considered here involve determining a winner of the reachability game for a given vertex of the game, computing the representation of all vertices where a given player wins, synthesising the winning strategy, or determining the value of the vertex. The study of the problem begins at the general level of infinite state stochastic games with finite branching. Several fundamental results are presented, including (strong) determinacy in the sense that in every configuration one of the players always can win. The relationship between general and positional (memoryless deterministic) strategies is also studied, as well as the existence of optimal strategies. After that we turn our attention to PDA games. We present some known undecidability results for this general class and discuss also restrictions which render several problems decidable. We also show that regularity of winning regions is tightly connected to the distinction between general and qualitative objectives, i.e. objectives where the threshold may be an arbitrary rational number, or the number 0 or 1, respectively. A complex discussion of the above problems with nontrivial solutions are presented for the mentioned problems in the classes of BPA games and one-counter automata. Finally, the Büchi objective is discussed. It differs from the reachability in the requirement that the target set should be visited infinitely many times instead of at least one visit required in reachability. We present some basic results for this objective in the context of BPA games. |
| Related projects: |