An automaton (a one-counter net, pushdown automaton, or just an NFA) is said to be history deterministic if there is a policy that constructs a run on-the-fly while reading an input word, such that if the word is in the language of the automaton, then the run on that word is accepting. There are multiple open problems concerning their algorithmic properties and expressivity.
Are history-deterministic one-counter automata strictly more expressive than deterministic one-counter automata?
The problem of checking language inclusion between history-deterministic automata, even for models beyond one-counter nets, is sandwiched between the following two problems: 1. checking language inclusion between two deterministic automata (lower bound), and 2. checking for simulation between two nondeterministic automata (upper bound). Can we pinpoint the complexity of checking language inclusion between two history-deterministic one-counter nets?
We will consider two-player games where the winning objectives are given by a Boolean combination of energy and parity conditions. E.g., the problem of deciding simulation between two one-counter nets is an instance of this problem, where the Duplicator has the objective of keeping her energy positive for at least as long until Spoiler's energy is positive.
This project will focus on identifying the Boolean combinations of energy and parity objectives for which such games are decidable. I am especially interested in objectives that arise from 2-token games or from simulation of parity one-counter nets.