一句话：将 token 博弈扩展到定量自动机，刻画历史确定性并给出多类 HDness 判定复杂度。
历史确定性自动机的非确定性可仅由已读前缀消解，在博弈与合成中组合性良好，但判定 HDness 通常困难甚至不可判定。本文将 token 博弈推广到定量设置，用以判定定量自动机的 HDness。结果显示：1-token 博弈刻画有限字上所有定量/布尔自动机以及无限字上 discounted-sum、Inf、Reachability 的 HDness；2-token 博弈刻画无限字上 LimInf、LimSup、Sup 的 HDness。据此，Safety、Reachability、Inf、Sup 的 HDness 可在 PTime 判定，DSum 在 NP∩co-NP，LimSup 在拟多项式时间，LimInf 在指数时间；后两者在权重数为对数时仅需多项式时间。
A nondeterministic automaton is history-deterministic if its nondeterminism can be resolved by only considering the prefix of the word read so far. Due to their good compositional properties, history-deterministic automata are useful in solving games and synthesis problems. Deciding whether a given nondeterministic automaton is history-deterministic (the HDness problem) is generally a difficult task, which can involve an exponential procedure, or even be undecidable, as is the case for example with pushdown automata. Token games provide a PTime solution to the HDness problem of B\"uchi and coB\"uchi automata, and it is conjectured that 2-token games characterise HDness for all $\omega$-regular automata. We extend token games to the quantitative setting and analyse their potential to help deciding HDness of quantitative automata. In particular, we show that 1-token games characterise HDness for all quantitative (and Boolean) automata on finite words, as well as discounted-sum (DSum), Inf and Reachability automata on infinite words, and that 2-token games characterise HDness of LimInf and LimSup automata, as well as Sup automata on infinite words. Using these characterisations, we provide solutions to the HDness problem of Safety, Reachability, Inf and Sup automata on finite and infinite words in PTime, of DSum automata on finite and infinite words in NP$\cap$co-NP, of LimSup automata in quasipolynomial time, and of LimInf automata in exponential time, where the latter two are only polynomial for automata with a logarithmic number of weights.
@article{paperbot2185,
title = {Token Games and History-Deterministic Quantitative-Automata},
author = {Udi Boker and Karoliina Lehtinen},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 4},
year = {2023},
doi = {10.46298/lmcs-19(4:8)2023}
}