DEQ: Equivalence Checker for Deterministic Register Automata

Andrzej S. Murawski; Steven J Ramsay; Nikos Tzevelekos

doi:10.1007/978-3-030-31784-3_20

DEQ: Equivalence Checker for Deterministic Register Automata

Andrzej S. Murawski, Steven J Ramsay, Nikos Tzevelekos

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

3 Citations (Scopus)

223 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 language	English
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
Publisher	Springer
Pages	350-356
Number of pages	7
ISBN (Print)	978-3-030-31783-6
DOIs	https://doi.org/10.1007/978-3-030-31784-3_20
Publication status	Published - 21 Oct 2019

Publication series

Name	Programming and Software Engineering [Lectures in Computer Science]
Publisher	Springer
Volume	11781
ISSN (Print)	0302-9743

Access to Document

10.1007/978-3-030-31784-3_20

Full-text PDF (accepted author manuscript)
This is the author accepted manuscript (AAM). The final published version (version of record) is available online via Springer at https://link.springer.com/chapter/10.1007%2F978-3-030-31784-3_20. Please refer to any applicable terms of use of the publisher.
Accepted author manuscript, 383 KB

Handle.net

Persistent link

Cite this

Murawski, A. S., Ramsay, S. J., & Tzevelekos, N. (2019). DEQ: Equivalence Checker for Deterministic Register Automata. In Y.-F. Chen, C.-H. Cheng, & J. Esparza (Eds.), ATVA 2019: Automated Technology for Verification and Analysis (pp. 350-356). (Programming and Software Engineering [Lectures in Computer Science]; Vol. 11781). Springer. https://doi.org/10.1007/978-3-030-31784-3_20

@inproceedings{1e2215c14584483589daa7a668afddd3,

title = "DEQ: Equivalence Checker for Deterministic Register Automata",

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.",

author = "Murawski, \{Andrzej S.\} and Ramsay, \{Steven J\} and Nikos Tzevelekos",

year = "2019",

month = oct,

day = "21",

doi = "10.1007/978-3-030-31784-3\_20",

language = "English",

isbn = "978-3-030-31783-6",

series = "Programming and Software Engineering [Lectures in Computer Science]",

publisher = "Springer",

pages = "350--356",

editor = "Yu-Feng Chen and Chih-Hong Cheng and Javier Esparza",

booktitle = "ATVA 2019",

address = "United States",

}

DEQ: Equivalence Checker for Deterministic Register Automata. / Murawski, Andrzej S.; Ramsay, Steven J; Tzevelekos, Nikos.
ATVA 2019: Automated Technology for Verification and Analysis. ed. / Yu-Feng Chen; Chih-Hong Cheng; Javier Esparza. Springer, 2019. p. 350-356 (Programming and Software Engineering [Lectures in Computer Science]; Vol. 11781).

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

TY - GEN

T1 - DEQ

T2 - Equivalence Checker for Deterministic Register Automata

AU - Murawski, Andrzej S.

AU - Ramsay, Steven J

AU - Tzevelekos, Nikos

PY - 2019/10/21

Y1 - 2019/10/21

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-030-31784-3_20

DO - 10.1007/978-3-030-31784-3_20

M3 - Conference Contribution (Conference Proceeding)

SN - 978-3-030-31783-6

T3 - Programming and Software Engineering [Lectures in Computer Science]

SP - 350

EP - 356

BT - ATVA 2019

A2 - Chen, Yu-Feng

A2 - Cheng, Chih-Hong

A2 - Esparza, Javier

PB - Springer

ER -

DEQ: Equivalence Checker for Deterministic Register Automata

Abstract

Publication series

Access to Document

Handle.net

Fingerprint

Cite this