-
Revelations: A Decidable Class of POMDPs with Omega-Regular Objectives
Authors:
Marius Belly,
Nathanaël Fijalkow,
Hugo Gimbert,
Florian Horn,
Guillermo A. Pérez,
Pierre Vandenhove
Abstract:
Partially observable Markov decision processes (POMDPs) form a prominent model for uncertainty in sequential decision making. We are interested in constructing algorithms with theoretical guarantees to determine whether the agent has a strategy ensuring a given specification with probability 1. This well-studied problem is known to be undecidable already for very simple omega-regular objectives, b…
▽ More
Partially observable Markov decision processes (POMDPs) form a prominent model for uncertainty in sequential decision making. We are interested in constructing algorithms with theoretical guarantees to determine whether the agent has a strategy ensuring a given specification with probability 1. This well-studied problem is known to be undecidable already for very simple omega-regular objectives, because of the difficulty of reasoning on uncertain events. We introduce a revelation mechanism which restricts information loss by requiring that almost surely the agent has eventually full information of the current state. Our main technical results are to construct exact algorithms for two classes of POMDPs called weakly and strongly revealing. Importantly, the decidable cases reduce to the analysis of a finite belief-support Markov decision process. This yields a conceptually simple and exact algorithm for a large class of POMDPs.
△ Less
Submitted 16 December, 2024;
originally announced December 2024.
-
A positional $\mathbfΠ^0_3$-complete objective
Authors:
Antonio Casares,
Pierre Ohlmann,
Pierre Vandenhove
Abstract:
We study zero-sum turn-based games on graphs. In this note, we show the existence of a game objective that is $\mathbfΠ^0_3$-complete for the Borel hierarchy and that is positional, i.e., for which positional strategies suffice for the first player to win over arenas of arbitrary cardinality. To the best of our knowledge, this is the first known such objective; all previously known positional obje…
▽ More
We study zero-sum turn-based games on graphs. In this note, we show the existence of a game objective that is $\mathbfΠ^0_3$-complete for the Borel hierarchy and that is positional, i.e., for which positional strategies suffice for the first player to win over arenas of arbitrary cardinality. To the best of our knowledge, this is the first known such objective; all previously known positional objectives are in $\mathbfΣ^0_3$. The objective in question is a qualitative variant of the well-studied total-payoff objective, where the goal is to maximise the sum of weights.
△ Less
Submitted 3 October, 2024;
originally announced October 2024.
-
The Power of Counting Steps in Quantitative Games
Authors:
Sougata Bose,
Rasmus Ibsen-Jensen,
David Purser,
Patrick Totzke,
Pierre Vandenhove
Abstract:
We study deterministic games of infinite duration played on graphs and focus on the strategy complexity of quantitative objectives. Such games are known to admit optimal memoryless strategies over finite graphs, but require infinite-memory strategies in general over infinite graphs.
We provide new lower and upper bounds for the strategy complexity of mean-payoff and total-payoff objectives over…
▽ More
We study deterministic games of infinite duration played on graphs and focus on the strategy complexity of quantitative objectives. Such games are known to admit optimal memoryless strategies over finite graphs, but require infinite-memory strategies in general over infinite graphs.
We provide new lower and upper bounds for the strategy complexity of mean-payoff and total-payoff objectives over infinite graphs, focusing on whether step-counter strategies (sometimes called Markov strategies) suffice to implement winning strategies. In particular, we show that over finitely branching arenas, three variants of limsup mean-payoff and total-payoff objectives admit winning strategies that are based either on a step counter or on a step counter and an additional bit of memory. Conversely, we show that for certain liminf total-payoff objectives, strategies resorting to a step counter and finite memory are not sufficient. For step-counter strategies, this settles the case of all classical quantitative objectives up to the second level of the Borel hierarchy.
△ Less
Submitted 25 June, 2024;
originally announced June 2024.
-
How to Play Optimally for Regular Objectives?
Authors:
Patricia Bouyer,
Nathanaël Fijalkow,
Mickael Randour,
Pierre Vandenhove
Abstract:
This paper studies two-player zero-sum games played on graphs and makes contributions toward the following question: given an objective, how much memory is required to play optimally for that objective? We study regular objectives, where the goal of one of the two players is that eventually the sequence of colors along the play belongs to some regular language of finite words. We obtain different…
▽ More
This paper studies two-player zero-sum games played on graphs and makes contributions toward the following question: given an objective, how much memory is required to play optimally for that objective? We study regular objectives, where the goal of one of the two players is that eventually the sequence of colors along the play belongs to some regular language of finite words. We obtain different characterizations of the chromatic memory requirements for such objectives for both players, from which we derive complexity-theoretic statements: deciding whether there exist small memory structures sufficient to play optimally is NP-complete for both players. Some of our characterization results apply to a more general class of objectives: topologically closed and topologically open sets.
△ Less
Submitted 18 September, 2023; v1 submitted 18 October, 2022;
originally announced October 2022.
-
Half-Positional Objectives Recognized by Deterministic Büchi Automata
Authors:
Patricia Bouyer,
Antonio Casares,
Mickael Randour,
Pierre Vandenhove
Abstract:
In two-player games on graphs, the simplest possible strategies are those that can be implemented without any memory. These are called positional strategies. In this paper, we characterize objectives recognizable by deterministic Büchi automata (a subclass of omega-regular objectives) that are half-positional, that is, for which the protagonist can always play optimally using positional strategies…
▽ More
In two-player games on graphs, the simplest possible strategies are those that can be implemented without any memory. These are called positional strategies. In this paper, we characterize objectives recognizable by deterministic Büchi automata (a subclass of omega-regular objectives) that are half-positional, that is, for which the protagonist can always play optimally using positional strategies (both over finite and infinite graphs). Our characterization consists of three natural conditions linked to the language-theoretic notion of right congruence. Furthermore, this characterization yields a polynomial-time algorithm to decide half-positionality of an objective recognized by a given deterministic Büchi automaton.
△ Less
Submitted 28 August, 2024; v1 submitted 3 May, 2022;
originally announced May 2022.
-
Characterizing Omega-Regularity through Finite-Memory Determinacy of Games on Infinite Graphs
Authors:
Patricia Bouyer,
Mickael Randour,
Pierre Vandenhove
Abstract:
We consider zero-sum games on infinite graphs, with objectives specified as sets of infinite words over some alphabet of colors. A well-studied class of objectives is the one of $ω$-regular objectives, due to its relation to many natural problems in theoretical computer science. We focus on the strategy complexity question: given an objective, how much memory does each player require to play as we…
▽ More
We consider zero-sum games on infinite graphs, with objectives specified as sets of infinite words over some alphabet of colors. A well-studied class of objectives is the one of $ω$-regular objectives, due to its relation to many natural problems in theoretical computer science. We focus on the strategy complexity question: given an objective, how much memory does each player require to play as well as possible? A classical result is that finite-memory strategies suffice for both players when the objective is $ω$-regular. We show a reciprocal of that statement: when both players can play optimally with a chromatic finite-memory structure (i.e., whose updates can only observe colors) in all infinite game graphs, then the objective must be $ω$-regular. This provides a game-theoretic characterization of $ω$-regular objectives, and this characterization can help in obtaining memory bounds. Moreover, a by-product of our characterization is a new one-to-two-player lift: to show that chromatic finite-memory structures suffice to play optimally in two-player games on infinite graphs, it suffices to show it in the simpler case of one-player games on infinite graphs. We illustrate our results with the family of discounted-sum objectives, for which $ω$-regularity depends on the value of some parameters.
△ Less
Submitted 13 January, 2023; v1 submitted 4 October, 2021;
originally announced October 2021.
-
Arena-Independent Finite-Memory Determinacy in Stochastic Games
Authors:
Patricia Bouyer,
Youssouf Oualhadj,
Mickael Randour,
Pierre Vandenhove
Abstract:
We study stochastic zero-sum games on graphs, which are prevalent tools to model decision-making in presence of an antagonistic opponent in a random environment. In this setting, an important question is the one of strategy complexity: what kinds of strategies are sufficient or required to play optimally (e.g., randomization or memory requirements)? Our contributions further the understanding of a…
▽ More
We study stochastic zero-sum games on graphs, which are prevalent tools to model decision-making in presence of an antagonistic opponent in a random environment. In this setting, an important question is the one of strategy complexity: what kinds of strategies are sufficient or required to play optimally (e.g., randomization or memory requirements)? Our contributions further the understanding of arena-independent finite-memory (AIFM) determinacy, i.e., the study of objectives for which memory is needed, but in a way that only depends on limited parameters of the game graphs. First, we show that objectives for which pure AIFM strategies suffice to play optimally also admit pure AIFM subgame perfect strategies. Second, we show that we can reduce the study of objectives for which pure AIFM strategies suffice in two-player stochastic games to the easier study of one-player stochastic games (i.e., Markov decision processes). Third, we characterize the sufficiency of AIFM strategies through two intuitive properties of objectives. This work extends a line of research started on deterministic games to stochastic ones.
△ Less
Submitted 30 November, 2023; v1 submitted 19 February, 2021;
originally announced February 2021.
-
Decisiveness of Stochastic Systems and its Application to Hybrid Models (Full Version)
Authors:
Patricia Bouyer,
Thomas Brihaye,
Mickael Randour,
Cédric Rivière,
Pierre Vandenhove
Abstract:
In [ABM07], Abdulla et al. introduced the concept of decisiveness, an interesting tool for lifting good properties of finite Markov chains to denumerable ones. Later, this concept was extended to more general stochastic transition systems (STSs), allowing the design of various verification algorithms for large classes of (infinite) STSs. We further improve the understanding and utility of decisive…
▽ More
In [ABM07], Abdulla et al. introduced the concept of decisiveness, an interesting tool for lifting good properties of finite Markov chains to denumerable ones. Later, this concept was extended to more general stochastic transition systems (STSs), allowing the design of various verification algorithms for large classes of (infinite) STSs. We further improve the understanding and utility of decisiveness in two ways. First, we provide a general criterion for proving decisiveness of general STSs. This criterion, which is very natural but whose proof is rather technical, (strictly) generalizes all known criteria from the literature. Second, we focus on stochastic hybrid systems (SHSs), a stochastic extension of hybrid systems. We establish the decisiveness of a large class of SHSs and, under a few classical hypotheses from mathematical logic, we show how to decide reachability problems in this class, even though they are undecidable for general SHSs. This provides a decidable stochastic extension of o-minimal hybrid systems.
[ABM07] Parosh A. Abdulla, Noomene Ben Henda, and Richard Mayr. 2007. Decisive Markov Chains. Log. Methods Comput. Sci. 3, 4 (2007).
△ Less
Submitted 10 January, 2022; v1 submitted 28 September, 2020;
originally announced September 2020.
-
Decisiveness for countable MDPs and insights for NPLCSs and POMDPs
Authors:
Nathalie Bertrand,
Patricia Bouyer,
Thomas Brihaye,
Paulin Fournier,
Pierre Vandenhove
Abstract:
Markov chains and Markov decision processes (MDPs) are well-established probabilistic models. While finite Markov models are well-understood, analysing their infinite counterparts remains a significant challenge. Decisiveness has proven to be an elegant property for countable Markov chains: it is general enough to be satisfied by several natural classes of countable Markov chains, and it is a suff…
▽ More
Markov chains and Markov decision processes (MDPs) are well-established probabilistic models. While finite Markov models are well-understood, analysing their infinite counterparts remains a significant challenge. Decisiveness has proven to be an elegant property for countable Markov chains: it is general enough to be satisfied by several natural classes of countable Markov chains, and it is a sufficient condition for simple qualitative and approximate quantitative model-checking algorithms to exist.
In contrast, existing works on the formal analysis of countable MDPs usually rely on ad hoc techniques tailored to specific classes. We provide here a general framework to analyse countable MDPs by extending the notion of decisiveness. Compared to Markov chains, MDPs exhibit extra non-determinism that can be resolved in an adversarial or cooperative way, leading to multiple natural notions of decisiveness. We show that these notions enable the approximation of reachability and safety probabilities in countable MDPs using simple model-checking procedures.
We then instantiate our generic approach to two concrete classes of models inducing countable MDPs: non-deterministic probabilistic lossy channel systems and partially observable MDPs. This leads to an algorithm to approximately compute safety probabilities in each of these classes.
△ Less
Submitted 21 April, 2025; v1 submitted 24 August, 2020;
originally announced August 2020.
-
Decisiveness of Stochastic Systems and its Application to Hybrid Models
Authors:
Patricia Bouyer,
Thomas Brihaye,
Mickael Randour,
Cédric Rivière,
Pierre Vandenhove
Abstract:
In [ABM07], Abdulla et al. introduced the concept of decisiveness, an interesting tool for lifting good properties of finite Markov chains to denumerable ones. Later, this concept was extended to more general stochastic transition systems (STSs), allowing the design of various verification algorithms for large classes of (infinite) STSs. We further improve the understanding and utility of decisive…
▽ More
In [ABM07], Abdulla et al. introduced the concept of decisiveness, an interesting tool for lifting good properties of finite Markov chains to denumerable ones. Later, this concept was extended to more general stochastic transition systems (STSs), allowing the design of various verification algorithms for large classes of (infinite) STSs. We further improve the understanding and utility of decisiveness in two ways. First, we provide a general criterion for proving decisiveness of general STSs. This criterion, which is very natural but whose proof is rather technical, (strictly) generalizes all known criteria from the literature. Second, we focus on stochastic hybrid systems (SHSs), a stochastic extension of hybrid systems. We establish the decisiveness of a large class of SHSs and, under a few classical hypotheses from mathematical logic, we show how to decide reachability problems in this class, even though they are undecidable for general SHSs. This provides a decidable stochastic extension of o-minimal hybrid systems. [ABM07] Parosh A. Abdulla, Noomene Ben Henda, and Richard Mayr. 2007. Decisive Markov Chains. Log. Methods Comput. Sci. 3, 4 (2007).
△ Less
Submitted 22 September, 2020; v1 submitted 13 January, 2020;
originally announced January 2020.
-
Games Where You Can Play Optimally with Arena-Independent Finite Memory
Authors:
Patricia Bouyer,
Stéphane Le Roux,
Youssouf Oualhadj,
Mickael Randour,
Pierre Vandenhove
Abstract:
For decades, two-player (antagonistic) games on graphs have been a framework of choice for many important problems in theoretical computer science. A notorious one is controller synthesis, which can be rephrased through the game-theoretic metaphor as the quest for a winning strategy of the system in a game against its antagonistic environment. Depending on the specification, optimal strategies mig…
▽ More
For decades, two-player (antagonistic) games on graphs have been a framework of choice for many important problems in theoretical computer science. A notorious one is controller synthesis, which can be rephrased through the game-theoretic metaphor as the quest for a winning strategy of the system in a game against its antagonistic environment. Depending on the specification, optimal strategies might be simple or quite complex, for example having to use (possibly infinite) memory. Hence, research strives to understand which settings allow for simple strategies.
In 2005, Gimbert and Zielonka provided a complete characterization of preference relations (a formal framework to model specifications and game objectives) that admit memoryless optimal strategies for both players. In the last fifteen years however, practical applications have driven the community toward games with complex or multiple objectives, where memory -- finite or infinite -- is almost always required. Despite much effort, the exact frontiers of the class of preference relations that admit finite-memory optimal strategies still elude us.
In this work, we establish a complete characterization of preference relations that admit optimal strategies using arena-independent finite memory, generalizing the work of Gimbert and Zielonka to the finite-memory case. We also prove an equivalent to their celebrated corollary of great practical interest: if both players have optimal (arena-independent-)finite-memory strategies in all one-player games, then it is also the case in all two-player games. Finally, we pinpoint the boundaries of our results with regard to the literature: our work completely covers the case of arena-independent memory (e.g., multiple parity objectives, lower- and upper-bounded energy objectives), and paves the way to the arena-dependent case (e.g., multiple lower-bounded energy objectives).
△ Less
Submitted 14 January, 2022; v1 submitted 12 January, 2020;
originally announced January 2020.
-
Functional Design of Computation Graph
Authors:
Pierre Vandenhove
Abstract:
Representing the control flow of a computer program as a computation graph can bring many benefits in a broad variety of domains where performance is critical. This technique is a core component of most major numerical libraries (TensorFlow, PyTorch, Theano, MXNet,...) and is successfully used to speed up and optimise many computationally-intensive tasks. However, different design choices in each…
▽ More
Representing the control flow of a computer program as a computation graph can bring many benefits in a broad variety of domains where performance is critical. This technique is a core component of most major numerical libraries (TensorFlow, PyTorch, Theano, MXNet,...) and is successfully used to speed up and optimise many computationally-intensive tasks. However, different design choices in each of these libraries lead to noticeable differences in efficiency and in the way an end user writes efficient code. In this report, we detail the implementation and features of the computation graph support in OCaml's numerical library Owl, a recent entry in the world of scientific computing.
△ Less
Submitted 10 December, 2018;
originally announced December 2018.
