序列理论的决策程序（技术报告）
摘要：序列理论是对字符串理论的扩展，字符串理论中字母表是无穷的，而序列理论对应的字母表理论可以是线性整数算术等。序列是可扩展数组的自然抽象，允许包括附加、映射、分割和连接在内的多种操作。尽管主流的SMT求解器对序列理论的工具支持越来越多，但对序列理论的可判定性了解甚少，这与对字符串理论的掌握程度形成鲜明对比。我们表明，具有连接和正则约束的可判定字符串理论可以扩展到形成布尔代数的字母表理论上的序列世界，同时保持可判定性。特别地，当正则约束被解释为参数化自动机（扩展了符号自动机和变量自动机）时，可判定性成立，但当被解释为寄存器自动机（即使在相等字母表理论上）时则失败。当添加长度约束时，该问题与具有长度（和正则）约束的单词方程等价。在具有符号传导器的情况下也进行了类似的研究，符号传导器自然地模拟了序列函数，如映射、分割、过滤等等。我们开发了一个基于参数化自动机的新的序列求解器SeCo，并在两类基准测试中展示了其有效性：（i）对操作数组的程序和参数化系统进行不变式检查，以及（ii）对符号寄存器自动机进行基准测试。
作者：Artur Je.z, Anthony W. Lin, Oliver Markgraf, Philipp R"ummer
论文ID：2308.00175
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-08-02