Abstract
We consider the verification problem for Dynamic Register Automata (DRA). DRA extend classical register automata by process creation. In this setting, each process is equipped with a finite set of registers in which the process IDs of other processes can be stored. A process can communicate with processes whose IDs are stored in its registers and can send them the content of its registers. The state reachability problem asks whether a DRA reaches a configuration where at least one process is in an error state. We first show that this problem is in general undecidable. This result holds even when we restrict the analysis to configurations where the maximal length of the simple paths in their underlying (un)directed communication graphs are bounded by some constant. Then we introduce the model of degenerative DRA which allows nondeterministic reset of the registers. We prove that for every given DRA, its corresponding degenerative one has the same set of reachable states. While the state reachability of a degenerative DRA remains undecidable, we show that the problem becomes decidable with nonprimitive recursive complexity when we restrict the analysis to strongly bounded configurations, i.e. configurations whose underlying undirected graphs have bounded simple paths. Finally, we consider the class of strongly safe DRA, where all the reachable configurations are assumed to be strongly bounded. We show that for strongly safe DRA, the state reachability problem becomes decidable.
BibTeX  Entry
@InProceedings{abdulla_et_al:LIPIcs:2014:4878,
author = {Parosh Aziz Abdulla and Mohamed Faouzi Atig and Ahmet Kara and Othmane Rezine},
title = {{Verification of Dynamic Register Automata}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {653665},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897774},
ISSN = {18688969},
year = {2014},
volume = {29},
editor = {Venkatesh Raman and S. P. Suresh},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2014/4878},
URN = {urn:nbn:de:0030drops48787},
doi = {10.4230/LIPIcs.FSTTCS.2014.653},
annote = {Keywords: Verification, Reachability problem, Register automata}
}
Keywords: 

Verification, Reachability problem, Register automata 
Collection: 

34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014) 
Issue Date: 

2014 
Date of publication: 

12.12.2014 