带有不完整但归纳性教师的自动机学习（技术报告）
Automata Learning with an Incomplete but Inductive Teacher (Technical Report)
AI总结：
本文提出IdMAT新教师形式化方法及LIndA算法，用于自动机学习中的归纳不变量合成，通过SAT求解处理不确定性与反例。
摘要：
主动自动机学习（AAL）在最小充分教师（MAT）下的应用已成功用于通过成员查询和等价性查询推断出一个正则语言。该语言可能并未完全表征：我们因此感兴趣于在目标类中寻找任何解，可能包含许多正则语言。一些问题如正则语言分离或在正则模型检查（RMC）背景下的归纳不变量合成确实可能有多个答案。因此，我们引入IdMAT：一种新的教师形式化方法，能够同时针对目标类中的任何语言回答查询。这种针对不变量合成优化的教师可能提供不完整的
英文摘要：
Active automata learning (AAL) under a Minimally Adequate Teacher (MAT) has been successfully used to infer a regular language through membership and equivalence queries. This language might not be fully characterized: we are then interested in finding any solution in a target class of possibly many regular languages. Some problems such as regular language separation or inductive invariant synthesis in the context of regular model checking (RMC) may indeed admit more than one answer. We therefore introduce IdMAT: a new teacher formalism answering queries with respect to any language in the target class, all at once. Such a teacher tailored towards invariant synthesis might provide incomplete "don't know" answers, but also inductive facts of the form "if w1 is accepted, so is w2". We pair IdMAT with a novel AAL algorithm LIndA that 1. encodes all uncertainties as a unique SAT instance and does not fork, 2. leverages incremental SAT solving and UNSAT core analysis, and 3. handles counterexamples of the simple or inductive type in a frugal manner inspired by the Rivest-Schapire refinement technique. We finally evaluate a prototype implementation in the context of regular language separation and RMC.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
