Games on mildly nondeterministic automata: limit-average history-deterministic automata

History-determinism

History-deterministic automata are mildly nondeterministic automata, as follows. An automaton A is history-deterministic if Eve wins the following game:

At each turn Adam plays a letter, and Eve responds with a transition of A over this letter; in the limit, a play consists of a word played by Adam and a run (sequence of transitions) of A, played by Eve. Eve wins if either Adam’s word is not in L(A) or Eve’s run is accepting. In other words, an automaton is history-deterministic if there is a way to build accepting runs on the fly, letter by letter.

Limit average automata

Quantitative automata represent funcitons from (finite or infinite) words to values. Limit avegrage (or Mean payoff) automata are quantitative automata that capture value of a word by looking at the long-term average of its behaviour.

The aim of this project is to investigate the power of history-determinism in limit average automata. In particular, we are interested in whether history-deterministic limit-average automata are more expressive (or, failing that, more succinct) than deterministic ones, and whether we can decide (a) whether a limit-average automaton is history-deterministic (b) whether a history-deterministic limit-average automaton is determinisable.

Design a site like this with WordPress.com
Get started