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-移动）的直观含义。我们提出一种基于无限字母表的自动机模型——饱和自动机，其所有可接受语言必然满足模仿饱和的封闭性质。我们展示了如何将理想化并发算法语言（FICA）的有限片段翻译为饱和自动机，验证了其适合建模高阶并发性。进一步发现，对于范式项，所生成的自动机在状态与转移数量上与项规模呈线性关系，且可在多项式时间内构建。这与此前为FICA寻求自动机理论模型的尝试形成对比——早期方法即使在处理范式时也无法保证饱和性，且翻译过程中存在指数级膨胀。