利用SAT学习以最小化布尔自动机
摘要：使用SAT求解器，我们描述了一种非确定性Büchi自动机（NBA）的最小化过程。对于一个自动机A，借助SAT求解器学习到另一个具有最少状态数量的自动机A_min。 这是通过逐步计算逼近A的自动机A'来完成的，这些自动机在接受给定的有限正例集合并拒绝给定的有限反例集合方面接近A。在过程中，这些示例集合逐步增加。因此，我们的方法可以看作是基于Angluin的“最小适应教师”的通用学习算法的一个实例。 我们使用SAT求解器为给定的正例和负例集合找到一个NBA。我们使用通过构造确定性奇偶自动机的补集来检查以这种方式计算的候选NBA与A的等价性。等价性失败会产生新的正例或反例。我们的方法在小型自动机的完整抽样以及相当多的较大自动机示例上取得了成功。 我们成功地在一万多个自动机上运行了最小化过程，大多数自动机的状态数最多为10个，包括所有可能的具有两个状态和字母表大小为3的自动机的补集，并讨论了结果和运行时间；单个示例具有超过100个状态。
作者：Stephan Barth, Martin Hofmann
论文ID：1210.2452
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2012-10-10