高阶并发的叶子自动机
Leafy Automata for Higher-Order Concurrency
摘要：
有限理想化并发算法（Finitary Idealized Concurrent Algol，FICA）是一种结合了函数式、命令式和并发计算的原型程序设计语言。存在一个完全抽象的FICA博弈模型，原则上可以用来证明FICA程序的等价性和安全性。不幸的是，这些问题对于整个语言来说都是不可判定的，并且只知道非常基本的可判定子语言。我们提出叶自动机作为一个专门的自动机理论的形式主义表示游戏语义的FICA。自动机使用具有树结构无限字母表。我们表明，游戏语义的任何FICA长期可以表示的痕迹，一个树叶自动机。相反，任何叶子自动机的迹都可以用FICA项表示。由于与FICA的密切匹配，我们认为叶自动机作为一个很有前途的起点，寻找可判定的语言子类，更一般地说，提供了一个新的视角高阶并发计算模型。此外，我们确定了一个片段的FICA，是适合验证翻译成一个特定的类叶自动机。使用后一类的局部性，其中级别之间的通信是有限的，每隔一级有界的，我们表明，他们的空虚问题是可判定的减少到Petri网的可达性。
英文摘要：
Finitary Idealized Concurrent Algol (FICA) is a prototypical programming language combining functional, imperative, and concurrent computation. There exists a fully abstract game model of FICA, which in principle can be used to prove equivalence and safety of FICA programs. Unfortunately, the problems are undecidable for the whole language, and only very rudimentary decidable sub-languages are known. We propose leafy automata as a dedicated automata-theoretic formalism for representing the game semantics of FICA. The automata use an infinite alphabet with a tree structure. We show that the game semantics of any FICA term can be represented by traces of a leafy automaton. Conversely, the traces of any leafy automaton can be represented by a FICA term. Because of the close match with FICA, we view leafy automata as a promising starting point for finding decidable subclasses of the language and, more generally, to provide a new perspective on models of higher-order concurrent computation. Moreover, we identify a fragment of FICA that is amenable to verification by translation into a particular class of leafy automata. Using a locality property of the latter class, where communication between levels is restricted and every other level is bounded, we show that their emptiness problem is decidable by reduction to Petri net reachability.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
