π-演算中深度有界性的一个证明系统
A Type System for proving Depth Boundedness in the pi-calculus
摘要：
深度有界的π演算片段是一类具有可判定性的系统，它可以解决一些重要的验证问题。不幸的是，片段的成员身份是不可判定的。我们提出了一种新的类型系统，参数化的有限森林，正式的名称使用的方式，尊重森林的π条款。类型检查是可判定的，类型推断是可计算的;此外，可类型化的pi项保证是深度有界的。第二个贡献的文件是一个等价的证明之间的语义类型的条款和嵌套的数据类记忆自动机，一类自动机的数据字。我们相信，这种联系可以帮助建立新的联系之间的丰富理论的无限字母表自动机和名义演算。
英文摘要：
The depth-bounded fragment of the pi-calculus is an expressive class of systems enjoying decidability of some important verification problems. Unfortunately membership of the fragment is undecidable. We propose a novel type system, parameterised over a finite forest, that formalises name usage by pi-terms in a manner that respects the forest. Type checking is decidable and type inference is computable; furthermore typable pi-terms are guaranteed to be depth bounded. The second contribution of the paper is a proof of equivalence between the semantics of typable terms and nested data class memory automata, a class of automata over data words. We believe this connection can help to establish new links between the rich theory of infinite-alphabet automata and nominal calculi.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
