← All problems
Unverified

On an equivalence between finitely many tokens and one invisible token

Consider a safety automaton AA, i.e., an automaton over infinite words where all but one rejecting sink state is accepting. For simplicity, we assume that AA has a single initial state. We will describe two game-based conditions for AA, 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 kk, the kk-explorability game of AA proceeds in infinitely many rounds and involves kk distinguishable tokens, which are all initially placed at the initial state of AA. In round ii of the kk-explorability game, where each of the kk tokens are each at some state of AA, the following sequence of moves are played. Letitia selects a letter aa For each token, Terence selects an outgoing transition on aa from the current state of that token, and then moves that token to the tail of that transition. The game then proceeds to round (i+1)(i+1). In the limit of an infinite play of this game, the sequence of letters played by Letitia forms a word ww while the path traced by Terence's kk-tokens trace kk runs on ww. Terence wins if either w∉L(A)w \notin L(A), or if at least one of his tokens traces an accepting run. If Terence has a strategy to win the kk-explorability game of AA for some kk, then we say that AA is explorable. Condition 2. Positive stochastic resolvability 1 The stochastic resolvability (SR) game of AA is similar to the 11-explorability game of AA, 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 AA is positively stochastically resolvable if there is a λ>0\lambda>0 and a strategy for Terence using which Terence wins the SR game on AA with probability at least λ\lambda. Conjecture. AA is explorable if and only if AA 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

Coming soon

Organizer

Boyuan Wang portraitBoyuan Wang
Minghan Wang portraitMinghan Wang
Bochao Li portraitBochao Li
Hongwei Hu portraitHongwei Hu