线性数据结构的泛量化不变量学习
Learning Universally Quantified Invariants of Linear Data Structures
摘要：
我们提出了一个新的自动机模型，称为量化数据自动机的话，可以在线性数据结构量化不变量的模型，并建立多时间主动学习算法，学习者被允许查询教师的成员资格和等价查询。为了表达可判定逻辑中的不变量，我们发明了一个可判定的QDA子类，称为弹性QDA，并证明了每个QDA都有唯一的最小过近似弹性QDA。然后，我们给出了这些理论上健全和有效的主动学习算法在被动学习框架中的应用，并表明我们可以有效地学习量化的线性数据结构不变量从动态运行的一个大类的程序中获得的样本。
英文摘要：
We propose a new automaton model, called quantified data automata over words, that can model quantified invariants over linear data structures, and build poly-time active learning algorithms for them, where the learner is allowed to query the teacher with membership and equivalence queries. In order to express invariants in decidable logics, we invent a decidable subclass of QDAs, called elastic QDAs, and prove that every QDA has a unique minimally-over-approximating elastic QDA. We then give an application of these theoretically sound and efficient active learning algorithms in a passive learning framework and show that we can efficiently learn quantified linear data structure invariants from samples obtained from dynamic runs for a large class of programs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
