Register automata are one of the most studied automata models over infinite alphabets with applications in learning, systems modelling and program verification. We present an equivalence checker for deterministic register automata, called DEQ, based on a recent polynomial-time algorithm that employs group-theoretic techniques to achieve succinct representations of the search space. We compare the performance of our tool to other available implementations, notably the learning library RALib and nominal frameworks LOIS and NLambda.
|Title of host publication||ATVA 2019|
|Subtitle of host publication||Automated Technology for Verification and Analysis|
|Editors||Yu-Feng Chen, Chih-Hong Cheng, Javier Esparza|
|Number of pages||7|
|Publication status||Published - 21 Oct 2019|
|Name||Programming and Software Engineering [Lectures in Computer Science]|