历史寄存器自动机
History-Register Automata
摘要：
程序与动态分配能够创建和使用无限数量的新鲜资源，如引用，对象，文件等，我们提出了历史寄存器自动机（HRA），一个新的自动机理论的形式主义建模这样的程序。HRA扩展了以前方法的表达能力，并使我们达到了可达性检查的可判定性极限。我们的机器的显着特点是它们使用无限的记忆集（历史），输入的符号可以有选择地存储和比较的符号遵循。此外，存储的符号可以通过重置来消耗或删除。我们表明，消费和复位功能的组合，使自动机足够强大，以模仿计数器机，并在所有常规操作下，除了互补收益率关闭。此外，我们还研究了较弱的概念HRAs之间的表现力和有效性的不同的平衡。
英文摘要：
Programs with dynamic allocation are able to create and use an unbounded number of fresh resources, such as references, objects, files, etc. We propose History-Register Automata (HRA), a new automata-theoretic formalism for modelling such programs. HRAs extend the expressiveness of previous approaches and bring us to the limits of decidability for reachability checks. The distinctive feature of our machines is their use of unbounded memory sets (histories) where input symbols can be selectively stored and compared with symbols to follow. In addition, stored symbols can be consumed or deleted by reset. We show that the combination of consumption and reset capabilities renders the automata powerful enough to imitate counter machines, and yields closure under all regular operations apart from complementation. We moreover examine weaker notions of HRAs which strike different balances between expressiveness and effectiveness.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
