On an equivalence between finitely many tokens and one invisible token
Consider a safety automaton , i.e., an automaton over infinite words where all but one rejecting sink state is accepting. For simplicity, we assume that has a single initial state. We will describe two game-based conditions for , which we conjecture to be equivalent. Both of these games involve a letter-picking adversary Letitia and a transition-picking protagonist Terence. Condition 1. Explorability For every positive natural number , the -explorability game of proceeds in infinitely many rounds and involves distinguishable tokens, which are all initially placed at the initial state of . In round of the -explorability game, where each of the tokens are each at some state of , the following sequence of moves are played. Letitia selects a letter For each token, Terence selects an outgoing transition on from the current state of that token, and then moves that token to the tail of that transition. The game then proceeds to round . In the limit of an infinite play of this game, the sequence of letters played by Letitia forms a word while the path traced by Terence's -tokens trace runs on . Terence wins if either , or if at least one of his tokens traces an accepting run. If Terence has a strategy to win the -explorability game of for some , then we say that is explorable. Condition 2. Positive stochastic resolvability 1 The stochastic resolvability (SR) game of is similar to the -explorability game of , except that Letitia does not obtain information on where Terence's token is (and she also does not obtain information on the transitions that Terence picks). To maximise the chance of Terence winning, Terence's strategies are now stochastic. We say that is positively stochastically resolvable if there is a and a strategy for Terence using which Terence wins the SR game on with probability at least . Conjecture. is explorable if and only if is positively stochastically resolvable. The above conjecture is also open for parity automata. Footnotes: 1 Coming up with a more reasonable name is another open problem :p
