A bottleneck in modern active automata learning is to test whether a hypothesized Mealy machine correctly describes the system under learning. The search space for possible counterexamples is given by so-called test suites, consisting of input sequences that have to be checked to decide whether a counterexample exists. This paper shows that significantly smaller test suites suffice under reasonable assumptions on the structure of the black box. These smaller test suites help to refute false hypotheses during active automata learning, even when the assumptions do not hold. We combine multiple test suites using a multi-armed bandit setup that adaptively selects a test suite. An extensive empirical evaluation shows the efficacy of our approach. For small to medium-sized models, the performance gain is limited. However, the approach allows learning models from large, industrial case studies that were beyond the reach of known methods.
翻译:现代主动式自动机学习的一个瓶颈在于测试假设的米利机是否正确描述了待学习系统。用于发现潜在反例的搜索空间由所谓测试套件构成,这些套件包含需要检查的输入序列,以判定是否存在反例。本文证明,在黑盒结构合理假设下,使用显著更小的测试套件即可达成目标。即便假设条件不成立,这些小型测试套件仍有助于在主动式自动机学习过程中反驳错误假设。我们通过多臂赌博机框架组合多个测试套件,实现自适应选择测试套件。大量实证评估表明了我们方法的有效性。对于中小型模型,性能提升较为有限。然而,该方法能够从已知方法无法触及的大型工业案例中学习模型。