Guarded Kleene Algebra with Tests: Automata Learning
Stefan Zetzsche, Alexandra Silva, Matteo Sammartino

TL;DR
This paper introduces GL*, an automata learning algorithm for Guarded Kleene Algebra with Tests (GKAT), demonstrating its efficiency over existing methods and its applicability to modeling simple imperative programs.
Contribution
The paper develops GL*, a novel automata learning algorithm specifically for GKAT, and provides a complexity analysis showing its improved efficiency over L*.
Findings
GL* outperforms L* in learning GKAT automata.
Implementation of GL* and L* in OCaml enables performance comparison.
GL* effectively models simple imperative programs using GKAT automata.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware Testing and Debugging Techniques · Software Engineering Research · Logic, programming, and type systems
