Recently, reactive synthesis, which asks to generate a system that guarantees correctness regardless of the behaviour of its environment, has been generalised to infinite alphabets. In this setting, specifications can be formalised as register automata. As is often the case, nondeterminism in the specification automaton leads to the synthesis problem being undecidable, yet deterministic register automata are much less expressive. History-determinism is a restricted form of nondeterminism which combines some of the algorithmic properties of deterministic automata with some of the succinctness and expressivity of nondeterministic ones. In particular, the synthesis problem for history-deterministic automata tends to be no harder than for deterministic ones, which makes this an interesting class to consider for reactive synthesis. In this extended abstract, we study the expressivity and succinctness of history-deterministic register automata, as well as their whether membership to the class is decidable. We also examine whether history-determinism coincides with good-for-gameness.
History-determinism was introduced by Henzinger and Piterman in Solving Games without Determinisation ( CSL 2006) as a means to reduce the complexity of reactive synthesis algorithms, and independently discovered by Colcombet in the context of cost functions (The theory of stabilisation monoids and regular cost function, ICALP 2009). At the 32nd Nordic Workshop on Programming Theory (NWPT 2021), I gave a talk to present some preliminary results obtained together with Karoliina Lehtinen about the class of history-deterministic register automata. As of today, this is work in progress, and we hope to understand more about them in the months to come, as they offer promising perspectives to further the study of reactive synthesis over infinite alphabets (see this article for our contribution to this line of reasearch).