论文标题
测试的守卫Kleene代数：自动机学习
Guarded Kleene Algebra with Tests: Automata Learning
论文作者
论文摘要
带有测试（GKAT）的守卫Kleene代数是Kleene代数的片段，其测试（KAT）是通过用鉴定式变体代替Kat的联合和迭代操作而产生的。 GKAT比KAT更有效地可以决定，并且表现力足以模拟简单的命令式程序，从而使其对应用程序的应用程序有吸引力。网络验证。在本文中，我们进一步探讨了GKAT的自动机理论，并介绍了GL*，这是一种通过观察其行为来学习黑框的GKAT自动机表示的算法。复杂性分析表明，学习具有GL*的GKAT程序的表示比使用Angluin的现有L*算法更有效。我们在OCAML中实现gl*和l*，并在示例程序中比较他们的性能。
Guarded Kleene Algebra with Tests (GKAT) is the fragment of Kleene Algebra with Tests (KAT) that arises by replacing the union and iteration operations of KAT with predicate-guarded variants. GKAT is more efficiently decidable than KAT and expressive enough to model simple imperative programs, making it attractive for applications to e.g. network verification. In this paper, we further explore GKAT's automata theory, and present GL*, an algorithm for learning the GKAT automaton representation of a black-box, by observing its behaviour. A complexity analysis shows that it is more efficient to learn a representation of a GKAT program with GL* than with Angluin's existing L* algorithm. We implement GL* and L* in OCaml and compare their performances on example programs.
