Verifying higher-order concurrency with data automata
Verifying higher-order concurrency with data automata
复制标题
使用数据自动机验证高阶并发
DOI：
--
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
I. Walukiewicz
中科院分区：
文献类型：
--
作者：
Alex Dixon;R. Lazic;A. Murawski;I. Walukiewicz
使用自动机理论和游戏语义技术相结合，我们提出了一种分析高阶并发程序的方法。我们选择的语言是有限理想并发算法（FICA），由于其相对简单的完全抽象的游戏模型。我们的第一个贡献是一个自动机模型的树结构的无限数据字母表，称为分裂自动机，其显着特点是分离的控制和记忆。我们表明，每一个FICA长期可以被翻译成这样的自动机。由于分裂自动机的结构，我们能够观察到微妙的方面的潜在的游戏semantics.This使我们能够识别一个片段的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.