Peled 等人和 Steffen 等人的开创性工作在模型学习和正式方法的领域之间建立了迷人的联系，特别是模型检验和基于模型的测试。随后的研究已经证实，在没有反应系统的易处理的白箱模型的情况下，学习模型通常是可以以相对低的成本获得的优良的替代方案。

为了检查学习模型的属性，可以使用模型检查（model checking）。事实上，Peled 等人已经在一种叫「黑箱检查（black box checking）」的方法中展示了如何完全整合模型学习与模型检查，其基本思想是使用模型检查器作为图 4 中一致性测试工具的「预处理器（preprocessor）」。当教师接收到学习器的假设时，首先运行模型检查器以验证假设模型是否满足 SUL 规定的所有属性。只有假设为真时，才转发给一致性测试器（conformance tester）。如果其中一个 SUL 属性不成立，那么模型检查器产生一个反例。现在有两种情况。第一种可能性是反例可以在 SUL 上再现。这意味着我们已经在 SUL（或其规定中）中展示了一个错误，我们停止学习。第二种可能性是反例不能在 SUL 上再现。在这种情况下，教师遵循假设是不正确的原则向学习器返回反例。在后来的工作中，黑箱检查方法已经进一步完善，并已成功应用于几个工业案例。

大多数学习算法的所需会员查询数量随着输入数量线性增长，并与状态数量成二次方。这意味着当输入数量增长时，学习算法规模相当好；换句话说，制定一个新的假设是容易的。然而，检查假设是否正确（一致性测试）会很快成为大量输入的瓶颈。如果当前假设具有 n 个状态，则 SUL 具有 n' 个状态，并且存在 k 个输入，则在最坏的情况下，需要运行包含 n'-n 个输入的所有可能序列的测试序列，即 k(n' ? n) 个可能性。因此，模型学习目前只能应用于少于 100 个输入的情况下。因此，我们寻求帮助我们减少输入数量的方法。

抽象（abstraction）是将模型学习方法扩展到现实应用程序的关键。Cho 等人通过在僵尸网络服务器和学习软件之间放置仿真器/映射器（emulator/mapper），将字母符号具体化为有效的网络消息并将它们发送到僵尸网络服务器（botnet servers），成功推断出现实僵尸网络命令和控制协议的模型。当接收到响应时，仿真器作反向处理：它将响应消息抽象为输出的字母，并将它们传递到学习软件。这种学习设置的示意图概述如图 5 所示。处理抽象的中间映射器组件的想法是非常自然的，并且在许多关于自动机学习的案例研究中被隐含地或明确地使用。Aarts 等人通过与谓词抽象（predicate abstraction）和抽象解释（abstract interpretation）建立连接，发展出了关于中间性抽象（intermediate abstraction）的数学理论。

图.5

一个补充性的简单但实用的方法是将模型学习应用在多个更小的输入子集上。这将明显降低学习复杂性；还因为对于有限数量的刺激，可达状态的集合通常将更小。然后，对于输入的子集学习的模型可以用于在学习更大子集的模型时生成反例。例如，Chalupar 等人已经应用的另一种方法是将通常以特定顺序发生的多个输入动作合并成单个高级动作，从而减少输入的数量。再次，已经用少量高级输入学习的模型可以用于在后续实验中产生反例，其中这些输入被分解成它们的组成部分。

正如 C.A.R. Hoare 所说，一个人可以说，在每个大程序中都有一个小的状态机试图出去。通过选择适当的输入动作集合并定义适当的映射器/抽象，我们可以使这个小状态机对学习者可见。

应用案例