Creative Commons Attribution 3.0 Unported license
Register automata (RAs) are finite automata extended with a finite set of registers to store and compare data. We study the concept of synchronizing data words in RAs: Does there exist a data word that sends all states of the RA to a single state? For deterministic RAs with k registers (k-DRAs), we prove that inputting data words with 2k+1 distinct data, from the infinite data domain, is sufficient to synchronize. We show that the synchronizing problem for DRAs is in general PSPACE-complete, and is NLOGSPACE-complete for 1-DRAs. For nondeterministic RAs (NRAs), we show that Ackermann(n) distinct data (where n is the size of RA) might be necessary to synchronize. The synchronizing problem for NRAs is in general undecidable, however, we establish Ackermann-completeness of the problem for 1-NRAs. Our most substantial achievement is proving NEXPTIME-completeness of the length-bounded synchronizing problem in NRAs (length encoded in binary). A variant of this last construction allows to prove that the bounded universality problem in NRAs is co-NEXPTIME-complete.
@InProceedings{babari_et_al:LIPIcs.MFCS.2016.15,
author = {Babari, Parvaneh and Quaas, Karin and Shirmohammadi, Mahsa},
title = {{Synchronizing Data Words for Register Automata}},
booktitle = {41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)},
pages = {15:1--15:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-016-3},
ISSN = {1868-8969},
year = {2016},
volume = {58},
editor = {Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2016.15},
URN = {urn:nbn:de:0030-drops-64996},
doi = {10.4230/LIPIcs.MFCS.2016.15},
annote = {Keywords: data words, register automata, synchronizing problem, Ackermann-completeness, bounded universality, regular-like expressions with squaring}
}