History Determinism vs. Good for Gameness in Quantitative Automata

TL;DR

This paper explores the relationships and differences between history determinism, good for gameness, and determinisability by pruning in quantitative automata, with implications for synthesis problems.

Contribution

It clarifies the distinctions between these automata models in the quantitative setting and relates them to synthesis approaches, extending prior Boolean results.

Findings

Good for gameness is broader than history determinism in quantitative automata.

History determinism coincides with determinisability by pruning under certain criteria.

Good-for-games automata are key for classical synthesis, while history deterministic automata relate to local synthesis.

Abstract

Automata models between determinism and nondeterminism/alternations can retain some of the algorithmic properties of deterministic automata while enjoying some of the expressiveness and succinctness of nondeterminism. We study three closely related such models -- history determinism, good for gameness and determinisability by pruning -- on quantitative automata. While in the Boolean setting, history determinism and good for gameness coincide, we show that this is no longer the case in the quantitative setting: good for gameness is broader than history determinism, and coincides with a relaxed version of it, defined with respect to thresholds. We further identify criteria in which history determinism, which is generally broader than determinisability by pruning, coincides with it, which we then apply to typical quantitative automata types. As a key application of good for games and history deterministic automata is synthesis, we clarify the relationship between the two notions and various quantitative synthesis problems. We show that good-for-games automata are central for "global" (classical) synthesis, while "local" (good-enough) synthesis reduces to deciding whether a nondeterministic automaton is history deterministic.