We study asymmetrically discounted stochastic games, in which players use distinct and reasonably apart discount factors. We show that optimal strategies in these games may require both memory and randomisation, in contrast to the classical symmetrically discounted setting. Our main technical contribution establishes that computing incentive Stackelberg equilibria - a variant of Stackelberg equilibria in which one player, called Player Max, can offer payments to the other player, called Player Min - is no harder than solving classical discounted games. We further show that optimal strategies in this setting can be realised by finite counting strategies, whereas restricting players to stationary strategies makes the problem computationally intractable. Finally, we establish that computing classical Stackelberg equilibria in these games under the constraint of memoryless strategies is NP-complete and remains NP-hard even when general or counting strategies are allowed.

We survey word automata with limited nondeterminism, a family of models lying between deterministic and fully nondeterministic automata. While determinism provides a simple algorithmic basis for verification, reactive synthesis, and probabilistic analysis, determinisation incurs large state blow-up, especially for ω-regular specifications. Limited nondeterminism offers a middle ground: it preserves some of the succinctness of nondeterministic automata while retaining enough structure for algorithmic use. We focus on three notions: unambiguous automata, in which each accepted word has at most one accepting run; good-for-games automata, whose nondeterministic choices can be resolved on the fly from the input prefix; and good-for-MDPs automata, which preserve optimal satisfaction probabilities when composed with MDPs. We compare these models in terms of expressiveness, succinctness, decision problems, minimisation, and applications to model checking, synthesis, reinforcement learning, and stochastic planning. Finally, we discuss how these threads converge: recent work has used good-for-games minimisation as a preprocessing step to reduce unambiguous and good-for-MDPs automata before composition, yielding more compact constructions for probabilistic analysis and planning. We present this as a recurring algorithmic pattern - resolving an automaton’s nondeterminism before it is amplified by the product with the system - that unifies otherwise separate lines of work.

Abstract Good-for-Games (GfG) automata require that their nondeterminism can be resolved on-the-fly, while unambiguous automata guarantee that no word has more than one accepting run. These two mutually exclusive ways of restricted nondeterminism play their roles independently in Markov chain model checking (MCMC) for almost a decade but synthesising them seems hopeless: an automaton that is both GfG and unambiguous is essentially deterministic. This work breaks this perception by combining the strengths of unambiguity with the GfG co-Büchi minimisation recently proposed by Abu Radi and Kupferman. More precisely, this combination allows us to turn unambiguous automata to certain types of probabilistic automata that can be used for MCMC. The resulting automata can be exponentially smaller, and we have provided a family of automata exemplifying this state space reduction, which translates into a significant acceleration of MCMC.

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