历史寄存器自动机

具有动态分配能力的程序能够创建和使用无限数量的新资源，如引用、对象、文件等。我们提出了历史寄存器自动机 (HRA)，这是一种用于建模此类程序的新的自动机理论形式化方法。HRA 扩展了先前方法的表达能力，并将可达性检查的可判定性推向了极限。我们机器的独特特征在于其使用无限内存集（历史），输入符号可以有选择地存储在其中并与后续符号进行比较。此外，存储的符号可以通过重置被消耗或删除。我们表明，消耗和重置能力的结合使得自动机强大到足以模拟计数器机，并产生除补运算外对所有正则运算的封闭性。我们还考察了较弱的 HRA 概念，它们在表达能力和有效性之间取得了不同的平衡。