Polynomial-time equivalence testing for deterministic fresh-register automata

Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos

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

2 Citations (Scopus)
45 Downloads (Pure)

Abstract

Register automata are one of the most studied automata models over infinite alphabets. The complexity of language equivalence for register automata is quite subtle. In general, the problem is undecidable but, in the deterministic case, it is known to be decidable and in NP. Here we propose a polynomial-time algorithm building upon automata- and group-theoretic techniques. The algorithm is applicable to standard register automata with a fixed number of registers as well as their variants with a variable number of registers and ability to generate fresh data values (fresh-register automata). To complement our findings, we also investigate the associated inclusion problem and show that it is PSPACE-complete.

Original languageEnglish
Title of host publication43rd International Symposium on Mathematical Foundations of Computer Science, MFCS 2018
EditorsIgor Potapov, James Worrell, Paul Spirakis
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Number of pages14
Volume117
ISBN (Print)9783959770866
DOIs
Publication statusPublished - 1 Aug 2018
Event43rd International Symposium on Mathematical Foundations of Computer Science, MFCS 2018 - Liverpool, United Kingdom
Duration: 27 Aug 201831 Aug 2018

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
ISSN (Print)1868-8969

Conference

Conference43rd International Symposium on Mathematical Foundations of Computer Science, MFCS 2018
Country/TerritoryUnited Kingdom
CityLiverpool
Period27/08/1831/08/18

Structured keywords

  • Programming Languages

Keywords

  • Automata over infinite alphabets
  • Bisimilarity
  • Computational group theory
  • Language equivalence

Fingerprint

Dive into the research topics of 'Polynomial-time equivalence testing for deterministic fresh-register automata'. Together they form a unique fingerprint.

Cite this