9.9GTJul 15
Generalised Reachability GamesSougata Bose, Nathanael Fijalkow, Daniel Hausmann et al.
We study two-player zero-sum turn-based games played on graphs with multiple reachability objectives called generalised reachability games. In classic reachability games the goal of one player, Eve, is to visit a given target set of vertices, and that of the other player, Adam, is to prevent this. In generalised reachability games, the single target set is replaced with a family of target sets and the objective of Eve is to visit all of them in any order. We study the complexity of deciding the winner in two-player games with generalised reachability objectives. Our study reveals that an important parameter that determines the complexity of this problem is the size of the target sets. We first prove that deciding the winner in such games is PSPACE-complete, and the PSPACE lower bound holds even when the size of each target set is at most three. By contrast, we show that the problem is FPT in the number of target sets of size greater than one. Moreover, we consider the memory requirements for both players and give matching upper and lower bounds on the sizes of winning strategies. We also study optimisation variants of these games. For the optimisation problems, we show intractability for most interesting cases. Particularly, in contrast to the tractability of generalised reachability in the case with singleton target sets, the optimisation problem is coNP-hard when Eve tries to maximise the number of target sets that are visited. Tractability of this case can be recovered in a different optimisation setting where Eve is required to pledge a maximum sized subset of target sets that she can guarantee to visit.
9.2FLMar 31
Resolving Nondeterminism by ChanceSoumyajit Paul, David Purser, Sven Schewe et al.
History-deterministic automata are those in which nondeterministic choices can be correctly resolved stepwise: there is a strategy to select a continuation of a run given the next input letter so that if the overall input word admits some accepting run, then the constructed run is also accepting. Motivated by checking qualitative properties in probabilistic verification, we consider the setting where the resolver strategy can randomize and only needs to succeed with lower-bounded probability. We study the expressiveness of such stochastically-resolvable automata as well as consider the decision questions of whether a given automaton has this property. In particular, we show that it is undecidable to check if a given NFA is $λ$-stochastically resolvable. This problem is decidable for finitely-ambiguous automata. We also present complexity upper and lower bounds for several well-studied classes of automata for which this problem remains decidable.
6.4GTMay 12
Social Welfare under Heterogeneous Time PreferencesSarvin Bahmani, Soumyajit Paul, Sven Schewe et al.
In several socioeconomic-critical decision-making settings, such as fair resource allocation, climate policy, or AI alignment, multiple principals interact within a common arena. While it is well established that these principals may have differing preferences, decision-making under heterogeneous time preferences remains relatively unexplored. In particular, principals may weigh future outcomes differently and may derive distinct utilities from the same decisions. Motivated by such scenarios, we introduce the notion of heterogeneous time preferences in MDPs, where multiple principals possess distinct reward functions and apply different discount factors to future rewards. To compute meaningful decisions in such settings, an AI agent must rely on a notion of optimality that accounts for the preferences of all principals. We adopt a utilitarian notion of social welfare, defined as the sum of utilities accrued to all principals, and study the synthesis of agent strategies that maximise this welfare. Under heterogeneous time preferences, we show that optimal strategies are no longer positional, even when all principals receive identical rewards. Nevertheless, optimal strategies remain structurally simple: they can be realized as pure finite-memory counting strategies, require only polynomial memory in the system size, and can be synthesized in polynomial time. On the other hand, we show that deciding threshold questions for optimal positional strategies is NP-hard, exposing a poor trade-off: insisting on positional simplicity neither makes synthesis tractable nor preserves social welfare.