Artifact for (An L# Based Algorithm for Active Learning of Minimal Separating Automata) @CAV2026

This artifact contains two Dockers files that make it possible to reproduce the experiments described in the CAV'26 paper the "An L# Based Algorithm for Active Learning of Minimal Separating Automata". Abstract: A DFA separates two disjoint languages L1 and L2 if it accepts every word in l1 and rejects every word in L2. Algorithms for active learning of small separating DFAs have many applications, e.g., for learning network invariants, learning contextual assumptions in compositional verification, learning state machines from large amounts of log data, and learning bug pattern descriptions. We propose a new and simple learning algorithm, inspired by L#, that learns a minimal separating DFA for disjoint languages L1 and L2 if one exists. Experiments show that our algorithm significantly outperforms existing active learning algorithms on both randomly generated and industrial benchmarks.本研究工件包含两个Docker文件，可复现发表于2026年CAV（国际计算机辅助验证会议，Computer-Aided Verification）会议论文《基于L#的极小分离自动机主动学习算法》中的实验。 摘要：若确定性有限自动机（Deterministic Finite Automaton, DFA）接受语言L₁中的所有字符串，并拒绝语言L₂中的所有字符串，则该DFA可分离两个不相交的语言L₁与L₂。面向小型分离DFA的主动学习算法具备诸多应用场景，例如学习网络不变量、在组合验证中学习上下文假设、从海量日志数据中学习状态机，以及学习缺陷模式描述。我们提出了一种受L#启发的新型简洁学习算法，该算法可针对不相交语言L₁与L₂学习得到极小分离DFA（若其存在）。实验结果表明，相较于现有主动学习算法，我们的算法在随机生成基准与工业基准上均实现了显著的性能提升。