用SAT学习最小化Büchi自动机
Learn with SAT to Minimize Büchi Automata
摘要：
我们描述了一个不确定的Büchi自动机（NBA）的最小化过程。对于一个自动机A，另一个具有最小状态数的自动机A_min在SAT求解器的帮助下学习。这是通过连续计算自动机A'来完成的，自动机A'在某种意义上近似A，它们接受给定的有限的正例集，拒绝给定的有限的负例集。在程序的过程中，这些示例集被连续地增加。因此，我们的方法可以被看作是一个通用的学习算法的基础上的“最低限度的适当的老师”的意义上的盎格鲁。我们使用SAT求解器为给定的正面和负面示例集找到NBA。我们通过构造确定性奇偶自动机来使用互补来检查以这种方式计算的候选者与A的等价性。不对等会产生新的正面或负面例子。我们的方法被证明是成功的完全采样的小自动机和相当多的例子较大的自动机。我们成功地运行了超过一万个自动机的最小化，其中大多数最多有十个状态，包括所有可能的自动机的补充与两个状态和字母表大小3，并讨论结果和运行时;单个例子有超过100个状态。
英文摘要：
We describe a minimization procedure for nondeterministic Büchi automata (NBA). For an automaton A another automaton A_min with the minimal number of states is learned with the help of a SAT-solver. This is done by successively computing automata A' that approximate A in the sense that they accept a given finite set of positive examples and reject a given finite set of negative examples. In the course of the procedure these example sets are successively increased. Thus, our method can be seen as an instance of a generic learning algorithm based on a "minimally adequate teacher" in the sense of Angluin. We use a SAT solver to find an NBA for given sets of positive and negative examples. We use complementation via construction of deterministic parity automata to check candidates computed in this manner for equivalence with A. Failure of equivalence yields new positive or negative examples. Our method proved successful on complete samplings of small automata and of quite some examples of bigger automata. We successfully ran the minimization on over ten thousand automata with mostly up to ten states, including the complements of all possible automata with two states and alphabet size three and discuss results and runtimes; single examples had over 100 states.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
