Learning Universally Quantified Invariants of Linear Data Structures
Learning Universally Quantified Invariants of Linear Data Structures
复制标题
学习线性数据结构的通用量化不变量
DOI：
10.1007/978-3-642-39799-8_57
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
D. Neider
中科院分区：
文献类型：
--
作者：
P. Garg;Christof Löding;P. Madhusudan;D. Neider
我们提出了一种新的自动机模型，称为量化的数据自动机，可以对线性数据结构进行量化不变性，并为其构建Poly Pime Active学习算法，其中允许学习者查询教师的成员资格和等效查询。为了表达可定义逻辑中的不变性，我们发明了一个可定义的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.