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)

45 Downloads (Pure)

Abstract

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
PublisherSpringer
Pages350-356
Number of pages7
ISBN (Print)978-3-030-31783-6
DOIs
Publication statusPublished - 21 Oct 2019

Publication series

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

Fingerprint

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

Cite this