DEQ: Equivalence Checker for Deterministic Register Automata

Andrzej S. Murawski, Steven J Ramsay, Nikos Tzevelekos

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

104 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationATVA 2019
Subtitle of host publicationAutomated Technology for Verification and Analysis
EditorsYu-Feng Chen, Chih-Hong Cheng, Javier Esparza
Number of pages7
ISBN (Print)978-3-030-31783-6
Publication statusPublished - 21 Oct 2019

Publication series

NameProgramming and Software Engineering [Lectures in Computer Science]
ISSN (Print)0302-9743


Dive into the research topics of 'DEQ: Equivalence Checker for Deterministic Register Automata'. Together they form a unique fingerprint.

Cite this