一句话：用分离控制与内存的 split 自动机编码 FICA，并为高阶并发找到一个验证可判定片段。
论文关注高阶并发程序的分析与验证。作者以 Finitary Idealised Concurrent Algol（FICA）为对象，结合自动机理论与博弈语义，提出一种定义在树结构无限数据字母表上的 split automata，其核心特征是控制与内存分离。他们证明每个 FICA 项都可翻译成此类自动机，从而能够观察底层博弈语义的细微性质。基于该编码，作者识别出 FICA 的一个片段：含迭代与受限同步但不含递归；与完整 FICA 不同，该片段上的多种验证问题可判定。
Using a combination of automata-theoretic and game-semantic techniques, we propose a method for analysing higher-order concurrent programs. Our language of choice is Finitary Idealised Concurrent Algol (FICA) due to its relatively simple fully abstract game model.Our first contribution is an automata model over a tree-structured infinite data alphabet, called split automata, whose distinctive feature is the separation of control and memory. We show that every FICA term can be translated into such an automaton. Thanks to the structure of split automata, we are able to observe subtle aspects of the underlying game semantics.This enables us to identify a fragment of FICA with iteration and limited synchronisation (but without recursion), for which, in contrast to the whole FICA, a variety of verification problems turn out to be decidable.