Saturation is a fundamental game-semantic property satisfied by strategies that interpret higher-order concurrent programs. It states that the strategy must be closed under certain rearrangements of moves, and corresponds to the intuition that program moves (P-moves) may depend only on moves made by the environment (O-moves). We propose an automata model over an infinite alphabet, called saturating automata, for which all accepted languages are guaranteed to satisfy a closure property mimicking saturation. We show how to translate the finitary fragment of Idealized Concurrent Algol (FICA) into saturating automata, confirming their suitability for modelling higher-order concurrency. Moreover, we find that, for terms in normal form, the resultant automaton has linearly many transitions and states with respect to term size, and can be constructed in polynomial time. This is in contrast to earlier attempts at finding automata-theoretic models of FICA, which did not guarantee saturation and involved an exponential blow-up during translation, even for normal forms.

翻译：饱和性是策略解释高阶并发程序时所满足的基本博弈语义性质。该性质要求策略在特定的移动重排操作下保持封闭，反映了程序方移动（P-移动）仅能依赖于环境方移动（O-移动）这一核心直观。我们提出了一种基于无限字母表的自动机模型——饱和自动机，该模型确保其接受的所有语言均满足类似饱和性质的封闭性条件。通过将理想化并发Algol的有限片段（FICA）翻译为饱和自动机，验证了该模型对高阶并发建模的适配性。进一步发现，对于范式项生成的自动机，其状态数与转移数均与项规模呈线性关系，且可在多项式时间内完成构造。这一结果与早期将FICA建模为自动机理论的尝试形成鲜明对比——此前方法既无法保证饱和性，在翻译过程中（即使针对范式项）也必然导致指数级状态膨胀。